(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
```

## No comments:

## Post a Comment