0:13
Recall that there is a huge gap between theory and practice of SAT solving.
Namely, currently we did not know how to prove that SAT can be solved in less
than two the n steps.
Namely, we have now example of an algorithm with the running time,
polynomial in the size of the formula times 1.99, for example,
to the n, where n is the number of variables of the input formula.
It is on one hand.
On the other hand we have state of the art SAT-solvers that can
handle instances that arise in practice that contain thousands and
even millions of variables in less than one second.
This suggests the following way of solving hard combinatorial problems in practice.
First you might want to reduce your problem to a satisfiability problem.
The structure of the satisfiability problem allows to do this very naturally
for many problems arising in practice.
We will see this on an example of solving Sudoku puzzle.
Then just use one of the efficient programs,
efficient SAT solvers that are already implemented.
There are many of them, and as I said they are very efficient.
Let me now recall you what a Sudoku puzzle is.
So in this case we are given a 9 x 9 grid which is partially filled by
digits from 1 to 9.
And our goal is to fill all the vacant places with digits so
that each row and each column and each of nine 3 x
3 blocks contain all the digits from 1 to 9.
This is an example of such a puzzle and
this is a solution that we're looking for in this case.
So now that for example in this row we have all digits from 1 to 9 and
also in this column and also in all of these nine 3 x 3 blocks.
2:12
So given a Sudoku puzzle we are going to construct
a satisfiable CNF formula such that from its satisfying
assignment we can construct the solution for the initial puzzle.
For this we are going to use the following Boolean variables.
There will be 9 x 9 x 9 of them.
Namely for each possibly values of i, j, and k, where i, j, and
k are at least 1 and at most 9, the variable xijk = 1 or
is equal to true, if the cell [i,j] contains the digit k.
Okay?
So these are Boolean variables.
There are 9 x 9 x 9 of them, which is roughly 700.
In our reduction, we will need a few times the several technical thing.
Assume that we have a few literals and we need to state
a formula which expresses the fact that exactly one of this literals is true.
We show here how to do this for three literals but
it generalizes easily for arbitrary number of literals.
So assume that we have three literals and
we want to express the fact in a CNF formula that exactly one of them is true.
So first we write down a clause that says then at least one of them is true,
this says l1 or l2 or l3.
Then we need to say also the constraints,
the value of these variables to satisfy the following property.
At most one of them is true, namely,
we need to forbid any two of them to have value 1 simultaneously.
We do this by adding a bunch of clauses of length two, namely for
any two different literals from our set,
we add two clause containing negations of these two literals.
For example, this one the first clause says
that it is not possible to assign the value 1 to l1 and l2 simulationously.
The second one says that we should not assign the value 1 to the first and
the third literal.
And, finally, the last one says that we should not assign the value 1 to
the second and the third literal..
So, finally, when we write down such a formula, then in any satisfying
assignment to this formula exactly one of l1, and l2 and l3 is true.
And also, it generalizes easily to any number of literals.
So we first right down the long clause containing all the literals and
then so that will contain k literals.
And then we write down roughly k squared literals
namely k choose 2 clauses that contain all pairs of negated literals.
We now write down the corresponding constraints.
First of all, for every values of i and j from 1 to 9, we state that in the cell [i,
j], there is exactly one digit, so it looks as follows.
So, this is a cell [i, j] in our grid and
we say that exactly one of the variables xij1, xij2 and so
on, xij9 should be assigned the value true.
So, if xij, for example, if xij4 is equal to true,
this means that we are going to put the digit 4 into this cell.
Then we need to state that for each values of k and
i, the row i contains exactly one occurrence of k.
This is done as follows.
We state that for each i and k, exactly one of the following variables is true.
So it is either xi1k or xi2k.
So this corresponds to the fact that either the first column in
the ith row contains k's or the second column or the last column.
Namely, if this is the ith row either this cell contains k or
this cell contains k and so on, the last cell contains k.
Then we do the same for column j and namely for each values of k and
j we state the fact that the column j contains exactly one occurrence of k.
6:36
We then need also to state that each of nine 3
x 3 blocks contains one occurrence of the digit k.
Again, we use the corresponding nine variables to say that
exactly one of them is equal to true.
Finally the last type of constraint is that when some cell is already filled.
If we have an instance where the cell [i,
j] already contains the digit k, we then we need just one clause
stating that the corresponding variable must be equal to true.
We know that it is already true, so we just add a single unit clause.
So the resulting formula contains about 2 to the 700 variables, so
the search space of all
possible candidate solutions in this case contains roughly ten to the two hundred.
So this is a huge search space.
It is certainly not possible for modern computers
to go through all possible candidates for a solution in this case.
At the same time, modern SAT-solvers solve the results in formula in blink of an eye.
We will see now.
We are going to use a mini SAT-solver for solving our Sudoku puzzle.
7:55
Before writing down the reduction let me show you the input format for
this SAT-solver.
So the formula is given in the following symbol format.
The first line here shows that our formula has 2 variables and 3 clauses.
Then each of the following three lines define a clause.
The first clause contains two variables, x1 and x2.
The second clause contains the variable x1 and the negation of the variable x2, so
minus x2 means the negation of the second variable.
Finally as the last clause contains two variables,
the negation of x1 and the negation of x2 okay?
So now let's call minisat on this formula, so
it reports immediately that it is satisfiable.
Now let's make it unsatisfiable, so for this we add the false clause.
-1, 2, 0, okay.
9:03
Yeah, in this case, the formula is unsatisfiable of course.
Now finally let me show you the code of an actual reduction that produces the CNF
formulas and then calls in minisat solver and then reads the solution for
a given Sudoku puzzle from a satisfying assignment to these formula.
So this is a simple code in Python, this gives the initial
Sudoku puzzle and then we create a list of clauses.
Then we just use variable digits which contains all the digits from 1 to 9.
The following method just returns a unique integer number for every variable.
We need this in order to give a formula to a minisat solver.
Then we have a method which, given a list of literals writes down clauses
that express the fact that exactly one of these literals is equal to true.
Namely, we first add a clause that contains all the literals
in the list literals, then for all pairs of literals
we add a clause containing two negated literals from this list.
As we've discussed already this expresses the fact that exactly one of them
is equal to true.
We then start writing down clauses expressing that each cell contains
exactly one digit.
Namely, for all pairs of digits we write down a clause stating that at least,
for all pairs of i and j, we write down the clause saying
that the cell [i, j] contains exactly one digit.
So the corresponding variable xijk is equal to 1 for exactly one value of k.
Then we say that k appears exactly once in row i.
For this we consider all possible values of i and
k and state that exactly one of the variables i,
j, k is equal to true for all possible values of j.
Then we say the same for columns, and then we say the same for blocks.
Namely, we can see that all possible starting position of blocks 1, 4, and 7.
And then for each such block and for each k we state
11:42
one corresponding variable.
Finally, we write down all the clauses.
Namely, we open a file, tmp.cnf,
in the first line we write, p cnf, followed by the number of variables.
In our case it is roughly 1,000 and then the number of clauses.
Then for each clause which is currently in our list of clauses we first append 0 to
satisfy the format which is accepted by the mini-SAT,
and then we just write down this clause.
Then we call the MiniSAT SAT-solver,
give it the formula tmp.cnf and also indicate the file tmp.sat,
where it will write down the satisfying assignment, okay?
Then we open the satisfying assignment file and read the first line.
If it is UNSAT, we just report that the formula is unsatisfiable.
If the first line is SAT, we know that the formula is satisfiable and
we know that then the second line will be followed by a satisfying assignment.
12:51
At this line we read the corresponding satisfying assignment and
then we parse it.
We just see that if
the corresponding variable in this assignment we print it, okay?
So and this is basically all, this completes all reduction.
So let's see what happens.
If we call this Python script
it will immediately find an answer.
So this is an answer for our initial puzzle.
Let me also make a small sanity check.
Let me tweak a little bit this puzzle.
Let me put 5 here.
Then the corresponding puzzle will be for
sure unsatisfiable just because now the first line contains
two occurrences of 5 so it is not possible to complete this puzzle.
Okay, now let me call it once again so in this case, the corresponding
formula is unsatisfiable and our scripts reports that there is no solution.
As you can see, it works in just the blink of an eye.
And you can feed your favorite Sudoku puzzle into this script to see how
fastly the mini SAT-solver will solve this puzzle.
Alexander S. KulikovVisiting Professor
Michael LevinLecturer
Daniel M KaneAssistant Professor
Neil RhodesAdjunct Faculty
