# 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[0m #C=3 #V=3 => { c3(x[0],x[2]) c2(x[2],x[1]) c1(x[1],x[0]) }