FMUS2: An efficient algorithm to compute minimal unsatisfiable subsets

Abstract

In the past few years, much attention has been given to the problem of finding Minimal Unsatisfiable Subsets (MUSes), not only for its theoretical importance but also for its wide range of practical applications, including software testing, hardware verification and knowledge-based validation. In this paper, we propose an algorithm for extracting all MUSes for formulas in the field of propositional logic and the function-free and equality-free fragment of first-order logic. This algorithm extends earlier work, but some changes have been made and a number of optimization strategies have been proposed to improve its efficiency. Experimental results show that our algorithm performs well on many industrial and generated instances, and the strategies adopted can indeed improve the efficiency of our algorithm.