{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "8f4deef8",
   "metadata": {},
   "source": [
    "# Constraint *ElementMatrix*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "05b84bb0",
   "metadata": {},
   "source": [
    "The constraint *ElementMatrix* ensures that the element of a specified matrix $x$ at specified indexes $i$ and $j$ has a specified value $v$.\n",
    "The semantics is $x[i][j] = v$. It is important to note that i and j are necessarily two integer variables of a constraint model (i.e., a variable of a CSP or COP model)."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ee828e2a",
   "metadata": {},
   "source": [
    "In Python, to post a constraint *ElementMatrix*, we use the facilities offered by the language, meaning that we can write expressions involving relational and indexing ([]) operators."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a8240e4b",
   "metadata": {},
   "source": [
    "## Variant 1"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "eb84e216",
   "metadata": {},
   "source": [
    "We consider the variant 1 of the constraint *ElementMatrix*: $x$ is a matrix of integer variables, $i$ and $j$ are  integer variables and $v$ is an integer variable. Important: we refer here to variables of the constraint model."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fa4712b5",
   "metadata": {},
   "source": [
    "To see how this constraint works, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "f5093871",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1be023fd",
   "metadata": {},
   "source": [
    "We introduce a two-dimensional array $x$ of $4 \\times 3$ variables, and three stand-alone variables $i$, $j$ and $v$ that will play the role of indexes and value."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "da9c6a1a",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=[3, 2], dom=range(4))\n",
    "i = Var(range(3))\n",
    "j = Var(range(2))\n",
    "v = Var(range(4))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "94c62976",
   "metadata": {},
   "source": [
    "We can display the structure of the array, as well as a few domains."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "eb405fd8",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Array x:  [\n",
      "  [x[0][0], x[0][1]]\n",
      "  [x[1][0], x[1][1]]\n",
      "  [x[2][0], x[2][1]]\n",
      "]\n",
      "A few domains:  0..3   0..2   0 1   0..3\n"
     ]
    }
   ],
   "source": [
    "print(\"Array x: \" ,x)\n",
    "print(\"A few domains: \", x[0][0].dom, \" \", i.dom, \" \", j.dom, \" \", v.dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "61681e67",
   "metadata": {},
   "source": [
    "Now, we can post a single constraint *ElementMatrix*, as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "29e3e714",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    x[i][j] == v\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fa7227e5",
   "metadata": {},
   "source": [
    "This means that the equation must hold, once we have assigned a value to all variables."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c9cf6729",
   "metadata": {},
   "source": [
    "By calling the function *solve()*, we can check that the problem (actually, the single constraint) is satisfiable (SAT). We can also display the values assigned to the variables in the solution that has been found."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "cb61f995",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[\n",
      "  [0, 0]\n",
      "  [0, 0]\n",
      "  [0, 0]\n",
      "]\n",
      "0 0 0\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(values(x))\n",
    "    print(value(i), value(j), value(v))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e7bf5b41",
   "metadata": {},
   "source": [
    "Clearly, the value in the first cell of $x$ (cell at row 0 and column 0) is equal to the value of $v$. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a2b4aca9",
   "metadata": {},
   "source": [
    "One question that we may ask is: how many solutions (supports) does there exist for our constraint taken alone? Because at any time (when variables are assigned), only one variable of the array is constrained, it means that we have $4^5 \\times 4 \\times 6$ solutions ($4^5$ possibilities for \"non concerned\" variables of $x$, $4$ possible values, and $6$ possibles indexes). We can check this by calling *solve()* with the named parameter *sols*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "222871be",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Last solution:  [\n",
      "  [2, 3]\n",
      "  [1, 2]\n",
      "  [0, 1]\n",
      "] 2 0 0\n",
      "Number of solutions:  24576\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(\"Last solution: \", values(x), value(i), value(j), value(v))\n",
    "    print(\"Number of solutions: \", n_solutions())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ddc43c38",
   "metadata": {},
   "source": [
    "## Variant 2"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5639f39f",
   "metadata": {},
   "source": [
    "We consider the variant 2 of the constraint *ElementMatrix*: $x$ is a matrix of integer variables, $i$ and $j$ are  integer variables and $v$ is an integer (not a variable). Important: we refer here to variables of the constraint model."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3fc5b16c",
   "metadata": {},
   "source": [
    "First of all, we need to remove everything that has been introduced so far by calling the function *clear()*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "bd902c72",
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()  # to clear previously posted variables and constraints"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2096da3b",
   "metadata": {},
   "source": [
    "We introduce a two-dimensional array $x$ of $3 \\times 2$ variables, and two stand-alone variables $i$ and $j$ that will play the role of indexes."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "0a98ba61",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=[3, 2], dom=range(4))\n",
    "i = Var(range(3))\n",
    "j = Var(range(2))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "950c57ba",
   "metadata": {},
   "source": [
    "Now, we can post a single constraint *ElementMatrix*, with the arbitrary value 1, as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "33cf7978",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    x[i][j] == 1\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "249cef30",
   "metadata": {},
   "source": [
    "By calling the function *solve()*, we can check that the problem (actually, the single constraint) is satisfiable (SAT). We can also display the values assigned to the variables in the found solution."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "066464f3",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[\n",
      "  [0, 0]\n",
      "  [0, 0]\n",
      "  [0, 1]\n",
      "] 2 1\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(values(x), value(i), value(j))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "71ae92a6",
   "metadata": {},
   "source": [
    "We should obtain 4 times less solutions than with the previous illustration (since the value is fixed), i.e., $4^5 \\times 6$ solutions. We can check this by calling *solve()* with the named parameter *sols*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "a432f143",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Last solution:  [\n",
      "  [2, 2]\n",
      "  [0, 0]\n",
      "  [1, 3]\n",
      "] 2 0\n",
      "Number of solutions:  6144\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(\"Last solution: \", values(x), value(i), value(j))\n",
    "    print(\"Number of solutions: \", n_solutions())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "67cf625f",
   "metadata": {},
   "source": [
    "## Variant 3"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "69c76fbc",
   "metadata": {},
   "source": [
    "We consider the variant 3 of the constraint *ElementMatrix*: $x$ is a matrix of integers (not variables), $i$ and $j$ are integer variables and $v$ is an integer variable. Important: we refer here to variables of the constraint model."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a711898a",
   "metadata": {},
   "source": [
    "Although this variant can be reformulated as a ternary extensional constraint, it is often used when modeling."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f91abe17",
   "metadata": {},
   "source": [
    "First of all, we need to remove everything that has been introduced so far."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "14c9880c",
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()  # to clear previously posted variables and constraints"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "db269443",
   "metadata": {},
   "source": [
    "We introduce a two-dimensional array $x$ of $3 \\times 2$ integers, and three stand-alone variables $i$, $j$ and $v$ that will play the role of indexes and value."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "a7425f9a",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = [\n",
    "     [2, 1],\n",
    "     [0, 1],\n",
    "     [3, 2]\n",
    "    ]\n",
    "i = Var(range(3))\n",
    "j = Var(range(2))\n",
    "v = Var(range(4))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "496c7da1",
   "metadata": {},
   "source": [
    "One may imagine to simply post the constraint *ElementMatrix*, as follows:"
   ]
  },
  {
   "cell_type": "raw",
   "id": "5630161f",
   "metadata": {
    "raw_mimetype": "text/x-python"
   },
   "source": [
    "satisfy(\n",
    "    x[i][j] == v\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f77af120",
   "metadata": {},
   "source": [
    "However, this is invalid (an error occurs) because it is not possible to use a special object (here, an object Var) as an index of a list of integers in Python. We need to transform the list of integers into a more specific list with the function *cp_array()*. So we write: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "6a6c61a0",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = cp_array(x)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5d018e25",
   "metadata": {},
   "source": [
    "Now, we can safely write:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "f380459c",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    x[i][j] == v\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "99259a44",
   "metadata": {},
   "source": [
    "We can call the function *solve()*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "6d69a433",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "0 0 2\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(value(i), value(j), value(v))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "83a594f0",
   "metadata": {},
   "source": [
    "It works! The good news is that when the data is loaded from a file (which is the usual case), all lists of integers have this specific type of list (returned by *cp_array()*), and so, it is very rare to need to call this function explicitly."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "89df3f75",
   "metadata": {},
   "source": [
    "If ever we want to count the number of solutions, we can proceed as follows. Note how the named parameter *sol* of *values()* is used to indicate the index of a solution."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "00b6ab12",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: (0,0,2) \n",
      "Solution 2: (0,1,1) \n",
      "Solution 3: (1,1,1) \n",
      "Solution 4: (1,0,0) \n",
      "Solution 5: (2,0,3) \n",
      "Solution 6: (2,1,2) \n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    for k in range(n_solutions()):\n",
    "        print(f\"Solution {k+1}: ({value(i, sol=k)},{value(j, sol=k)},{value(v, sol=k)}) \")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8852b3de",
   "metadata": {},
   "source": [
    "Although this is not the most efficient way of doing that, an alternative is to iteratively add a constraint that forbids the last found solution and to call *solve()*. This way, after each solution, a new instance is generated and the solver is loaded (in the future, we plan to be able to let the solver alive). Hence, we can enumerate all solutions (supports) of the constraint as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "31e47d58",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Supports are:\n",
      "  (0,0,2)\n",
      "  (0,1,1)\n",
      "  (1,0,0)\n",
      "  (2,0,3)\n",
      "  (1,1,1)\n",
      "  (2,1,2)\n"
     ]
    }
   ],
   "source": [
    "print(\"Supports are:\")\n",
    "while solve() is SAT:\n",
    "    print(f\"  ({value(i)},{value(j)},{value(v)})\")\n",
    "    satisfy(\n",
    "        cp_array(i,j,v) != (value(i),value(j),value(v))\n",
    "    )"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a9aa033d",
   "metadata": {},
   "source": [
    "A first remark is that once the six supports of the constraint have been computed, one can post a ternary constraint *Extension* instead of a constraint *ElementMatrix*, as follows: "
   ]
  },
  {
   "cell_type": "raw",
   "id": "09e7cb8c",
   "metadata": {
    "raw_mimetype": "text/x-python"
   },
   "source": [
    "satisfy(\n",
    "    (i,j,v) in {(0,0,2),(0,1,1),(1,0,0),(1,1,1),(2,0,3),(2,1,2)}\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "10aceb8f",
   "metadata": {},
   "source": [
    "A second remark is that we have used again the function *cp_array()*, this time to build a specific list of variables. If we do not call it, and simply write $(i,j,v)$ or $[i,j,v]$, an error will occur. However, most of the times, we directy use introduced arrays (or sub-arrays) of the model, and they have the right type of list, and so, it is very rare to need to call *cp_array()* explicitly.   "
   ]
  }
 ],
 "metadata": {
  "celltoolbar": "Raw Cell Format",
  "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
}