{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "670f8144",
   "metadata": {},
   "source": [
    "# Constraint *Circuit*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b50b3e93",
   "metadata": {},
   "source": [
    "The constraint *Circuit* ensures that the values taken by the variables of a specified list $x$ forms a circuit, with the assumption that each pair $(i,x[i])$ represents an arc.\n",
    "It is also possible to indicates that the circuit must be of a given size (greater than or equal to $2$)."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "827d522d",
   "metadata": {},
   "source": [
    "The context is when problems involve graphs that are defined with integer variables (encoding called ``successors variables''). Graph-based constraints, like *Circuit*, involve then a main list of variables $x$.\n",
    "The assumption is that each pair $(i,x[i])$ represents an arc (or edge) of the graph to be built; if $x[i]=j$, then it means that the successor of node $i$ is node $j$.\n",
    "Note that a loop, or self-loop, corresponds to a variable $x[i]$ such that $x[i]=i$. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7851a363",
   "metadata": {},
   "source": [
    "Below, we give several illustrations corresponding to representative use cases of the constraint *Circuit*."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "201715a5",
   "metadata": {},
   "source": [
    "## Case 1: Circuit of Any Size"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "355b76ab",
   "metadata": {},
   "source": [
    "We start with a case of *Circuit* without any form of restriction about the size. However, in order to be relevant, note that a circuit cannot be of size 0 (and so, its size is at least 2)."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "57d760cf",
   "metadata": {},
   "source": [
    "To see how this constraint works, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "d9afb2b5",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "607ade26",
   "metadata": {},
   "source": [
    "For our illustration, we introduce an array $x$ of 6 variables, each one with {0,1,2,3,4,5} as domain. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "cf477c3f",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=6, dom=range(6))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e54efa07",
   "metadata": {},
   "source": [
    "We can display (the structure of) the array as well as the domain of the first variable."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "3243d0ab",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Array of variable x:  [x[0], x[1], x[2], x[3], x[4], x[5]]\n",
      "Domain of any variable:  0..5\n"
     ]
    }
   ],
   "source": [
    "print(\"Array of variable x: \", x)\n",
    "print(\"Domain of any variable: \", x[0].dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "75e1b04c",
   "metadata": {},
   "source": [
    "We simply post a single constraint *Circuit* on the variables of $x$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "972bde92",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Circuit(x)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6d3e0eca",
   "metadata": {},
   "source": [
    "By calling the function *solve()*, we can check that the problem (actually, the single constraint) is satisfiable (SAT). We can also print the values assigned to the variables in the found solution; we can call the function *values()* that collects the values assigned (in the last found solution) to a specified list of variables."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "e25dc9c4",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 1, 2, 3, 5, 4]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "265d961c",
   "metadata": {},
   "source": [
    "One can see (actually, the output may depend on the used solver) that some loops are present. At the extreme case, the circuit is only of size 2."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ca7fb7a2",
   "metadata": {},
   "source": [
    "To avoid loops, it is possible to post unary constraints: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "ccacde77",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    x[i] != i for i in range(6) \n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "218d5b20",
   "metadata": {},
   "source": [
    "Interestingly, we can display the internal representation of the posted constraints; although a little bit technical, we can see that the information is correctly recorded (note that 'ne' stands for 'not equal')."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "facb732e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "circuit(list:x[])\n",
      "intension(function:ne(x[0],0))\n",
      "intension(function:ne(x[1],1))\n",
      "intension(function:ne(x[2],2))\n",
      "intension(function:ne(x[3],3))\n",
      "intension(function:ne(x[4],4))\n",
      "intension(function:ne(x[5],5))\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c864628c",
   "metadata": {},
   "source": [
    "The number of circuits without any loop is $5! =120$. One can enumerate the 15 first solutions as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "e88efa56",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [1, 2, 3, 4, 5, 0]\n",
      "Solution 2: [1, 2, 3, 5, 0, 4]\n",
      "Solution 3: [1, 2, 5, 4, 0, 3]\n",
      "Solution 4: [1, 2, 4, 0, 5, 3]\n",
      "Solution 5: [1, 2, 5, 0, 3, 4]\n",
      "Solution 6: [1, 2, 4, 5, 3, 0]\n",
      "Solution 7: [1, 3, 4, 2, 5, 0]\n",
      "Solution 8: [1, 3, 5, 4, 2, 0]\n",
      "Solution 9: [1, 4, 5, 2, 3, 0]\n",
      "Solution 10: [1, 4, 3, 5, 2, 0]\n",
      "Solution 11: [1, 4, 3, 0, 5, 2]\n",
      "Solution 12: [1, 5, 3, 4, 0, 2]\n",
      "Solution 13: [1, 5, 3, 0, 2, 4]\n",
      "Solution 14: [1, 5, 0, 4, 2, 3]\n",
      "Solution 15: [1, 3, 0, 5, 2, 4]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=15) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\"Solution {i+1}: {values(x, sol=i)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "398502c0",
   "metadata": {},
   "source": [
    "## Case 2: Circuit of Specified Size"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7f15705f",
   "metadata": {},
   "source": [
    "We consider now a case of *Circuit* with a specified size. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "17e509e9",
   "metadata": {},
   "source": [
    "To start, we remove the posted constraints by calling the function *unpost()* with the parameter ALL."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "3ddb58d2",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost(ALL)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "556c30d7",
   "metadata": {},
   "source": [
    "We can check that there are no more constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "ef5717cc",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "128671a7",
   "metadata": {},
   "source": [
    "We post a single constraint *Circuit* on $x$, with the restriction that the circuit must be of size 3:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "2fe15896",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Circuit(x, size=3)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6a4543c6",
   "metadata": {},
   "source": [
    "We can run the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "4f37f10c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 1, 2, 4, 5, 3]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7fb31961",
   "metadata": {},
   "source": [
    "On can compute that the number of solutions (supports) for this constraint is: ${6 \\choose 3} \\times 2 = 40$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "568a5b2e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 1, 2, 4, 5, 3]\n",
      "Solution 2: [0, 1, 2, 5, 3, 4]\n",
      "Solution 3: [0, 1, 3, 4, 2, 5]\n",
      "Solution 4: [0, 1, 4, 2, 3, 5]\n",
      "Solution 5: [0, 1, 4, 3, 5, 2]\n",
      "Solution 6: [0, 1, 5, 3, 2, 4]\n",
      "Solution 7: [0, 1, 5, 2, 4, 3]\n",
      "Solution 8: [0, 1, 3, 5, 4, 2]\n",
      "Solution 9: [0, 2, 3, 1, 4, 5]\n",
      "Solution 10: [0, 3, 1, 2, 4, 5]\n",
      "Solution 11: [0, 3, 2, 4, 1, 5]\n",
      "Solution 12: [0, 4, 2, 1, 3, 5]\n",
      "Solution 13: [0, 3, 2, 5, 4, 1]\n",
      "Solution 14: [0, 5, 2, 1, 4, 3]\n",
      "Solution 15: [0, 5, 2, 3, 1, 4]\n",
      "Solution 16: [0, 4, 2, 3, 5, 1]\n",
      "Solution 17: [0, 4, 1, 3, 2, 5]\n",
      "Solution 18: [0, 2, 4, 3, 1, 5]\n",
      "Solution 19: [0, 2, 5, 3, 4, 1]\n",
      "Solution 20: [0, 5, 1, 3, 4, 2]\n",
      "Solution 21: [1, 2, 0, 3, 4, 5]\n",
      "Solution 22: [1, 3, 2, 0, 4, 5]\n",
      "Solution 23: [1, 4, 2, 3, 0, 5]\n",
      "Solution 24: [1, 5, 2, 3, 4, 0]\n",
      "Solution 25: [2, 0, 1, 3, 4, 5]\n",
      "Solution 26: [2, 1, 3, 0, 4, 5]\n",
      "Solution 27: [2, 1, 5, 3, 4, 0]\n",
      "Solution 28: [3, 1, 0, 2, 4, 5]\n",
      "Solution 29: [5, 1, 0, 3, 4, 2]\n",
      "Solution 30: [5, 0, 2, 3, 4, 1]\n",
      "Solution 31: [5, 1, 2, 0, 4, 3]\n",
      "Solution 32: [3, 1, 2, 5, 4, 0]\n",
      "Solution 33: [3, 0, 2, 1, 4, 5]\n",
      "Solution 34: [4, 1, 2, 0, 3, 5]\n",
      "Solution 35: [3, 1, 2, 4, 0, 5]\n",
      "Solution 36: [4, 0, 2, 3, 1, 5]\n",
      "Solution 37: [4, 1, 2, 3, 5, 0]\n",
      "Solution 38: [5, 1, 2, 3, 0, 4]\n",
      "Solution 39: [2, 1, 4, 3, 0, 5]\n",
      "Solution 40: [4, 1, 0, 3, 2, 5]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\"Solution {i+1}: {values(x, sol=i)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8efb8491",
   "metadata": {},
   "source": [
    "### Variable Size"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1654b31d",
   "metadata": {},
   "source": [
    "One can record the size of the circuit in a variable."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c6ed9aa6",
   "metadata": {},
   "source": [
    "To start, we remove the posted constraint by calling the function *unpost()*:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "6e4c5a3e",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "91fa4b50",
   "metadata": {},
   "source": [
    "We introduce a variable $y$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "b60f0113",
   "metadata": {},
   "outputs": [],
   "source": [
    "y = Var(range(7))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d4d0a783",
   "metadata": {},
   "source": [
    "We post a single constraint *Circuit* on $x$, with the restriction that the circuit must be of size $y$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "e2932ead",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Circuit(x, size=y)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0ef7a826",
   "metadata": {},
   "source": [
    "We can run the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "6d16cf76",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 1, 2, 3, 5, 4] 2\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x), value(y))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5ab933d5",
   "metadata": {},
   "source": [
    "We can enumerate the 10 first solutions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "9e634476",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 1, 2, 3, 5, 4] 2\n",
      "Solution 2: [0, 1, 2, 4, 5, 3] 3\n",
      "Solution 3: [0, 1, 2, 5, 3, 4] 3\n",
      "Solution 4: [0, 1, 2, 5, 4, 3] 2\n",
      "Solution 5: [0, 1, 2, 4, 3, 5] 2\n",
      "Solution 6: [0, 1, 3, 4, 2, 5] 3\n",
      "Solution 7: [0, 1, 3, 4, 5, 2] 4\n",
      "Solution 8: [0, 1, 3, 5, 2, 4] 4\n",
      "Solution 9: [0, 1, 4, 5, 3, 2] 4\n",
      "Solution 10: [0, 1, 4, 2, 5, 3] 4\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=10) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\"Solution {i+1}: {values(x, sol=i)} {value(y, sol=i)}\")"
   ]
  }
 ],
 "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
}