I. Introduction
Model checking techniques for safety properties (such as IC3/PDR [5], [7]) are fundamental in formal verification. Given a circuit and safety property, IC3 returns either (1) UNSAFE along with a counter-example trace that leads from an initial state to an unsafe state; or (2) SAFE along with a safe inductive invariant certifying that the circuit cannot reach an unsafe state. The former provides actionable feedback to the user that can be applied to identify the source of the failure. The latter typically does not, and as such, provides the user with little confidence that the check passes for the “right” reasons, rather than due to e.g., unjustified assumptions or vacuity. Boolean satisfiability solvers suffer from a similar lack of feedback regarding unsatisfiable formulas; the solver may be able to return a certificate such as a resolution refutation [22], but this provides limited insight. Instead, unsatisfiable cores—subsets of the clauses of the formula that are themselves unsatisfiable—appear more useful. Minimal unsatisfiable cores, also called minimal unsatisfiable subsets (MUSes) are of particular interest. Given an unsatisfiable formula, several algorithms have been developed to extract all MUSes [1], [14], [13], [18] or to extract a smallest MUS [11]. MUSes have seen application in a variety of areas including maximum satisfiability solving [15], vacuity detection [19], automated debugging [21], identifying missing constraints in verification [12], and others [16].