Jul 042011
 

One of my recent interests has been in solving problems with various kinds of satisfiability solvers. As an introduction to this idea I want to demonstrate how to create a sudoku solver with almost no effort by reduction to a common satisfiability problem (CNF-SAT) and using an existing solver (MiniSat).

Solving sudoku by reduction to CNF-sat is hardly a new idea, I’m sure a quick google would show various approaches. If the mathematical notation below looks a little scary perhaps try reading the code further down, it really is quite simple if you can read propositional formulas.

A quick sudoku recap

A sudoku puzzle is a 9×9 grid of cells, split into 9 non overlapping 3×3 “boxes”. Some of these will be labelled with a digit from 1 to 9, others will be blank. The aim is to label the remaining cells so that every row, column and box contains the digits 1 through 9.

Unsolved sudoku grid

Unsolved sudoku grid


Solved sudoku gird

Solved sudoku gird

CNF-SAT

Perhaps the most well known satisfiability problem is propositional satisfiability: given a formula in propositional logic can we find assignments for all the variables which makes the formula true? A subset of this problem is satisfiability on formulas in conjunctive normal form (CNF-SAT). A formula is in conjunctive normal form if it is a conjunction of clauses, where a clause is a disjunction of literals (a literal is just a variable or its negation), e.g

\[ (a \vee \neg b) \wedge (\neg a \vee c \vee d) \wedge (\neg b \vee \wedge \neg d) \] \[ a \wedge (\neg a \wedge \neg b) \]

The reduction

Our aim is, given an unsolved sudoku grid, to identify a set of variables and a CNF formula upon them which is satisfiable if and only if the gird has a solution. Additionally we want the assignment of variables (the model) to describe unambiguously the solution to the puzzle. We’ll proceed by first finding a way to represent the grid with boolean variables, then find formulas which ensure the grid satisfies the sudoku constraints and matches the given puzzle grid.

Grid representation

Let us begin by identifying a way to describe sudoku grids with a set of boolean variables which would be easy to enforce sudoku constraints upon with a propositional formula. Let our boolean variables be \( \{x_{i,j,k} : i,j,k \in \{1,\ldots,9\} \}\). The interpretation is that if \( x_{i,j,k} \) is true then cell \( (i,j) \) is labelled with k.

Of course this representation does not enforce that every cell has exactly one label! We’ll have to include a term in the reduction formula that ensures this is the case. If a cell has more than one label than it will have some pair of distinct labels. So given a cell \( (i,j) \) the we can check it has exactly one label with a CNF formula

\[ l_{i,j}:=(x_{i,j,1} \vee \ldots \vee x_{i,j,9}) \bigwedge_{k,l \in \{1,\ldots,9\}}_{k \neq l} \neg x_{i,j,k} \vee \neg x_{i,j,l}.\]

So to ensure the model describes a labelling we just need the formula
\[ \sigma := \bigwedge_{i,j \in \{ 1,\ldots,9 \}} l_{i,j} \] to be true. Note this is in CNF.

Sudoku constraints

Now we need to include the sudoku constraints: each row, column and box needs to contain the labels 1 through 9. Let a group be a set of 9 cells that must contain all the digit. Let \( \mathcal{G} \) be a set of sets containing the all the groups on a sudoku grid, i.e groups for the rows, columns and boxes \(3 \times 3 \) boxes. We can now express the sudoku constraint with the following CNF formula:

\[ \phi = \underbrace{\bigwedge_{k \in \{1,\ldots,9\}}}_{\textrm{for each digit}} \underbrace{\left( \bigvee_{(i,j)\in\mathcal{G}} x_{i,j,k} \right)}_{\textrm{each group has}}_{ \textrm{a cell labeled with it}} \]

Once again this is a CNF.

Puzzle constraints

Now we just need to include constraints that restrict cells that were labelled in the puzzle grid to keep that label. Let
\[ \mathcal{C}:=\{(i,j,k):\textrm{cell $(i,j)$ has label $k$ in puzzle grid}\}. \]
Then the formula
\[ \psi := \bigwedge_{(i,j,k) \in \mathcal{C}}x_{i,j,k}\]
ensures that the solution matches the original puzzle (again \( \psi \) is in CNF).

Putting it all together

So given a puzzle the formula
\[ \sigma \wedge \phi \wedge \psi \] is satisfied if and only if the variables \( \{x_{i,j,k} : i,j,k \in \{1,\ldots,9\} \}\) describe a solution to the puzzle. Cell \( (i,j) \) is labelled \( k \) if and only if \( x_{i,j,k} \) is true.

It’s easy enough to code this up in Haskell. The following code extract constructs the formula form a sudoku grid. A variable in MiniSat is a positive integer, so I had to create a bijection from labelled cells (triples) to integers. A CNF formula in the code below is just a list of list of integers.

-- cartesean product of a list with itself
cross list = [(x,y) | x <- list, y <- list]
 
-- Sudoku cells values are represented by triples where the first and second
-- entry specify row and column respectively (zero indexed) and the third
-- specifies labelling (1-9).
-- Define a bijection between cell value triples and natural numbers that will
-- serve as boolean variable names.
cellToVar (i,j,k) = fromIntegral $ (k-1)*81 + i*9 + j + 1
varToCell x = ((i `mod` 81) `div` 9, i `mod` 9, (i `div` 81)+1)
	where i = (fromIntegral x)-1
 
-- List of clauses that ensures a given cell is labeled with exactly one value.
-- Checks for every pair of labels that the cell is NOT labeled by both
-- and that the cell is is labeled with at least one value.
oneLabel (i,j) = atLeastOne : lessThan2
	where notBoth (c1,c2) = [- cellToVar (i,j,c1), - cellToVar (i,j,c2)]
              lessThan2  = map notBoth $ [(i,j) | (i,j) <- cross [1..9], i /= j]
              atLeastOne = map cellToVar [(i,j,k) | k <- [1..9]]
 
-- List of clauses that ensures every cell has exactly one label.
validLabeling = foldr ((++).oneLabel) [] $ cross [0..8]
 
-- Definition: A group of cells is a set of cells that must contain
-- one of all the labels. i.e. One of the column, rows or 3x3 squares.
-- List of the square groups of cells.
squareGroups = [quadrent i j | (i,j) <- cross [0..2]]
	where quadrent x y = [(x*3+i,y*3+j) | (i,j) <- cross [0..2]]
-- List of rows, list of cols.
rows = [[(i,j) | i <- [0..8]] | j <- [0..8]]
cols = [[(i,j) | j <- [0..8]] | i <- [0..8]]
 
-- Formula that ensures a group of cells contains at least one of all labels [1-9].
groupGood group = foldr ((:).label) [] [1..9]
	where label k = map cellToVar [(i,j,k) | (i,j) <- group ]
 
-- Formula ensuring a labeling is good.
-- A labeling is "good" if it satisfies the sudoku constraints, that is every
-- square, row and cell contains one of each label.
goodLabeling = foldr ((++).groupGood) [] (squareGroups ++ rows ++ cols) 
 
-- Produce a formula for a set of sudoku constraints - filled in cells,
-- for which a model describes a sudoku solution.
sudokuForm cells = validLabeling ++ goodLabeling ++ (map consClause cells)
	where consClause cell = [cellToVar cell]

To see the full code, which includes IO, have a look at the github.

Results and further thoughts

Considering that we’ve at no point actually thought about how to solve sudokus this technique works remarkably well. This solver can reliably solve “hard” instances quickly, simple na├»ve solvers can take a long time on these. The github contains some harder puzzles, some coming from this article.

Of course specialist algorithms will do even better, but we’ve pretty much solved the problem with no effort. In a future post I hope to describe some harder problems I’ve tackled with boolean satisfiability, in these cases there were no existing algorithms to solve the problem and SAT (but not CNF-SAT) reduction turned out to be the best of all the techniques I tried!

 Posted by at 6:24 pm

 Leave a Reply

(required)

(required)

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>