SudokuSAT.lhs

  <!--
\begin{code}
module SudokuSAT where
\end{code}
  -->

(This post is literate Haskell, [available here](https://gist.github.com/emilaxelsson/e15a3b72eef7468e5edf).)

Inspired by an [old(-ish) Galois post](https://galois.com/blog/2009/03/solving-sudoku-using-cryptol/) about using its SAT back end to solve sudokus, here is a similar sudoku solver written in Haskell using Koen Claessen's [SAT+ library](https://github.com/koengit/satplus).

  <!--
\begin{code}
import Data.List

import SAT hiding (modelValue)
import SAT.Equal
import SAT.Val
\end{code}
  -->



Representing sudokus
--------------------------------------------------------------------------------

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

\begin{code}
type Sudoku = [[Maybe Int]]
\end{code}

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](https://en.wikipedia.org/wiki/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:

\begin{code}
blocks :: [[a]] -> [[a]]
\end{code}

  <!--
\begin{code}
blocks _ = []
\end{code}
  -->

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 representation of `blocks` from this post, because it's part of a [lab here at Chalmers](http://www.cse.chalmers.se/edu/course/TDA555/lab3.html).)



Solving constraints using SAT+
--------------------------------------------------------------------------------

[SAT+](https://github.com/koengit/satplus) 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:

~~~~~~~~~~~~~~~~~~~~{.haskell}
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`:

~~~~~~~~~~~~~~~~~~~~{.haskell}
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:

~~~~~~~~~~~~~~~~~~~~{.haskell}
solve :: Solver -> [Lit] -> IO Bool
~~~~~~~~~~~~~~~~~~~~

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

~~~~~~~~~~~~~~~~~~~~{.haskell}
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:

\begin{code}
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)
\end{code}

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:

\begin{code}
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
\end{code}

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:

\begin{code}
toSudoku :: Solver -> Sudoku' -> IO Sudoku
toSudoku sol rs = mapM (mapM (fmap Just . modelValue sol)) rs
\end{code}

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

\begin{code}
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
\end{code}