{
"nbformat": 4,
"nbformat_minor": 0,
"metadata": {
"colab": {
"name": "SAT_exercise.ipynb",
"provenance": [],
"collapsed_sections": []
},
"kernelspec": {
"name": "python3",
"display_name": "Python 3"
}
},
"cells": [
{
"cell_type": "markdown",
"metadata": {
"id": "3YkhTd5SHieg",
"colab_type": "text"
},
"source": [
"### Experimenting with SAT solvers: an introduction"
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "-9ztEWuqIoI_",
"colab_type": "text"
},
"source": [
"A SAT solver takes as input a propositional formula in conjunctive normal form (CNF) and returns one of two answers: SAT, if the formula is satisfiable, or UNSAT, if it is unsatisfiable. If the answer is SAT the solver will furthermore return a satisfying assignment. SAT is an example of an NP-complete problem (in, fact it was the first problem class discovered to be NP-complete!), and thus the best algorithms require time exponential in the number of propositional symbols in the worst case. Quite surprisingly, SAT solvers can nonetheless produce an answer for a formula with over a million variables in seconds. As a result SAT solvers have become the \"go to\" tool for solving NP-hard problems in the absence of known problem-specific heuristics, and they have made a large impact on the real world in areas such as hardware design verification, scheduling problems, and automatic theorem proving.\n",
"\n",
"Using a SAT solver on a given problem requires converting the problem into an equivalent propositional satisfiability question, solving the SAT question, and then converting the answer back to the terms in which the original problem was posed. The goal of this exercise is to give you some experience with SAT solvers, both in encoding a problem as a SAT question, and to get a sense of its efficiency. You can find further information about SAT solvers in the following [presentation](https://courses.cs.washington.edu/courses/csep573/11wi/lectures/ashish-satsolvers.pdf)."
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "Z9kLCGviG3PQ",
"colab_type": "text"
},
"source": [
"### Setting up a SAT solver in Python"
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "LNkxV24SG7-E",
"colab_type": "text"
},
"source": [
"In this exercise, we'll use [PySAT](https://github.com/pysathq/pysat). Most modern solvers are written in C++ in order to have the highest possible efficiency; for ease of use, we'll use a Python binding. To install it on your local machine run the following:"
]
},
{
"cell_type": "code",
"metadata": {
"id": "42iKuN7FMETb",
"colab_type": "code",
"colab": {}
},
"source": [
"!pip install python-sat"
],
"execution_count": 0,
"outputs": []
},
{
"cell_type": "markdown",
"metadata": {
"id": "xAY-V3QWj_7D",
"colab_type": "text"
},
"source": [
"Or, if you run into a Python version issue with the command above, try to install it with pip3:"
]
},
{
"cell_type": "code",
"metadata": {
"id": "4SwVUUcXj-yA",
"colab_type": "code",
"outputId": "17f1e3db-5cdb-4867-f47b-af1919749deb",
"colab": {
"base_uri": "https://localhost:8080/",
"height": 54
}
},
"source": [
"!pip3 install python-sat"
],
"execution_count": 0,
"outputs": [
{
"output_type": "stream",
"text": [
"Requirement already satisfied: python-sat in /usr/local/lib/python3.6/dist-packages (0.1.5.dev6)\n",
"Requirement already satisfied: six in /usr/local/lib/python3.6/dist-packages (from python-sat) (1.12.0)\n"
],
"name": "stdout"
}
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "L8c3KhO4M1Q4",
"colab_type": "text"
},
"source": [
"Now we are ready to import it. PySAT binds to many popular SAT solvers. In this assignment, we'll be using [MiniSAT](http://minisat.se/), because it is a very simple yet efficient solver, and many other modern solvers have built on top of it. If you read the C++ source code, it is only *a few* hundreds of lines."
]
},
{
"cell_type": "code",
"metadata": {
"id": "6N7JpBEXMzdY",
"colab_type": "code",
"outputId": "e381252a-9ee5-479d-b537-a4d96b229151",
"colab": {
"base_uri": "https://localhost:8080/",
"height": 54
}
},
"source": [
"from pysat.solvers import Minisat22\n",
"\n",
"solver = Minisat22()\n",
"solver.add_clause([-1, 2])\n",
"solver.add_clause([-2, 3])\n",
"print(solver.solve())\n",
"print(solver.get_model())"
],
"execution_count": 0,
"outputs": [
{
"output_type": "stream",
"text": [
"True\n",
"[-1, -2, -3]\n"
],
"name": "stdout"
}
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "20tHIzMFUZTU",
"colab_type": "text"
},
"source": [
"In this example, we first initialized a solver object whose backend is MiniSAT and added two clauses. Recall from lecture that a literal is either a propositional symbol or its negation, and a clause is a disjunction of literals. Here, literals are represented by integers; a postive integer represents an unnegated propositional symbol, and a negative integer represents the negation of a propositional symbol. Thus, for example, the integer +2 could be thought of as representing a propositional symbol $P_2$ and the integer -1 as representing $\\neg P_1$.\n",
"\n",
"Next, a clause is represented as a list of literals (positive and negative integers). Thus for example, ``solver.add_clause([-1, 2])`` adds the clause equivalent to $(\\neg P_1 \\vee P_2)$. Note that rather than referring to the propositional symbols as symbols such as $P_2$, we’ll typically use the integer 2 itself to refer to the corresponding propositional symbol. Note that you don't need to “declare” the propositional variables with PySAT; simply adding a clause that uses a particular integer for the first time is sufficient for the system to understand that the integer represents a new propositional symbol. The set of clauses added in this fashion are taken as being conjoined together, thereby defining the propositional sentence to be tested by the SAT solver. Checking the satisfiability of the created CNF formula is done using ``solver.solve()``; if it is satisfiable, ``solver.get_model()`` returns a truth assignment that satisfies the formula. We'll be using the ``.add_clause()``, ``.solve()``, and ``.get_model()`` methods a lot later in this exercise."
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "AzjnxgtSvjbV",
"colab_type": "text"
},
"source": [
"### A tutorial: Solving a Sudoku puzzle via SAT technology"
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "ljQ1FnTBvrWQ",
"colab_type": "text"
},
"source": [
"\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[314]\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."
]
}
]
}