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

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.