UnSAT core extraction with assumptions

When a model is unsatisfiable, it can be desirable to get a better idea of which Boolean variables make it unsatisfiable. Commonly, these Boolean variables are ‘switches’ that turn constraints on or off, hence such Boolean variables can be used to get a better idea of which constraints make the model unsatisfiable.

In the satisfiability literature, the Boolean variables of interests are called assumption literals and the solver will assume they are true. Any subset of these assumptions that, when true, makes the model unsatisfiable is called an unsatisfiable core.

Lazy Clause Generation solvers, like OR-Tools, are built on SAT solvers and hence can inherit the ability to define assumptions and extract an unsatisfiable core.

Since version 8.2, OR-Tools supports declaring assumptions, and extracting an unsat core. We also implement this functionality in CPMpy, using PySAT-like s.solve(assumptions=[...]) and s.get_core():

from cpmpy import *
from cpmpy.solvers import CPM_ortools

bv = boolvar(shape=3)
iv = intvar(0,9, shape=3)

# circular 'bigger then', UNSAT
m = Model(
    bv[0].implies(iv[0] > iv[1]),
    bv[1].implies(iv[1] > iv[2]),
    bv[2].implies(iv[2] > iv[0])
)

s = CPM_ortools(m)
print(s.solve(assumptions=bv))
print(s.status())
print("core:", s.get_core())
print(bv.value())

This opens the door to more advanced use cases, such as Minimal Unsatisfiable Subsets (MUS) and QuickXplain-like tools to help debugging.

In our tools, we implemented a simple MUS deletion based algorithm, using assumptions.

from cpmpy.tools import mus

print(mus(m.constraints))

We welcome any additional examples that use CPMpy in this way! Here is one example: the MARCO algorithm for enumerating all MUS/MSSes. Here is another: a stepwise explanation algorithm for SAT problems (implicit hitting-set based).

More information on how to use these tools can be found in the tools API documentation

One OR-Tools specific caveat is that this particular (default) solver’s Python interface is by design stateless. That means that, unlike in PySAT, calling s.solve(assumptions=bv) twice for a different bv array does NOT REUSE anything from the previous run: no warm-starting, no learnt clauses that are kept, no incrementality, so there will be some pre-processing overhead. If you know of another CP solver with a (Python) assumption interface that is incremental, let us know!

A final-final note is that you can manually warm-start OR-Tools with a previously found solution through s.solution_hint(); see also the MARCO code linked above.