中文摘要：

极小不可满足子式能够为可满足性模理论（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.