A_CDCL_overview.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In this notebook, we are going to have a quick look at a new functionality introduced in `choco-solver-4.10.0`: the Conflict-Driven Clause learning (CDCL) framework."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%%loadFromPOM\n",
    "<repository>\n",
    "  <id>oss-sonatype-snapshots</id>\n",
    "  <url>https://oss.sonatype.org/content/repositories/snapshots/</url>\n",
    "</repository>\n",
    "<dependency>\n",
    "  <groupId>org.choco-solver</groupId>\n",
    "  <artifactId>choco-solver</artifactId>\n",
    "  <version>4.10.0-SNAPSHOT</version>\n",
    "</dependency>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Such a framework is an adapation of the well-konw SAT [CDCL algorithm](https://en.wikipedia.org/wiki/Conflict-driven_clause_learning) to discrete constraint solver.\n",
    "By exploiting the implication graph (that records events, i.e. variables' modifications), this algorithm is able to derive a new constraint from the events that led to a contradiction. \n",
    "\n",
    "Once added to the constraint network, this constraint makes possible to \"backjump\" (non-chronological backtrack) to the appropriate decision in the decision path.\n",
    "\n",
    "In CP, learned constraints are denoted \"signed-clauses\" which is a disjunction of signed-literals, *i.e.* membership unary constraints : $\\bigvee_{i = 0}^{n} X_i \\in D_{i}$ where $X_i$ are variables and $D_i$ a set of values.\n",
    "A signed-clause is satisfied when at least one signed-literal is satisfied. \n",
    "\n",
    "#### Warning #### \n",
    "\n",
    "> In CP, CDCL algorithm requires that each constraint of a problem can be explained. Even though a default explanation function for any constraint, dedicated functions offers better performances. \n",
    "> In `choco-solver-4.10.0` a few set of constraints is equiped with dedicated explanation function (unary constraints, binary and ternary, sum and scalar). \n",
    "\n",
    "Ok, now let's move to a small example: the [Latin Square Problem](https://en.wikipedia.org/wiki/Latin_square).\n",
    "A latin square is an $n \\times n$ array filled with $n$ different values, each occurring exactly once in each row and exactly once in each column.\n",
    "\n",
    "Here is a function that models a naive version of the LS problem:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "import java.util.function.Function;\n",
    "import static java.util.stream.IntStream.range;\n",
    "import org.chocosolver.solver.Model;\n",
    "import org.chocosolver.solver.variables.IntVar;\n",
    "import org.chocosolver.solver.search.strategy.Search;\n",
    "\n",
    "Function<Integer, Model> latin = n -> {\n",
    "    Model model = new Model();\n",
    "    IntVar[] vars = model.intVarArray(\"c\", n * n, 1, n);\n",
    "    // Constraints\n",
    "    for (int i = 0; i < n; i++) {\n",
    "        int j = i;\n",
    "        range(0, n - 1)\n",
    "                .forEach(a -> range(a + 1, n)\n",
    "                        .forEach(b -> {\n",
    "                            vars[j * n + a].ne(vars[j * n + b]).post(); // rows\n",
    "                            vars[a * n + j].ne(vars[b * n + j]).post(); // cols\n",
    "                        }));\n",
    "    }\n",
    "    model.getSolver().setSearch(Search.inputOrderLBSearch(vars));\n",
    "    model.getSolver().showShortStatistics();\n",
    "    return model;\n",
    "};"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "A solution to LS problem with $n$ = 14 requires 523513 nodes:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "latin.apply(14).getSolver().solve();"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Using CDCL, the same solution can be found in only 1187 nodes:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Model m = latin.apply(14);\n",
    "m.getSolver().setLearningSignedClauses();\n",
    "m.getSolver().solve();"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Indeed, each of the 907 failures is derived into a new signed-clause which helps reducing the search space.\n",
    "Since the enumeration strategy is static, so the 2nd search space is ensured to be strictly included in the 1st one. \n",
    "\n",
    "#### Remark ####\n",
    "> The model can be improved by using an `allDifferent` constraint which offers a more powerful filtering algorithm. In that case, the CDCL doest not reduce the number of nodes explored.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Limitations ##\n",
    "\n",
    "One may noticed that, in comparison to the no-CDCL approach, very few nodes can be explored per second.\n",
    "This is due to the application of the CDCL algorithm which globally slows down the resolution process.\n",
    "Indeed:\n",
    "1. Events need to be recorded in the implication graph.\n",
    "2. New operations are executed on each conflict to derive a signed-clauses. \n",
    "3. The number of learned signed-clauses increases w.r.t. the number of conflict, this can slow down the propagation step (reaching a fix-point or detecting a new conflict).\n",
    "\n",
    "The last point is probably the most expensive one. That's why, from time to time, some learned clauses need to be forgotten (in `DefaultSettings`: every 100000 failures, half of them are removed under conditions).\n",
    "Beware, removing a learned sign may not be inconsequential.\n",
    "For example, the \"same\" contradiction can thrown again in the future, or the enumeration strategy may be impacted.\n",
    "\n",
    "In conclusion, CDCL can be very powerful in reducing search space. \n",
    "However, this reduction sometimes does not compensate the algorithm cost it comes with."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Java",
   "language": "java",
   "name": "java"
  },
  "language_info": {
   "codemirror_mode": "java",
   "file_extension": ".java",
   "mimetype": "text/x-java-source",
   "name": "Java",
   "pygments_lexer": "java",
   "version": "11+28"
  },
  "widgets": {
   "application/vnd.jupyter.widget-state+json": {
    "state": {},
    "version_major": 2,
    "version_minor": 0
   }
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}