\n", " \n", "\n", "Figure 1: A Sudoku puzzle.\n", "
\n", "\n", "First, we will go through a brief tutorial on how to encode a problem using SAT. Encoding a problem with SAT typically involves answering two questions:\n", "\n", "1. What are the propositional symbols?\n", "2. How can we write down propositional sentences that reflect the constraints that the problem places on those propositional symbols?\n", "\n", "Let's take a second and think about these two questions for a Sudoku puzzle. A propositional formula should be equivalent to a Sudoku puzzle in the sense that every satisfying assignment corresponds to a solution to the Sudoku puzzle, and vice versa. How do we create this one-to-one mapping?\n", "\n", "There are many ways of translating a Sudoku puzzle into a SAT problem. Here is one example. To answer question #1, let’s create nine propositional symbols for each cell \$(i,j)\$, one for each integer 1 through 9 that might be at that location. In other words there will be 729 propositional symbols – there are 81 cells, and each of them can have one of nine integer values. To refer to these symbols we’ll use the notation \$v_{x, (i, j)}\$, which is the propositional symbol that represents that integer \$x\$ is placed in location \$(i,j)\$. It is true if \$x\$ is in location \$(i,j)\$ – in other words, \$v_{x,(i,j)}=true\$ if and only if symbol \$x\$ is in cell \$(i,j)\$. Thus, for example, in Figure 1, \$v_{5, (0, 0)}=true\$ and \$v_{1, (0, 0)}=false\$.\n", "\n", "Next, how do we represent these propositional symbols in a SAT solver? We create two mappings: in the example above, we use \$v_{x,(i, j)}\$ to represent the propositional symbol corresponding to Sudoku integer value \$x\$ and location \$(i, j)\$; however, in an actual Python implementation clauses are written in integers (remember we call ``.add_clause([-1, 2])`` to add clause \$(\\neg P_1 \\vee P_2)\$. Therefore, we need a mechanism to keep track of the relations between variable integers in the SAT solver and propositional symbols associated with each cell and each Sudoku integer. We thus create two mappings, one from a propositional symbol representing Sudoku integer value \$x\$ and cell \$(i, j)\$ to a variable integer in the SAT solver, and the other from the variable integer in SAT solver back to the Sudoku integer value \$x\$ and cell \$(i, j)\$. In this way, we are able to keep track of what each variable integer in the solver means. We do this in the following code snippet:\n" ] }, { "cell_type": "code", "metadata": { "id": "yPj9_I4oWYtQ", "colab_type": "code", "colab": {} }, "source": [ "n = 9 # there are 9 symbols, thus 9 rows/columns\n", "\n", "# we create a mapping from propositional symbol v_{x,(i, j)}\n", "# to variables indices in SAT solver.\n", "varmap = dict()\n", "# we also store the reverse mapping from variables \n", "# indices in SAT solver to propositional symbol v_{x,(i, j)}\n", "# so that we can later visualize the solution.\n", "mapback = dict()\n", "\n", "idx = 1\n", "for i in range(n):\n", " for j in range(n):\n", " for x in range(1, n+1):\n", " varmap[(i, j, x)] = idx\n", " mapback[idx] = (i, j, x)\n", " idx += 1" ], "execution_count": 0, "outputs": [] }, { "cell_type": "markdown", "metadata": { "id": "j5fF_3TIffSO", "colab_type": "text" }, "source": [ "Let's do an example to have a better grasp of the mapping:" ] }, { "cell_type": "code", "metadata": { "id": "j_3B9gBxfmK_", "colab_type": "code", "outputId": "e5656452-5109-4685-8e52-5fc958d68155", "colab": { "base_uri": "https://localhost:8080/", "height": 54 } }, "source": [ "print(\"propositional symbol representing Sudoku integer value 7 at position (3, 4) is *{}th* variable in the SAT solver.\".format(varmap[(3,4,7)]))\n", "i, j, x = mapback\n", "print(\"314th variable in SAT solver is propositional symbol representing Sudoku integer value *{}* at position *({}, {})*\".format(i, j, x))" ], "execution_count": 0, "outputs": [ { "output_type": "stream", "text": [ "propositional symbol representing Sudoku integer value 7 at position (3, 4) is *286th* variable in the SAT solver.\n", "314th variable in SAT solver is propositional symbol representing Sudoku integer value *3* at position *(7, 8)*\n" ], "name": "stdout" } ] }, { "cell_type": "markdown", "metadata": { "id": "TYz_SnUkaq5f", "colab_type": "text" }, "source": [ "The second question is to formulate propositional sentences that represent the constraints that define a legal solution to a Sudoku problem so that the resulting SAT assignment corresponds to a Sudoku solution. The nature of Sudoku problems suggests thinking about this as three categories of constraints: row constraints, column constraints, and block constraints. In each row, in each column, and in each block, each symbol only shows up once. Here is how we can write up some code to represent this as a sentence in CNF." ] }, { "cell_type": "code", "metadata": { "id": "NEvDSqXUae7s", "colab_type": "code", "colab": {} }, "source": [ "import itertools\n", "\n", "\"\"\"creates row constraints.\n", "\n", " Keyword arguments:\n", " solver -- to which SAT solver we are adding constraints\n", " ivarmap -- the mapping from a boolean variable that represents a specific\n", " symbol and a specific location to an integer in clause\n", " n -- the size of the Sudoku board\n", " \"\"\"\n", "def row(solver, ivarmap, n):\n", " for x in range(1, n+1):\n", " for i in range(n):\n", " in_row = [ivarmap[(i,j,x)] for j in range(n)]\n", " # these are mutually exclusive constraints saying that\n", " # each symbol appears *at most* once in the row.\n", " for (c1, c2) in itertools.combinations(in_row, 2):\n", " # no any pairs of variables can be true simultaneously\n", " solver.add_clause([-c1, -c2])\n", " # this is an at least 1 constraint saying that there\n", " # has to be one symbol that appears in the row\n", " solver.add_clause(in_row)\n", "\n", "\"\"\"creates column constraints.\n", "\n", " Keyword arguments:\n", " solver -- to which SAT solver we are adding constraints\n", " ivarmap -- the mapping from a boolean variable that represents a specific\n", " symbol and a specific location to an integer in clause\n", " n -- the size of the Sudoku board\n", " \"\"\"\n", "def column(solver, ivarmap, n):\n", " for x in range(1, n+1):\n", " for j in range(n):\n", " in_column = [ivarmap[(i,j,x)] for i in range(n)]\n", " for (c1, c2) in itertools.combinations(in_column, 2):\n", " solver.add_clause([-c1, -c2])\n", " solver.add_clause(in_column)\n", "\n", "\"\"\"creates block constraints.\n", "\n", " Keyword arguments:\n", " solver -- to which SAT solver we are adding constraints\n", " ivarmap -- the mapping from a boolean variable that represents a specific\n", " symbol and a specific location to an integer in clause\n", " n -- the size of the Sudoku board\n", " \"\"\"\n", "def square(solver, ivarmap, n):\n", " sqrt_n = np.sqrt(n)\n", " assert sqrt_n == int(sqrt_n)\n", " sqrt_n = int(sqrt_n)\n", " for x in range(1, n+1):\n", " for i in range(0, n, sqrt_n):\n", " for j in range(0, n, sqrt_n):\n", " in_square = [ivarmap[(p,q,x)] for p in range(i, i+sqrt_n) for q in range(j, j+sqrt_n)]\n", " for (c1, c2) in itertools.combinations(in_square, 2):\n", " solver.add_clause([-c1, -c2])\n", " solver.add_clause(in_square)" ], "execution_count": 0, "outputs": [] }, { "cell_type": "code", "metadata": { "id": "NDa3YoNVUYLs", "colab_type": "code", "outputId": "d1e00d16-b7c7-41a7-f37e-9ad5d1feb641", "colab": { "base_uri": "https://localhost:8080/", "height": 182 } }, "source": [ "import numpy as np # we'll need numpy's 2-dim array\n", "\n", "s = Minisat22()\n", "\n", "# then create the constraints\n", "row(s, varmap, n)\n", "column(s, varmap, n)\n", "square(s, varmap, n)\n", "\n", "\"\"\"print the truth assignment returned by SAT solver to a Sudoku assignment\n", "\n", " Keyword arguments:\n", " imodel -- the truth assignment to be decoded to a Sudoku assignment\n", " ivarmap -- the mapping from an integer in SAT solver to a boolean variable \n", " that represents a specific symbol and a specific location\n", " \"\"\"\n", "def print_sudoku(imodel, imapback):\n", " sol = np.zeros((n,n)).astype(int)\n", " for i in range(len(imodel)):\n", " if imodel[i] > 0:\n", " x, y, val = mapback[i+1]\n", " sol[x, y] = val\n", " print(sol)\n", "\n", "s.solve()\n", "model = s.get_model()\n", "print_sudoku(model, mapback)" ], "execution_count": 0, "outputs": [ { "output_type": "stream", "text": [ "[[0 0 0 0 0 0 0 0 9]\n", " [0 0 0 0 0 9 0 0 0]\n", " [0 0 9 0 0 0 0 0 0]\n", " [0 0 0 0 0 0 0 9 0]\n", " [0 0 0 0 9 0 0 0 0]\n", " [0 9 0 0 0 0 0 0 0]\n", " [0 0 0 0 0 0 9 0 0]\n", " [0 0 0 9 0 0 0 0 0]\n", " [9 0 0 0 0 0 0 0 0]]\n" ], "name": "stdout" } ] }, { "cell_type": "markdown", "metadata": { "id": "gXJNPGxkC3Bo", "colab_type": "text" }, "source": [ "As you might have noticed, the solution returned by the SAT solver is not correct yet. While our formulation ensures that each integer occurs only once in every row, column, and block it does not require that every cell be assigned an integer. The zeros in the Sudoku board above are the cells that no symbols were assigned to. Therefore, we need to force each cell to be assigned exactly one integer. We add that by the following:" ] }, { "cell_type": "code", "metadata": { "id": "uhoqlVn1EVsT", "colab_type": "code", "outputId": "ae49c5bb-5760-4b90-b74a-cf4be8412311", "colab": { "base_uri": "https://localhost:8080/", "height": 182 } }, "source": [ "\"\"\"creates cell constraints.\n", "\n", " Keyword arguments:\n", " solver -- to which SAT solver we are adding constraints\n", " ivarmap -- the mapping from a boolean variable that represents a specific\n", " symbol and a specific location to an integer in clause\n", " n -- the size of the Sudoku board\n", " \"\"\"\n", "def cell(solver, ivarmap):\n", " for i in range(n):\n", " for j in range(n):\n", " in_cell = [ivarmap[(i,j,x)] for x in range(1, n+1)]\n", " for (c1, c2) in itertools.combinations(in_cell, 2):\n", " solver.add_clause([-c1, -c2])\n", " solver.add_clause(in_cell)\n", "\n", "cell(s, varmap)\n", "\n", "s.solve()\n", "model = s.get_model()\n", "print_sudoku(model, mapback)" ], "execution_count": 0, "outputs": [ { "output_type": "stream", "text": [ "[[1 5 9 2 6 8 4 3 7]\n", " [2 4 8 1 7 3 5 9 6]\n", " [3 7 6 4 9 5 1 8 2]\n", " [4 2 1 3 8 6 7 5 9]\n", " [7 6 3 5 1 9 2 4 8]\n", " [8 9 5 7 4 2 6 1 3]\n", " [5 1 2 8 3 7 9 6 4]\n", " [6 3 4 9 2 1 8 7 5]\n", " [9 8 7 6 5 4 3 2 1]]\n" ], "name": "stdout" } ] }, { "cell_type": "markdown", "metadata": { "id": "ke0l76NgFAZ0", "colab_type": "text" }, "source": [ "We’re done! We now have working code for taking arbitrary Sudoku problems and converting them in propositional satisfiability problems. You can learn more about this in the following [article](https://codingnest.com/modern-sat-solvers-fast-neat-underused-part-1-of-n/)." ] }, { "cell_type": "markdown", "metadata": { "id": "cmIvgdtcGDgH", "colab_type": "text" }, "source": [ "### A Scheduling Problem\n", "\n", "Now that you have gained experience with translating a problem into a propositional formula, let’s apply this to a scheduling problem (based on a now rather dated 170 year-old problem known as [Kirkman's schoolgirl problem](https://en.wikipedia.org/wiki/Kirkman%27s_schoolgirl_problem)):\n", "\n", "> Fifteen students in a school walk out in groups of size three for seven days in succession: it is required to arrange them daily so that no two shall walk twice in a group.\n", "\n", "To encode this problem, let's again follow the questions we listed above: what are the propositional symbols, and what are the constraints on them. We will help you answer the first question, and you'll work on the second one. Let's create a propositional symbol representing and a propositional symbol representing . The variable maps are as follows:" ] }, { "cell_type": "code", "metadata": { "id": "_Df21OUYTG5p", "colab_type": "code", "colab": {} }, "source": [ "n_student = 15\n", "n_day = (n_student-1)//2\n", "n_group = n_student//3\n", "\n", "idx2 = 1\n", "varmap2 = dict()\n", "mapback2 = dict()\n", "\n", "# if student 𝑖 walks in group 𝑔 on day 𝑑\n", "for d in range(n_day):\n", " for g in range(n_group):\n", " for i in range(n_student):\n", " varmap2[(d, g, i)] = idx2\n", " mapback2[idx2] = (d, g, i)\n", " idx2 += 1\n", "\n", "# if student pair (𝑖,𝑗) walks in group 𝑔 on day 𝑑\n", "for d in range(n_day):\n", " for g in range(n_group):\n", " for (i, j) in itertools.combinations(range(n_student), 2):\n", " varmap2[(d, g, (i, j))] = idx2\n", " mapback2[idx2] = (d, g, (i, j))\n", " idx2 += 1\n", "\n", "# to link these two propositional symbols, we add the following constraints:\n", "# if student pair (𝑖,𝑗) walks in group 𝑔 on day 𝑑, then student 𝑖 walks in \n", "# group 𝑔 on day 𝑑 and student 𝑗 walks in group 𝑔 on day 𝑑; if student 𝑖 and \n", "# student 𝑗 walk in group 𝑔 on day 𝑑, then student pair (𝑖,𝑗) walks in group \n", "# 𝑔 on day 𝑑\n", "def link_symbols(solver, ivarmap):\n", " for d in range(n_day):\n", " for g in range(n_group):\n", " for (i, j) in itertools.combinations(range(n_student), 2):\n", " solver.add_clause([-ivarmap[(d, g, i)], -ivarmap[(d, g, j)], ivarmap[(d, g, (i, j))]])\n", " solver.add_clause([-ivarmap[(d, g, (i, j))], ivarmap[(d, g, i)]])\n", " solver.add_clause([-ivarmap[(d, g, (i, j))], ivarmap[(d, g, j)]])" ], "execution_count": 0, "outputs": [] }, { "cell_type": "markdown", "metadata": { "id": "M8Zki0qTTJ-u", "colab_type": "text" }, "source": [ "**Exercise 4A (report in PDF)** How many propositional symbols does this encoding generate? Explain your answer." ] }, { "cell_type": "markdown", "metadata": { "id": "ILfR4cMZZgRb", "colab_type": "text" }, "source": [ "For the two exercises below, please export this Jupyter notebook to a .py file. If you are working on Google Colab, you can download the .py file by doing the following: \n", "\n", " \n", "\n", "\n", "\n", "\n", "\n" ] }, { "cell_type": "markdown", "metadata": { "id": "Y9DQJbX9SLIB", "colab_type": "text" }, "source": [ "**Exercise 4B (report in .py file)** Please complete the encoding by coming up with the constraints. \n", "\n", "*HINT:* First, write your constraints out in English. Then, convert them into the clauses that will be used to compute a solution, similar to what was done for Sudoku." ] }, { "cell_type": "code", "metadata": { "id": "H8sNtFL2TUEx", "colab_type": "code", "colab": {} }, "source": [ "# def sol_4B():\n", " # please define such a function in your .py file, as we'll be calling it to check your answer\n", " # you should return whatever it is in the .get_model()\n", " # for example:\n", " # s = Minisat22()\n", " # ... do whatever ...\n", " # return s.get_model()" ], "execution_count": 0, "outputs": [] }, { "cell_type": "markdown", "metadata": { "id": "Ud48cqp8SLL1", "colab_type": "text" }, "source": [ "**Exercise 4C (report in .py file)** Can you use the SAT solver to come up with ten different schedules? \n", "\n", "*HINT:* There are many ways to do this. Here is one: think about how to prevent the solver from returning a truth assignment? More specifically, what constraints can you add to prevent that?" ] }, { "cell_type": "code", "metadata": { "id": "kyWsLvpWTTf_", "colab_type": "code", "colab": {} }, "source": [ "# def sol_4C():\n", " # please define such a function in your .py file, as we'll be calling it to check your answer\n", " # please return the 10 models you compute in a list\n", " # for example:\n", " # res = []\n", " # for _ in range(10):\n", " # # add constraints to your solver\n", " # s.add_clause(...)\n", " # # append solutions\n", " # res.append(s.get_model())\n", " # return res" ], "execution_count": 0, "outputs": [] }, { "cell_type": "markdown", "metadata": { "id": "Mp7KfYmnp_Uu", "colab_type": "text" }, "source": [ "### Some final notes:\n", "\n", "* As the Boolean Satisfiability problem is an NP-hard problem, it is too easy to run into a case where it takes too long to get a solution. If you don't get an answer for a minute, that often means your constraints are too hard. A rule of thumb is to aim for making clauses with fewer literals!\n", "* Use print() as much as you can! If you're stuck, use print() to see what truth assignment the SAT solver returns, inspect what constraints are missing, and then you can add clauses according to those missed constraints (just like we did for the Sudoku problem). Remeber, we have defined a mapping called ``mapback2``; you can use that to translate from a propositional symbol to which student walk in which group on which day." ] } ] }