| 求解极小SMT不可满足子式的宽度优先搜索算法 |
| |
| 引用本文： | 张建民,沈胜宇,李思昆.求解极小SMT不可满足子式的宽度优先搜索算法[J].计算机辅助设计与图形学学报,2009,21(7). |
| |
| 作者姓名： | 张建民 沈胜宇 李思昆 |
| |
| 作者单位： | 国防科学技术大学计算机学院,长沙,410073 |
| |
| 摘 要： | 极小不可满足子式能够为可满足性模理论(SMT)公式的不可满足的原因提供精确的解释,帮助自动化工具迅速定位错误.针对极小SMT不可满足子式的求解问题,提出了SMT公式搜索树及其3类结点的概念,并给出了不可满足子式、极小不可满足子式与3类结点之间的映射关系.基于这种映射关系,采用宽度优先的搜索策略提出了宽度优先搜索的极小SMT不可满足子式求解算法.基于业界公认的SMT Competition 2007测试集进行实验的结果表明,该算法能够有效地求解极小不可满足子式.
|
| 关 键 词： | 可满足性模理论 极小不可满足子式 搜索树 宽度优先搜索 |
A Breadth-first-search Algorithm for Deriving Minimal Unsatisfiable Subformulae in Satisfiability Modulo Theories |
| |
| Zhang Jianmin,Shen Shengyu,Li Sikun.A Breadth-first-search Algorithm for Deriving Minimal Unsatisfiable Subformulae in Satisfiability Modulo Theories[J].Journal of Computer-Aided Design & Computer Graphics,2009,21(7). |
| |
| Authors: | Zhang Jianmin Shen Shengyu Li Sikun |
| |
| Affiliation: | College of Computer;National University of Defense Technology;Changsha 410073 |
| |
| Abstract: | A minimal unsatisfiable subformula can provide a succinct explanation of infeasibility of formulae in satisfiability modulo theories(SMT),and could be used in automatic tools to rapidly locate the errors.We present the definitions of searching tree for a formula in SMT and three kinds of nodes,and discuss the relationship between minimal unsatisfiable subformula and the nodes.Based on the relationship,we propose a breadth-first-search algorithm to derive minimal unsatisfiable subformulae in SMT.We have eval... |
| |
| Keywords: | DPLL(T) satisfiability modulo theories (SMT) minimal unsatisfiable subformula DPLL(T) searching tree breadth first search |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
