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

Difference between LTL and CTL

(Note that this article assume some intuitive understanding of CTL.)

I’m currently teaching a course on Hardware Description and Verification, in which we cover computation tree logic (CTL) model checking. In preparing for the course, I wanted to fully understand the differences between CTL and LTL. The common informal explanation that LTL has linear time while CTL has branching time is useless without further explanation. I had a certain understanding of CTL, and my initial assumption was that LTL is what you get by excluding all $E$ formulas from CTL. This assumption turned out to be wrong.

My assumption would imply that LTL is a subset of CTL, but the Wikipedia page claims that neither logic is a subset of the other. It seems like I’m not alone in being confused about the difference between the two logics: This Stack Exchange page has the same question. The answer on that page talks about the LTL formula

$$\mathit{\text{FG}}p$$

which, apparently, is not the same as the CTL formula

$$\mathit{\text{AF}}\mathit{\text{AG}}p$$

(as I previously thought). After reading the Stack Exchange answer I started to get a sense of the difference, but I still wasn’t able to formulate it easily. So I had no more excuses not to look into the actual formal semantics of LTL and CTL. This survey by Emerson served as a good reference for that.

Common superset: CTL*

The difference between LTL and CTL is easiest to understand by considering CTL* which has both LTL and CTL as subsets. CTL* has two syntactic categories giving rise to two different kinds of formulas: state formulas and path formulas. A state formula is something that holds for a given state in a system (modeled as a Kripke structure), while a path formula holds for a given path. A path is an infintie sequence of states such that each consecutive pair of states is in the transition relation; i.e. a trace of an infinite run of the system. Note that, even though a state formula is a property of a single state, it can still talk about future states by using the path quantifiers $A$ and $E$.

Now, the important thing to note is that an LTL formula is a (restricted) CTL* path formula while a CTL formula is a (restricted) CTL* state formula. Path formulas are not very interesting on their own, since one is usually interested in expressing properties of all or some paths from the initial state. Hence, the real meaning of an LTL formula is obtained by adding an implicit $A$ quantifier to it turning it into a state formula. Thus the meaning of the LTL formula $f$ is the meaning of the CTL* formula $Af$.

The example

With this understanding, we can try to reformulate the above examples in English:

The LTL formula $\mathit{\text{FG}}p$ can be read as

“Every path (implicit $A$) will eventually ($F$) reach a point after which $p$ is always true ($Gp$).”

Or perhaps more clearly:

“Every path has a finite prefix after which $p$ is always true.”

The CTL formula $\mathit{\text{AF}}\mathit{\text{AG}}p$ can be read as

“Every path ($A$) will eventually ($F$) reach a state from which every path ($A$) has the property that $p$ is always true ($Gp$).”

These formulas are subtly different, and they can be distinguished by the following system of three states:

$S_1\mapsto S_1\mathrm{\text{or}}{S}_2(\mathrm{\text{atomic:}}p)$

$S_2\mapsto S_3(\mathrm{\text{atomic:}}\neg p)$

$S_3\mapsto S_3(\mathrm{\text{atomic:}}p)$

Every run of this system will either (1) stay in $S_1$ forever, or (2) wait some finite time and then make a transition to $S_2$ and $S_3$. In both cases, it holds that the trace has a finite prefix after which $p$ is always true. Hence the LTL formula holds.

However, the CTL formula does not hold, because there is a path that never reaches a state at which $\mathit{\text{AG}}p$ holds. This is the path in which the system stays in $S_1$ forever. Even if it stays in $S_1$ forever, it always has the possibility to escape to $S_2$.

Summary

As demonstrated by the above example, the difference between LTL and CTL (except for the absense of $E$ in LTL) is that an LTL formula can be verified by considering each path in isolation. If each individual path obeys the path formula, the LTL formula is true. To verify a CTL formula, one may also have to consider the alternative possibilities for each state in a path.