Extracting Unsatisfiable Cores

In case a CSP instance is unsatisfiable, one may want to identify the cause of unsatisfiability. Extracting a minimal unsatisfiable core (i.e. subset) of constraints may be relevant. With ACE, this is possible by setting the value of the named parameter extraction, of function solve(), to True. If a core is extracted by the solver, the constant CORE is returned. In that case, one can call the function core() to get the constraints of the identified core.

Important. Currently, a string is returned by core(). We shall revisit this simplistic way of getting the information in the next version of PySCP$^3$.

First, we need first to import the library PyCSP 3 :

from pycsp3 import *

Let us consider the following toy model:

x = VarArray(size=10, dom=range(10))

satisfy(
    AllDifferent(x),
    x[0] > x[1],
    x[1] > x[2],
    x[2] > x[0]
);

This problem instance is unsatisfiable:

print(solve())

UNSAT

We can display an unstaisfiable core:

if solve(extraction=True) is CORE:
    print(core())

c CORE #C=3 #V=3 => { c3(x[0],x[2]) c2(x[2],x[1]) c1(x[1],x[0]) }