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.

Â