Skip to content

Instantly share code, notes, and snippets.

@emilaxelsson
Last active October 26, 2015 11:00
Show Gist options
  • Save emilaxelsson/e15a3b72eef7468e5edf to your computer and use it in GitHub Desktop.
Save emilaxelsson/e15a3b72eef7468e5edf to your computer and use it in GitHub Desktop.
<!--
\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}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment