-
题名基于否证蕴含的极小一阶不可满足子式求解算法
被引量：1
- 1
-
-
作者
张建民
沈胜宇
李思昆
-
机构
国防科学技术大学计算机学院
-
出处
《计算机学报》
EI
CSCD
北大核心
2010年第3期415-426,共12页
-
基金
国家自然科学基金(60603088)资助~~
-
文摘
解释公式不可满足的原因在软件分析与验证等众多领域都具有非常重要的理论与应用价值,而极小不可满足子公式能够为公式不可满足的原因提供精炼的解释,帮助应用领域的自动化工具迅速定位错误,准确地诊断问题失败的本质缘由.文中针对极小一阶不可满足子式的求解问题,引入了否证蕴含图及其正向与逆向可达结点的概念,并证明了不可满足子式与否证蕴含图之间的关系.基于二者的关系,提出了基于冲突分析与否证蕴含的极小一阶不可满足子式求解算法,并融合了蕴含图剪枝技术,以提高算法效率.通过实验与当前最优的深度优先搜索算法进行了比较,结果表明:文中的算法显著优于深度优先搜索算法,并且随着公式复杂度的增加,性能优势更加明显.
-
关键词
一阶逻辑公式
可满足模理论问题
极小不可满足子式
消解否证
否证蕴含图
-
Keywords
first-order formula
satisfiability modulo theories（SMT）
minimal unsatisfiable subformulae
resolution refutation
refutation implication graph
-
分类号
TP302
[自动化与计算机技术—计算机系统结构]
-
-
题名可满足性求解技术研究
被引量：4
- 2
-
-
作者
张建民
沈胜宇
李思昆
-
机构
国防科学技术大学计算机学院
-
出处
《计算机工程与科学》
CSCD
北大核心
2010年第1期50-54,共5页
-
基金
国家自然科学基金资助项目(60603088
90707003)
-
文摘
求解公式的可满足性在诸如形式化验证、电子设计自动化与人工智能等众多领域中都具有非常重要的理论与应用价值,成为近年来的研究热点。本文针对命题公式与一阶公式的可满足性问题,重点介绍了布尔可满足性与可满足性模理论求解技术的基本原理,并且根据算法的类型进行分类阐述,分析了各种算法的优缺点。最后,讨论了目前面临的主要挑战,对今后的研究方向进行了展望。
-
关键词
布尔可满足问题
可满足性模理论问题
完全方法
不完全方法
-
Keywords
Boolean satisfiability（SAT）
satisfiability modulo theories（SMT）
complete method
incomplete method
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
