| 结合高级正向推理过程的可满足性问题解决器 |
| |
| 引用本文： | 丁敏,唐璞山,周电.结合高级正向推理过程的可满足性问题解决器[J].中国科学(E辑),2005,35(4):426-438. |
| |
| 作者姓名： | 丁敏 唐璞山 周电 |
| |
| 作者单位： | 上海复旦大学微电子系专用集成电路国家重点实验室,上海,200433 |
| |
| 基金项目： | 国家自然科学基金，国家高技术研究发展计划(863计划)，美国国家自然科学基金 |
| |
| 摘 要： | 提出了一个可满足性问题解决器,它结合了DPLL(Davis Putnam Loge- mann and Loveland)算法和作为高级推理技术之一的失败性文字检查(FLD,Failed Literal Detection)技术.在失败性文字检查技术中,又提出了动态筛选方法,它包含了两条规则: 内部和外部筛选.在保证能在每个决策层上发现大部分失败性文字的同时,降低了失败性文字检查所测试的文字数目及相应的计算时间.不同于其他类型的预定义的删除标准,在这一方法中文字的删除是动态的,从这点上讲,文中的失败性文字检查算法可以适应不同类型的测试基准实例.许多不必要的测试可以被避免,因而提高了失败性文字检查的计算速度.为了进一步提高失败性文字检查的效率,故此还增加了其他静态的测试约束.实验表明,经过优化后的失败性文字检查算法的效率明显高于其他的高级正向推理技术.
|
| 关 键 词： | 可满足性问题 形式验证 电子设计自动化 |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
