基于否证蕴含的极小一阶不可满足子式求解算法

• 作者: 张建民 李思昆 沈胜宇
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 一阶逻辑公式 可满足模理论问题 极小不可满足子式 消解否证 否证蕴含图
• 年，卷（期）: 2010,（3）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 415-426
• 页数: 12页
• 分类号: TP302
• 字数: 12303字
• 语种: 中文
• DOI: 10.3724/SP.J.1016.2010.00415

摘要

解释公式不可满足的原因在软件分析与验证等众多领域都具有非常重要的理论与应用价值,而极小不可满足子公式能够为公式不可满足的原因提供精炼的解释,帮助应用领域的自动化工具迅速定位错误,准确地诊断问题失败的本质缘由.文中针对极小一阶不可满足子式的求解问题,引入了否证蕴含图及其正向与逆向可达结点的概念,并证明了不可满足子式与否证蕴含图之间的关系.基于二者的关系,提出了基于冲突分析与否证蕴含的极小一阶不可满足子式求解算法,并融合了蕴含图剪枝技术,以提高算法效率.通过实验与当前最优的深度优先搜索算法进行了比较,结果表明:文中的算法显著优于深度优先搜索算法,并且随着公式复杂度的增加,性能优势更加明显.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李思昆	国防科学技术大学计算机学院	133	1339	18.0	31.0
2	张建民	国防科学技术大学计算机学院	10	26	3.0	4.0
3	沈胜宇	国防科学技术大学计算机学院	8	30	3.0	5.0