求解布尔不可满足子式的消解悖论算法

• 作者: 庞征斌 张建民 徐炜遐 李思昆 黎铁军
• 来源期刊: 国防科技大学学报
• 学科: 工学
• 关键词: 形式验证 布尔可满足问题 不可满足子式 消解悖论 局部搜索
• 年，卷（期）: 2015,（1）
• 所属期刊栏目: 专题:微处理器设计与工艺
• 页码范围: 21-27
• 页数: 7页
• 分类号: TP391
• 字数: 8565字
• 语种: 中文
• DOI: 10.11887/j.cn.201501004

摘要

求解布尔不可满足子式在超大规模集成电路设计与验证领域都具有非常重要的理论与应用价值，帮助 EDA 工具迅速定位错误与不一致。针对求解不可满足子式的非完全方法，提出了消解悖论与悖论解析树的概念，在此基础上提出一种启发式局部搜索算法。该算法根据公式的消解规则，采用局部搜索过程直接构造证明不可满足性的悖论解析树，而后递归搜索得到不可满足子式；算法中融合了布尔推理技术、动态剪枝方法及蕴含消除方法以提高搜索效率。基于随机测试集进行了实验对比，结果表明提出的算法优于同类算法。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李思昆	国防科技大学高性能计算国家重点实验室	100	974	16.0	27.0
2	张建民	国防科技大学计算机学院	11	15	2.0	3.0
3	黎铁军	国防科技大学计算机学院	13	39	4.0	6.0
4	庞征斌	国防科技大学并行与分布处理重点实验室	19	107	5.0	10.0
5	徐炜遐	国防科技大学并行与分布处理重点实验室	20	52	4.0	6.0