Affiliations: CSI/CASL, University College Dublin, Dublin, Ireland. E-mails: {anton.belov, jpms}@ucd.ie | IST/INESC-ID, Technical University of Lisbon, Lisbon, Portugal. E-mail: ines@sat.inesc-id.pt
Note: [] Corresponding author: J. Marques-Silva, CASL, University College Dublin, Dublin, Ireland. E-mail: jpms@ucd.ie.
Abstract: Minimally Unsatisfiable Subformulas (MUS) find a wide range of practical applications, including product configuration, knowledge-based validation, and hardware and software design and verification. MUSes also find application in recent Maximum Satisfiability algorithms and in CNF formula redundancy removal. Besides direct applications in Propositional Logic, algorithms for MUS extraction have been applied to more expressive logics. This paper proposes two algorithms for computation of MUSes of propositional formulas in Conjunctive Normal Form (CNF). The first algorithm is optimal in its class, meaning that it requires the smallest number of calls to a SAT solver. The second algorithm extends earlier work, but implements a number of new techniques. Among these, this paper analyzes in detail the technique of recursive model rotation, which provides significant performance gains in practice. Experimental results, obtained on representative practical benchmarks, indicate that the new algorithms achieve significant performance gains with respect to state of the art MUS extraction algorithms.
