《计算机学报》文章摘要   全文下载
文章题目	基于否证蕴含的极小一阶不可满足子式求解算法
作者	张建民 沈胜宇 李思昆
作者单位	(国防科学技术大学计算机学院 长沙 410073)
发表年份	2010
发表月份	3期(415—426)
文章摘要	摘要 解释公式不可满足的原因在软件分析与验证等众多领域都具有非常重要的理论与应用价值，而极小不可满足子公式能够为公式不可满足的原因提供精炼的解释，帮助应用领域的自动化工具迅速定位错误，准确地诊断问题失败的本质缘由.文中针对极小一阶不可满足子式的求解问题，引入了否证蕴含图及其正向与逆向可达结点的概念，并证明了不可满足子式与否证蕴含图之间的关系.基于二者的关系，提出了基于冲突分析与否证蕴含的极小一阶不可满足子式求解算法，并融合了蕴含图剪枝技术，以提高算法效率.通过实验与当前最优的深度优先搜索算法进行了比较，结果表明：文中的算法显著优于深度优先搜索算法，并且随着公式复杂度的增加，性能优势更加明显. 关键词 一阶逻辑公式；可满足模理论问题；极小不可满足子式；消解否证；否证蕴含图 中图法分类号 TP302 DOI号: 10.3724/SP.J.1016.2010.00415