{ "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 }