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.