MUS Extraction using Clausal Proofs

ABSTRACT. Recent work introduced an effective method to extract reduced unsatisfiable cores of CNF formulas as a by-product of validating 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 propose 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.