Sudoku solver using SAT+

(This post is literate Haskell, available here.)

Inspired by an old(-ish) Galois post about using its SAT back end to solve sudokus, here is a similar sudoku solver written in Haskell using Koen Claessen’s SAT+ library.

Representing sudokus

We represent sudokus as a simple column-of-rows:

type Sudoku = [[Maybe Int]]

A valid sudoku will have 9 rows and 9 columns and each cell is either Nothing or a value between 1 and 9.

The rules of sudoku mandates that each of the 27 “blocks” (rows, columns and $3\times 3$ squares) only contain distincts numbers in the interval 1-9. So the first thing we need is a function for extracting the blocks of a sudoku:

blocks :: [[a]] -> [[a]]

The argument is a sudoku ($9\times 9$ elements) and the result is a list of blocks ($27\times 9$ elements). We use a polymorphic function in order to make it work also for the SAT representation of sudokus below.

(We omit the definition of blocks from this post, because it’s part of a lab here at Chalmers.)

Solving constraints using SAT+

SAT+ is a library that adds abstractions and convenience functions on top of the SAT solver MiniSAT. Here we will only make use of quite a small part of the library.

The inequality constraints of sudokus can be expressed using the following functions:

newVal   :: Ord a => Solver -> [a] -> IO (Val a)
val      :: a -> Val a
notEqual :: Equal a => Solver -> a -> a -> IO ()

Function newVal creates a logical value that can take on any of the values in the provided list. A specific known value is created using val, and finally, inequality between two values is expressed using notEqual.

The Solver object required by newVal and other functions is created by newSolver:

newSolver :: IO Solver

After a solver has been created and constraints have been added using the functions above, we can use solve to try to find a solution:

solve :: Solver -> [Lit] -> IO Bool

If solve returns True we can then use modelValue to find out what values were assigned to unknowns:

modelValue :: Solver -> Val a -> IO a

These are all the SAT+ functions we need to solve a sudoku.

The solver

In order to solve a sudoku, we first convert it to a “matrix” of logical values:

type Sudoku' = [[Val Int]]

fromSudoku :: Solver -> Sudoku -> IO Sudoku'
fromSudoku sol = mapM (mapM fromCell)
  where
    fromCell Nothing  = newVal sol [1..9]
    fromCell (Just c) = return (val c)

This simply converts the matrix of Maybe Int to a matrix of Val Int, such that Just c is translated to the logical value val c and Nothing is translated to a logical value in the range 1-9.

Next, we need to add inequality constraints according to the rules of sudoku. After obtaining the blocks using blocks, we just add constraints that all values in a block should be different:

isOkayBlock :: Solver -> [Val Int] -> IO ()
isOkayBlock sol cs = sequence_ [notEqual sol c1 c2  | c1 <- cs, c2 <- cs, c1/=c2]

isOkay :: Solver -> Sudoku' -> IO ()
isOkay sol = mapM_ (isOkayBlock sol) . blocks

After solving a sudoku, we need to be able to convert it back to the original representation. This is done using modelValue to query for the value of each cell:

toSudoku :: Solver -> Sudoku' -> IO Sudoku
toSudoku sol rs = mapM (mapM (fmap Just . modelValue sol)) rs

Now we have all the pieces needed to define the solver:

solveSud :: Sudoku -> IO (Maybe Sudoku)
solveSud sud = do
    sol  <- newSolver
    sud' <- fromSudoku sol sud
    isOkay sol sud'
    ok <- solve sol []
    if ok
      then Just <$> toSudoku sol sud'
      else return Nothing