| 求解布尔不可满足子式的消解悖论算法 |
| |
| 作者姓名： | 张建民 黎铁军 徐炜遐 庞征斌 李思昆 |
| |
| 作者单位： | 国防科学技术大学 计算机学院,国防科学技术大学 计算机学院,国防科学技术大学 并行与分布处理重点实验室,国防科学技术大学 并行与分布处理重点实验室,国防科技大学高性能国家重点实验室 |
| |
| 基金项目： | 国家自然科学基金项目（面上项目,重点项目,重大项目）;国家高技术研究发展计划（863计划） |
| |
| 摘 要： | 求解布尔不可满足子式在超大规模集成电路设计与验证领域都具有非常重要的理论与应用价值,帮助EDA工具迅速定位错误与不一致。针对求解不可满足子式的非完全方法,提出了消解悖论与悖论解析树的概念,在此基础上提出一种启发式局部搜索算法。该算法根据公式的消解规则,采用局部搜索过程直接构造证明不可满足性的悖论解析树,而后递归搜索得到不可满足子式;算法中融合了布尔推理技术、动态剪枝方法及蕴含消除方法以提高搜索效率。基于随机测试集进行了实验对比,结果表明提出的算法优于同类算法。
|
| 关 键 词： | 形式验证 布尔可满足问题 不可满足子式 消解悖论 局部搜索 |
| 收稿时间： | 2014-06-10 |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《国防科技大学学报》浏览原始摘要信息 |
|
点击此处可从《国防科技大学学报》下载免费的PDF全文 |
|
