Sudoku SAT-Solver

Sudokus are fun to solve - but watching a machine solve them isn’t as rewarding. However, what is fun is writing programs to solve them for you. I’ve written Sudoku solvers in the past using DFS with pruning and these have done the job fine but I wanted to try and write a solution that uses a SAT-solver.

SAT-solvers are designed to solve the Boolean Satisfiability Problem that seeks to find a truth assignment for each of a set of boolean variables for which the whole expression is true. For example the expression X1.X2 + X3 is true when X1 and X2 are both true. This is not the only solution though. Since X3 being true or X3, X1, X2 all being true are also solutions So this SAT problem has three solutions. The SAT problem is NP complete This means that all problems in the complexity class NP, which includes a wide range of natural decision and optimization problems, are at most as difficult to solve as SAT. There is no known algorithm that efficiently solves SAT, and it is generally believed that no such algorithm exists; yet this belief has not been proven mathematically, and resolving the question whether SAT has an efficient algorithm is equivalent to the P versus NP problem, which is the most famous open problem in the theory of computing.

SAT-solvers like pycosat require the boolean expression to be in Conjunctive Normal Form (CNF). An expression is in CNF if it is a conjunction of clauses, where a clause is a disjunction of literals; otherwise put, it is an AND of ORs. For example the expression -(X1+X2) is not in CNF but, after apply de Morgan’s Law, is transformed into -X1.X2 it is in CNF.

I wanted to write a Sudoku solver that uses a SAT-solver for the heavy lifting of finding a valid truth assignment for the variables. The problem is that a Sudoku problem requires you to assign a numerical value to each of the 81 cells where as SAT-solvers use boolean variables that are either true or false. The Sudoku needs to be transformed into a boolean expression in CNF to be solved. To do this instead of having one variable per cell we have 9 in the form X(i,j,k) each variable describes whether the cell i,j has a value of k. However this causes a problem because we need to enforce an additional constraint that exactly one of these variables be true for a given cell. We can do this in two parts. Consider first a simple case where we have two variables X1 and X2 and want to enforce that exactly one is true. We can say that at least one variable must be true (X1+X2) and also that both cannot be true -(X1.X2) which is a logical XOR. We can generalize this to N variables, X1, X2, ... ,XN by saying that as least on must be true X1+X2+ ... +XN and that no pair may both be true, -(X1.X2) . -(X2.X3) . ... . which conveniently happens to be in CNF. Code that takes a list of variables represented by positive integers and returns a CNF expression that evaluates to true when exactly one of the variables is true is given next where a negation is represent by a negative number and the absolute value of the number is the variable identifier.

def exactly_one(variables):
    cnf = [ variables ]
    n = len(variables)

    for i in xrange(n):
        for j in xrange(i+1, n):
            v1 = variables[i]
            v2 = variables[j]
            cnf.append([-v1, -v2])

    return cnf

We also need a way to bijectively map the boolean variable X(i,j,k) to a linear variable number which can be done like this:

def transform(i, j, k):
    return i*N*N + j*N + k + 1

We also need the inverse transform to get from a linear variable back to a cell and value:

def inverse_transform(v):
    v, k = divmod(v-1, N)
    v, j = divmod(v, N)
    v, i = divmod(v, N)
    return i, j, k

Armed with this we can generate the standard Sudoku constraints that the numbers 1 to 9 must appear in each row, each column and each 3x3 sub-matrix exactly ones. The final CNF is massive. I’ll spare you the entire 11,988 term expression. But this beautiful disaster is actually pretty cool. It’s a single Boolean Expression that evaluates to true for any value Sudoku and false otherwise. How many are there? Many. About 6,670,903,752,021,072,936,960 according to this paper solutions exist to the blank Sudoku including symmetries. If we augment it with expressions with the fixed cells’ values and find the truth assignment for the expression we have solved the corresponding Sudoku. All that remains if to fix the values of the grid that are given. Then use the inverse_transform to map the CNF variables back to number for each corresponding cell.

It solves the hardest Sudoku (in the sense of having the minimum number of cells filled in) which has the provably minimum number of 16 less in less than 100 milliseconds. Full Python code for the solver, which is about 75 lines long, is available here.