An algorithm to compute minimal unsatisfiable subsets for a decidable fragment of first-order formulas

In the past few years, SAT-based methods in propositional logic have been widely used to tackle practical problems in electronic design automation, software testing and hardware verification. However, lots of industrial problems can naturally be transformed to certain decidable fragments of first-order logic (FOL), which are more expressive than propositional logic. In this paper, we propose a novel algorithm to compute all minimal unsatisfiable subsets for a constrained variant of first-order formulas. By this means, we not only evaluate the satisfiability of specified formulas, but also extract minimal unsatisfiable cores. A heuristic strategy is proposed to improve the performance. Experimental results demonstrate that our algorithm performs well on many industrial instances, and the heuristic strategy is more robust than other strategies in time and space efficiency.