{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "e7a8df4d",
   "metadata": {},
   "source": [
    "# Extracting Unsatisfiable Cores"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2e2c26e6",
   "metadata": {},
   "source": [
    "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."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3f040a48",
   "metadata": {},
   "source": [
    "**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$."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "14b56292",
   "metadata": {},
   "source": [
    "First, we need first to import the library PyCSP 3 :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "d3ba64de",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1f2869c0",
   "metadata": {},
   "source": [
    "Let us consider the following toy model:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "05e1d6af",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=10, dom=range(10))\n",
    "\n",
    "satisfy(\n",
    "    AllDifferent(x),\n",
    "    x[0] > x[1],\n",
    "    x[1] > x[2],\n",
    "    x[2] > x[0]\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "288453d1",
   "metadata": {},
   "source": [
    "This problem instance is unsatisfiable:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "f4d068eb",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "UNSAT\n"
     ]
    }
   ],
   "source": [
    "print(solve())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0f99c897",
   "metadata": {},
   "source": [
    "We can display an unstaisfiable core:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "5ad44faf",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "c CORE\u001b[0m #C=3 #V=3 => { c3(x[0],x[2]) c2(x[2],x[1]) c1(x[1],x[0]) }\n"
     ]
    }
   ],
   "source": [
    "if solve(extraction=True) is CORE:\n",
    "    print(core())"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.7.12"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}