MUS Extraction using Clausal Proofs

Abstract. Recent work introduced an effective method for extraction of reduced unsatisfiable cores of CNF formulas as a by-product of vali-dation of clausal proofs emitted by conflict-driven clause learning SAT solvers. In this paper, we demonstrate that this method for trimming CNF formulas can also benefit state-of-the-art tools for the computation of a Minimal Unsatisfiable Subformula (MUS). Furthermore, we pro-pose a number of techniques that improve the quality of trimming, and demonstrate a significant positive impact on the performance of MUS extractors from the improved trimming.