Recent work introduced an effective method for extraction of reduced unsatisfiable cores of
CNF formulas as a by-product of validation 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 propose a number of techniques that improve the
quality of trimming, and demonstrate a significant positive impact on the performance of …

These approaches work as follows: 1. Solve the input formula and compute a resolution
graph. 2. Remove all redundant clauses, ie, those not in the core. 3. Pick a unmarked clause
C, mark C, and solve the formula without C and all learned clauses that depend on C. 4. If
that formula is satisfiable, then return to 3. 5. Otherwise update the resolution graph and
return to 2. 6. Terminate when all clauses are marked.