求解极小SMT不可满足子式的宽度优先搜索算法  

A Breadth-first-search Algorithm for Deriving Minimal Unsatisfiable Subformulae in Satisfiability Modulo Theories

作　　者：张建民[1] 沈胜宇[1] 李思昆[1] 

机构地区：[1]国防科学技术大学计算机学院,长沙410073

出　　处：《计算机辅助设计与图形学学报》2009年第7期984-990,共7页Journal of Computer-Aided Design & Computer Graphics

基　　金：国家自然科学基金(60603088;90707003)

摘　　要：极小不可满足子式能够为可满足性模理论(SMT)公式的不可满足的原因提供精确的解释,帮助自动化工具迅速定位错误.针对极小SMT不可满足子式的求解问题,提出了SMT公式搜索树及其3类结点的概念,并给出了不可满足子式、极小不可满足子式与3类结点之间的映射关系.基于这种映射关系,采用宽度优先的搜索策略提出了宽度优先搜索的极小SMT不可满足子式求解算法.基于业界公认的SMT Competition2007测试集进行实验的结果表明,该算法能够有效地求解极小不可满足子式.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 evaluated the effectiveness of the algorithm on SMT Competition 2007 industrial benchmarks. Experimental results show that the breadth-first-search algorithm can effectively compute minimal unsatisfiable subformula.

关 键 词：可满足性模理论 极小不可满足子式 DPLL(T) 搜索树 宽度优先搜索 

分 类 号：TP391.7[自动化与计算机技术—计算机应用技术]