Skip to content

Unsat Cores

For an unsatisfiable set of formulas, the UNSATCore is a set of propositions which the SAT Solver found to be unsatisfiable during its search. As described in the introduction chapter, this set does not need to be minimal.

Computing the Unsat Core

Internally, the unsat core is being computed by the UNSATCoreFunction directly on the solver. This only works for MiniSat and Glucose solvers and only if the parameter proofTracing is explicitly set to true. Additionally, when using a Glucose solver, the incremental mode has to be deactivated. As default, proof tracing is disabled since it requires slightly more time and memory.

As an example, consider the following list of propositions:

List<Proposition> props = new ArrayList<>();
props.add(new StandardProposition(p.parse("~A")));
props.add(new StandardProposition(p.parse("A | ~B")));
props.add(new StandardProposition(p.parse("B")));
props.add(new StandardProposition(p.parse("~B | C")));
props.add(new StandardProposition(p.parse("~C | D")));
props.add(new StandardProposition(p.parse("~D | E")));
props.add(new StandardProposition(p.parse("~C | E")));
props.add(new StandardProposition(p.parse("~E")));

When adding these formulas to a solver and solving them, the result is FALSE. Now we can extract the unsatisfiable core with

Tristate sat = solver.sat(); // (1)!
UNSATCore<Proposition> unsatCore = solver.unsatCore();
  1. sat() call is required and the result has to be FALSE before calling unsatCore()

The result is:

UNSATCore{
  isMUS=false,
  propositions=[
    StandardProposition{formula=~A, description=},
    StandardProposition{formula=A | ~B, description=},
    StandardProposition{formula=B, description=}
  ]
}

The first flag isMUS indicates whether the computed unsat core is known to be a MUS. To make sense of this, recall that a MUS is always an unsat core. Thus, also the MUS algorithms return an UNSATCore. In the case of computing a MUS with a MUS algorithm, the flag isMUS is true. When an unsat core has been extracted from the solver, at this point there is no guarantee that it is a MUS. Hence, in this use case the flag is always false.

The set of propositions in this core is:

~A
A | B
~B

In fact, we can see that this set of formulas contains a contradiction. And it only has 3 formulas compared to the original 8 formulas. In this case, it is even a MUS and a SMUS but this is a coincidence.

Practical Observation

Normally, the unsatisfiable core of a SAT solver does not have many redundant terms and usually reduces the original formulas/propositions significantly.