| 引用本文: | 张建民,黎铁军,徐炜遐,等.求解布尔不可满足子式的消解悖论算法.[J].国防科技大学学报,2015,37(1):21-27.[点击复制] |
| ZHANG Jianmin,LI Tiejun,XU Weixia,et al.A resolution-based Boolean unsatisfiable subformulas computing algorithm[J].Journal of National University of Defense Technology,2015,37(1):21-27[点击复制] |
|
| |
|
|
| 本文已被：浏览 13299次 下载 8881次 |
| 求解布尔不可满足子式的消解悖论算法 |
| 张建民1, 黎铁军1, 徐炜遐2, 庞征斌2, 李思昆3 |
|
(1.国防科技大学 计算机学院，湖南 长沙 410073;2.国防科技大学 并行与分布处理重点实验室，湖南 长沙 410073;3.国防科技大学 高性能计算国家重点实验室，湖南 长沙 410073)
|
| 摘要: |
| 求解布尔不可满足子式在超大规模集成电路设计与验证领域都具有非常重要的理论与应用价值，帮助EDA工具迅速定位错误与不一致。针对求解不可满足子式的非完全方法，提出了消解悖论与悖论解析树的概念，在此基础上提出一种启发式局部搜索算法。该算法根据公式的消解规则，采用局部搜索过程直接构造证明不可满足性的悖论解析树，而后递归搜索得到不可满足子式；算法中融合了布尔推理技术、动态剪枝方法及蕴含消除方法以提高搜索效率。基于随机测试集进行了实验对比，结果表明提出的算法优于同类算法。 |
| 关键词: 形式验证 布尔可满足问题 不可满足子式 消解悖论 局部搜索 |
| DOI：10.11887/j.cn.201501004 |
| 投稿日期：2014-06-10 |
| 基金项目:国家自然科学基金资助项目（61103083,61133007）；国家863计划资助项目（2012AA01A301);国家973计划资助项目（2011CB309705) |
|
| A resolution-based Boolean unsatisfiable subformulas computing algorithm |
| ZHANG Jianmin1, LI Tiejun1, XU Weixia2, PANG Zhengbin2, LI Sikun3 |
|
(1. College of Computer, National University of Defense Technology, Changsha 410073, China;2. National Key Laboratory of Parallel and Distributed Processing, National University of Defense Technology, Changsha 410073, China;3. State Key Laboratory of High Performance Computing, National University of Defense Technology, Changsha 410073, China)
|
| Abstract: |
| Computing unsatisfiable subformulas of Boolean formulas has practical applications in VLSI design and verification. The unsatisfiable subformulas can help electronic design automation tools to rapidly locate the errors and inconsistency. The definitions of resolution refutation and refutation parsing tree, and a heuristic local search algorithm to extract unsatisfiable subformulas from the resolution refutation of a formula are presented. The approach directly constructs the refutation parsing tree for proving unsatisfiability with a local search procedure, and then recursively derives unsatisfiable subformulas. The algorithm combines with reasoning heuristics, dynamic pruning and subsumption elimination method to improve the efficiency. The experimental results show that our algorithm outperforms the similar algorithms on the random benchmarks. |
| Keywords: formal verification Boolean satisfaction unsatisfiable subformula resolution refutation local search |
|
|
