{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "cf88ce2b",
   "metadata": {},
   "source": [
    "# Incremental Solving"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b1bcd8ca",
   "metadata": {},
   "source": [
    "Interestingly, one can really pilot the solving process by iteratively adding and/or removing constraints (and also adding/changing the objective), handling a form of incremental solving. To add constraints, we already know that it suffices to call *satisfy()*. To remove constraints, it suffices to call the function: \n",
    "\n",
    "*unpost()*\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "84755e52",
   "metadata": {},
   "source": [
    "When this function is called, the last *posting operation* is discarded: it corresponds to all constraints that were posted by the last call to *satisfy()*. It is also possible to give the index of the posting operation, and even a second parameter indicating the index of constraint(s) inside the specified posting operation."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d0988f75",
   "metadata": {},
   "source": [
    "Below, we illustrate incremental solving by showing how to enumerate solutions by means of solution-blocking constraints, how to simulate an optimization procedure and how to compute diversified solutions. But first, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "5353d2ff",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "25cb5a96",
   "metadata": {},
   "source": [
    "## Enumerating Solutions with Solution-Blocking Constraints"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "eb60feb6",
   "metadata": {},
   "source": [
    "For a given CSP $P$, a *solution-blocking constraint* of $P$ is a constraint that forbids a solution of $P$ (i.e., forbids a complete instantiation of the variables of $P$ corresponding to a solution). An original (but not necessarily efficient) way of enumerating the solutions of $P$ with a solver $S$ (that can, for example, only output a single solution) is to find solutions in sequence with $S$ while posting a new solution-blocking constraint every time a solution is found."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5a0c9aa9",
   "metadata": {},
   "source": [
    "Let us consider the following toy model:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "ba9f7d89",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=4, dom=range(7))\n",
    "\n",
    "satisfy(\n",
    "  AllDifferent(x),\n",
    "  Increasing(x),\n",
    "  Sum(x) == 10\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b3b8d83e",
   "metadata": {},
   "source": [
    "On the one hand, we can directly compute the number of solutions (and display them) as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "ea303d5b",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "4\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(n_solutions())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bba430ff",
   "metadata": {},
   "source": [
    "On the other hand, we can enumerate the solutions of this model by successively posting solution-blocking constraints:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "a51db14c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 1, 3, 6]\n",
      "Solution 2: [0, 1, 4, 5]\n",
      "Solution 3: [0, 2, 3, 5]\n",
      "Solution 4: [1, 2, 3, 4]\n"
     ]
    }
   ],
   "source": [
    "cnt = 0\n",
    "while solve() is SAT:\n",
    "    cnt += 1\n",
    "    print(f\"Solution {cnt}: {values(x)}\")\n",
    "    satisfy(x != values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d0b81a78",
   "metadata": {},
   "source": [
    "We can display the internal representation of the posted constraints; this way, although a little bit technical, we can see that the presence of the four solution-blocking constraints. Note that 'le'  and 'eq' stands for 'less than or equal to' and 'equal to'."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "4a903249",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "allDifferent(list:x[])\n",
      "ordered(list:x[], operator:le)\n",
      "sum(list:x[], condition:(eq,10))\n",
      "extension(list:x[], conflicts:(0,1,3,6))\n",
      "extension(list:x[], conflicts:(0,1,4,5))\n",
      "extension(list:x[], conflicts:(0,2,3,5))\n",
      "extension(list:x[], conflicts:(1,2,3,4))\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c781dc64",
   "metadata": {},
   "source": [
    "## Simulating an Optimization Procedure"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1e0f3834",
   "metadata": {},
   "source": [
    "For a given CSP $P$, an independent integer cost function $f$ to be minimized, defined from (the Cartesian product of the domains of) a subset $X$ of variables of $P$ to $\\mathbb{Z}$, and a solution $sol$ of $P$ whose cost computed by $f$ is $B$ , a *bound-improving constraint* of $P$ wrt $f$ and $sol$ is a constraint that forbids all solutions of $P$ with a bound greater than or equal to $B$: it can be written $f(X) < B$. An original (but not necessarily efficient) way of finding an optimal solution of $P$ wrt $f$ with a CSP solver $S$ is to find solutions in sequence with $S$ while posting a new bound-improving constraint every time a solution is found."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4bb13199",
   "metadata": {},
   "source": [
    "We give an illustration with the Prime-looking problem. But, we need first to clear everythinh has beend declared and posted."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "c1791cb6",
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9cbc9d54",
   "metadata": {},
   "source": [
    "The prime-looking problem is from Martin Gardner: a number is said to be prime-looking if it is composite but not divisible by 2, 3 or 5. We know that the three smallest prime-looking numbers are 49, 77 and 91. Can you find the prime-looking numbers less than 250?\n",
    "\n",
    "The model is rather simple:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "54c993aa",
   "metadata": {},
   "outputs": [],
   "source": [
    "# the number we look for\n",
    "x = Var(range(250))\n",
    "\n",
    "# a first divider\n",
    "d1 = Var(range(2, 250))\n",
    "\n",
    "# a second divider\n",
    "d2 = Var(range(2, 250))\n",
    "\n",
    "satisfy(\n",
    "    x == d1 * d2,\n",
    "    x % 2 != 0,\n",
    "    x % 3 != 0,\n",
    "    x % 5 != 0,\n",
    "    d1 <= d2\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "64a3aa6c",
   "metadata": {},
   "source": [
    "Let us consider that we have a cost function for this problem; this is simply the variable $x$ (to be maximized).\n",
    "One way of ensuring that we get a better solution after finding a first solution is given by the following piece of code: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "e384abcb",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "The prime-looking number is:  49\n",
      "The prime-looking number is:  77\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"The prime-looking number is: \", value(x))\n",
    "    satisfy(x > x.value)\n",
    "    if solve() is SAT:\n",
    "        print(\"The prime-looking number is: \", value(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "15fcd5b2",
   "metadata": {},
   "source": [
    "If we want to find an optimal solution, we can write instead:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "5fa8b6d2",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "The prime-looking number is:  77\n",
      "The prime-looking number is:  91\n",
      "The prime-looking number is:  119\n",
      "The prime-looking number is:  121\n",
      "The prime-looking number is:  133\n",
      "The prime-looking number is:  161\n",
      "The prime-looking number is:  203\n",
      "The prime-looking number is:  209\n",
      "The prime-looking number is:  217\n",
      "The prime-looking number is:  221\n",
      "The prime-looking number is:  247\n"
     ]
    }
   ],
   "source": [
    "while True:\n",
    "    if solve() is not SAT:\n",
    "        break\n",
    "    print(\"The prime-looking number is: \", value(x))\n",
    "    satisfy(x > x.value)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "77b19405",
   "metadata": {},
   "source": [
    "In some cases, one may be worried of posting many bound-improving constraints, knowing that only the last one is relevant (since it is stronger than the other ones). This can be observed that when displaying all posted constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "0ec5275c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "intension(function:eq(x,mul(d1,d2)))\n",
      "intension(function:ne(mod(x,2),0))\n",
      "intension(function:ne(mod(x,3),0))\n",
      "intension(function:ne(mod(x,5),0))\n",
      "intension(function:le(d1,d2))\n",
      "intension(function:gt(x,49))\n",
      "intension(function:gt(x,77))\n",
      "intension(function:gt(x,91))\n",
      "intension(function:gt(x,119))\n",
      "intension(function:gt(x,121))\n",
      "intension(function:gt(x,133))\n",
      "intension(function:gt(x,161))\n",
      "intension(function:gt(x,203))\n",
      "intension(function:gt(x,209))\n",
      "intension(function:gt(x,217))\n",
      "intension(function:gt(x,221))\n",
      "intension(function:gt(x,247))\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "704e8a78",
   "metadata": {},
   "source": [
    "To test another approach, let us first discard all constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "6e97e26f",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost(ALL)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c4bb8940",
   "metadata": {},
   "source": [
    "We can check that there are no more constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "69777d81",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "873e7fab",
   "metadata": {},
   "source": [
    "We post again the basic constraints of the model."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "50d04ffa",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    x == d1 * d2,\n",
    "    x % 2 != 0,\n",
    "    x % 3 != 0,\n",
    "    x % 5 != 0,\n",
    "    d1 <= d2\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "df568a96",
   "metadata": {},
   "source": [
    "And, to avoid keeping useless bound-improving constraints, we can store the object (constraint) that was posted previously so as to be able to delete it afterwards. This gives:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "72ae792a",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "The prime-looking number is:  49\n",
      "The prime-looking number is:  77\n",
      "The prime-looking number is:  91\n",
      "The prime-looking number is:  119\n",
      "The prime-looking number is:  121\n",
      "The prime-looking number is:  133\n",
      "The prime-looking number is:  161\n",
      "The prime-looking number is:  203\n",
      "The prime-looking number is:  209\n",
      "The prime-looking number is:  217\n",
      "The prime-looking number is:  221\n",
      "The prime-looking number is:  247\n"
     ]
    }
   ],
   "source": [
    "objective = None\n",
    "while True:\n",
    "    if solve() is not SAT:\n",
    "        break\n",
    "    print(\"The prime-looking number is: \", value(x))\n",
    "    if objective is not None:\n",
    "        objective.delete()\n",
    "    objective = satisfy(x > x.value)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "eb26cff6",
   "metadata": {},
   "source": [
    "We can check that only one bound-improving constraint is present."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "71ca1e1d",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "intension(function:eq(x,mul(d1,d2)))\n",
      "intension(function:ne(mod(x,2),0))\n",
      "intension(function:ne(mod(x,3),0))\n",
      "intension(function:ne(mod(x,5),0))\n",
      "intension(function:le(d1,d2))\n",
      "intension(function:gt(x,247))\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fea82f5f",
   "metadata": {},
   "source": [
    "Let us discard it."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "44492eb9",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "07be5792",
   "metadata": {},
   "source": [
    "We control that it is no more present."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "a4470e7c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "intension(function:eq(x,mul(d1,d2)))\n",
      "intension(function:ne(mod(x,2),0))\n",
      "intension(function:ne(mod(x,3),0))\n",
      "intension(function:ne(mod(x,5),0))\n",
      "intension(function:le(d1,d2))\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f8ecbb93",
   "metadata": {},
   "source": [
    "As an alternative, it is possible to call the function *unpost()* that discards the constraint(s) posted at the last call to *satisfy()*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "9103f27e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "The prime-looking number is:  49\n",
      "The prime-looking number is:  77\n",
      "The prime-looking number is:  91\n",
      "The prime-looking number is:  119\n",
      "The prime-looking number is:  121\n",
      "The prime-looking number is:  133\n",
      "The prime-looking number is:  161\n",
      "The prime-looking number is:  203\n",
      "The prime-looking number is:  209\n",
      "The prime-looking number is:  217\n",
      "The prime-looking number is:  221\n",
      "The prime-looking number is:  247\n"
     ]
    }
   ],
   "source": [
    "objective = False\n",
    "while True:\n",
    "    if solve() is not SAT:\n",
    "        break\n",
    "    print(\"The prime-looking number is: \", value(x))\n",
    "    if objective:\n",
    "        unpost()\n",
    "    else:\n",
    "        objective = True  \n",
    "    satisfy(x > x.value)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6e58b9f7",
   "metadata": {},
   "source": [
    "## Computing Diversified Solutions"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bd61db3a",
   "metadata": {},
   "source": [
    "Instead of enumerating solutions in the order \"fixed\" by the solver, one may want to diversify computed solutions by exploiting some distances. In other words, we may be interested in diverse solutions."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f5d331b5",
   "metadata": {},
   "source": [
    "Below, we give a few illustrations. But, we need first to clear everythinh has beend declared and posted."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "a0ab7818",
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "54a96077",
   "metadata": {},
   "source": [
    "Let us consider the following toy model:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "698f6181",
   "metadata": {},
   "outputs": [],
   "source": [
    "n = 8\n",
    "\n",
    "x = VarArray(size=n, dom=range(5))\n",
    "\n",
    "satisfy(\n",
    "    Maximum(x) == 4\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1b57cdf0",
   "metadata": {},
   "source": [
    "If we want to enumerate 5 solutions while maximizing the Hamming distance between found solutions, we can write this piece of code:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "id": "2ca4a722",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 0, 0, 0, 0, 0, 0, 4]\n",
      "Solution:  [1, 1, 1, 1, 1, 1, 4, 0]\n",
      "Solution:  [2, 2, 2, 2, 2, 4, 1, 1]\n",
      "Solution:  [3, 3, 3, 3, 4, 2, 2, 2]\n",
      "Solution:  [4, 4, 4, 4, 3, 3, 3, 3]\n"
     ]
    }
   ],
   "source": [
    "solutions = []\n",
    "while len(solutions) < 5 and solve() in {SAT, OPTIMUM}:\n",
    "    print(\"Solution: \", values(x))\n",
    "    solutions.append(values(x))\n",
    "    maximize(\n",
    "        Sum(x[i] != solution[i] for i in range(n) for solution in solutions)\n",
    "    )"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "33d2b1ce",
   "metadata": {},
   "source": [
    "Note that the problem instance is initially a CSP, and then becomes a COP because an objective is posted after the first turn of the loop (note also that any new objective overwrites the previous one, if any is present). This is the reason why we check if the solving status is either SAT or OPTIMUM."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "id": "b2923d08",
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2ecbff43",
   "metadata": {},
   "source": [
    "As a second illustration, let us consider the following model:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "id": "18e01cfc",
   "metadata": {},
   "outputs": [],
   "source": [
    "n = 8\n",
    "\n",
    "x = VarArray(size=n, dom=range(7))\n",
    "\n",
    "satisfy(\n",
    "    Sum(x) == 22\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2637435a",
   "metadata": {},
   "source": [
    "If we want to enumerate 5 solutions while maximizing the Euclidean distance between found solutions, we can write: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "id": "ca0f9f8e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 0, 0, 0, 4, 6, 6, 6]\n",
      "Solution:  [4, 6, 6, 6, 0, 0, 0, 0]\n",
      "Solution:  [6, 4, 0, 0, 6, 0, 0, 6]\n",
      "Solution:  [0, 0, 4, 6, 0, 6, 6, 0]\n",
      "Solution:  [0, 6, 6, 0, 6, 4, 0, 0]\n"
     ]
    }
   ],
   "source": [
    "solutions = []\n",
    "while len(solutions) < 5 and solve() in {SAT,OPTIMUM}:\n",
    "    print(\"Solution: \", values(x))\n",
    "    solutions.append(values(x))\n",
    "    maximize(\n",
    "        Sum(abs(x[i] - solution[i]) for i in range(n) for solution in solutions)\n",
    "    )"
   ]
  }
 ],
 "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
}