Solving Sudoku Using Preemptive Sets


A while back, the American Mathematical Society published a paper by J. F. Crook titled “A Pencil-and-Paper Algorithm for Solving Sudoku Puzzles” that claimed to provide a way to solve any Sudoku puzzle using only paper and pencil.

This is less impressive than it sounds, though, because people were already solving Sudoku puzzles just fine. It’s just that the hard ones would often require the uncomfortable step of taking a blind guess to make further progress. This paper formalizes a neat trick using a concept called the “preemptive set” to make guessing come up less frequently (though you still have to do it for the hardest puzzles).

The preemptive set heuristic is a little different from the standard set of tricks for solving Sudoku puzzles, and it’s pretty interesting to see what it looks like in Haskell. First we’ll have to up some preliminaries and think about how to model the general task of solving a Sudoku puzzle. Then we’ll be able to see what this trick is all about. Along the way, we can see how Haskell lets us write code that closely reflects how we think about the problem domain.

Name all the things

Sudoku terms

It’ll be useful to first get specific about a few bits of terminology.

A Sudoku board is a 9-by-9 grid of cells, where some cells contain a number and others are left blank. The puzzle is solved when each row, column, and box contains the digits 1 through 9 and every cell contains exactly one digit.

Collectively, instead of saying “rows, columns, and boxes”, we’ll say ranges, so each range must contain the digits 1 through 9.

An important concept in solving these puzzles is that each cell will have a set of numbers that it can potentially contain. This is called the markup of the cell, and as we proceed in solving the puzzle, we will cross out numbers from the markup until every cell has only one number. That remaining number is the solution of that cell.

The board in Haskell

Now let’s think about the types that we can use to represent a Sudoku board. Each cell in the board is either solved with a single number or unsolved with a set of potential solutions. Simple enough:

data Cell = Unsolved !IntSet
          | Solved !Int
          deriving (Eq)

We will give each cell a unique index $(i,j)$, where $i$ is the row and $j$ is the column, and the board itself is a collection of 81 cells associated with their indices $(i,j)$. We’ll just use a Map type to represent this mapping from index to cell.

type Idx = (Int, Int)
newtype Board = Board (Map Idx Cell) deriving (Eq)

There are some very simple functions that we’ll need to implement on these types, but they’re not particularly interesting, so I’ll skip over those details here. You can find the full source code on GitHub.

Marking up the puzzle

The first thing we’ll want to do with our puzzle is to build the markup. That is, to go through the unsolved cells and cross out any numbers that cannot possibly belong in that cell. This is called constraint propagation, and you can actually implement a complete Sudoku solver by combining just this trick with some guessing.

But let’s just think about how we might compute the markup of a puzzle, in words.

Markup Algorithm

  1. Write the numbers 1 – 9 in every unsolved cell.
  2. Look at a solved cell. Let’s say we have the number 5 in cell $(1,1)$.
  3. Cross out 5 from its peer cells, which are all the other cells in its row, column, and box.
  4. Repeat from step 2 for every solved cell.

Sometimes we will create additional solved cells by this algorithm. We could be clever and keep track of the new solved cells so that we make sure to cross out their peers as well. But a simple alternative is to just iterate the markup algorithm a few times until the we run out of numbers to cross out.

This is maybe a completely obvious algorithm, but notice that it has a couple of important properties that we will want to model in Haskell:

  1. It’s stateful. That is, we write on the grid and therefore change it. It would be convoluted to try to write this algorithm without this implicit state.
  2. It can fail if we’re not given a proper Sudoku puzzle. For example, if there are two solved cells in a single column that are both 5, then following our algorithm would result in a cell with no possible numbers in it.

So we need some kind of way to represent a stateful calculation that can fail. This sounds like a job for…

The m-word

A monad! We will use the StateT monad to model stateful computation, and the Maybe monad for the possibility of failure. Let’s call this the BoardState monad. We’ll also need to implement readCell and writeCell inside this monad so that we can implement crossOut.

type BoardState a = StateT Board Maybe a -- Board -> Maybe (a, Board)
readCell :: Idx -> BoardState Cell
writeCell :: Idx -> Maybe Cell -> BoardState ()

Since the implementations of readCell and writeCell are immediate from their types, I’ll just leave the code for the GitHub appendix.

Now we have enough components to implement our first non-trivial function, crossOut, which takes a collection of cell indices and, for each of those cells, deletes some numbers from it, and writes back the updated cell. If you take the previous sentence and add some symbols here and there, you will get this definition:

crossOut ijs values = forM_ ijs $ \ij ->
    readCell ij >>= return . deleteCellValues values >>= writeCell ij

And now we’re ready to implement the markup algorithm:

markup board =
  flip execStateT board $
  forM_ (boardCells board) $ \(ij, cell) -> do
    when (cellIsSolved cell) $ do
      let Solved n = cell
      let peers = filter (/= ij) $ colOf ij ++ rowOf ij ++ boxOf ij
      crossOut peers (IntSet.singleton n)

We want users of markup to not worry (or even know) about the fact that the markup algorithm is expressed in a stateful way, so we will use execStateT inside the function to get the result out of the StateT monad.

Inside the stateful execution, markup looks quite like the algorithm that we stated in words earlier. Conveniently, it operates on an implicit board in the background, so we didn’t need to thread the board state through every function. That would have added a lot of unnecessary repetitiveness and would have obscured the simple core idea of the algorithm. And we didn’t need to make board a global variable to achieve this implicit statefulness.

We also didn’t need to explicitly handle every possible failure state. If at any point we get to an invalid board state by crossing out the last remaining value of a cell, we get a Nothing that just propagates out and the whole markup function will return Nothing.

Best of all, we got this all for free, just by selecting the right monads!

Preemptive sets

Up to this point, we built the foundations of a Sudoku solver by describing what we wanted in words, and then carefully translating those words into Haskell. By picking the right data representations, we were able to write code in a way that closely modeled the problem domain, relegating secondary effects to some carefully chosen monads.

Now we’ll be able to take this foundation and build a very straightforward solver on top.

To do this, we’ll finally introduce the notion of a preemptive set. Let’s start with the Haskell representation:

data PreSet = PreSet
  { psNumbers :: !IntSet
  , psCells :: !(Set Idx)
  }

A preemptive set, or a PreSet as we’ve called it here, is a product type of a set of numbers and a set of cells. We’ve found a preemptive set when the set of numbers has the same size as the set of cells, and the numbers are the only numbers that can occupy those cells.

We can find a preemptive set by looking at the markup of a row, column, or box, and trying to find groups of unsolved cells that share the same numbers. For example, if you find three cells that share only $5,7,9$, then you’ve found a preemptive set. Note that not every cell in the set needs to have all three numbers in its markup. One of them could be $5$, one of them could be $5,7$, and the final one could be $7,9$. The rule is that no cell’s markup can contain anything other than the those three numbers.

So a way to check whether a set of cells is a preemptive set is to simply calculate the union of the markup of the cells (which gives you the set of numbers that those cells can contain), and then compare the size of that union to the number of cells. If those two quantities are equal, then you have a preemptive set.

Now here’s the key: once you have found a preemptive set s :: PreSet, say in a row, you know that the numbers of that set psNumbers s must be in one of the cells psCells s. Therefore those numbers could not be in any other cells in that row. So you can cross those numbers off of the markup of the cells that are not in the preemptive set. By going along the puzzle, identifying all the preemptive sets, and applying this cross-out logic, you can solve most simple to medium difficulty puzzles without guessing.

Once again, I’ll only discuss the interesting parts of the implementation here, but you can find the full source code on GitHub.

The algorithm

Let’s consider first how we would find a preemptive set of a particular size. We would need to consider each row, column, and box, and check every combination of unsolved cells of size $n$. So for sets of size 2, there would be $\binom{9}{2} \times 9 \times 3=972$ combinations to try, and for sets of size 3, there would be $\binom{9}{3} \times 9 \times 3=2268$ combinations. This points to an obvious solution: brute force!

For each range (row, column, or cell), we will just every combination until we find all the possible preemptive sets. There’s one obvious optimization here that we can add easily: when we find a preemptive set, we remove the cells in that set from further consideration. This whittling down of the cells under consideration lends itself quite naturally to a recursive process for a fixed preset size:

findPreSets :: Board -> Int -> [Idx] -> [PreSet]
findPreSets board n range = go (combinations n unsolvedCells) []
  where
    unsolvedCells = filter (cellIsUnsolved . boardGetCell board) range
    unionMarkupOfCells = IntSet.union . cellMarkup . boardGetCell board
    go [] acc = acc
    go (x:xs) acc =
      let nums = foldr unionMarkupOfCells IntSet.empty x
      in if IntSet.size nums == n
           then go
                  (removeAny x xs)
                  (PreSet {psNumbers = nums, psCells = Set.fromList x} : acc)
           else go xs acc

To use this function, we will call it once for each preemptive set size we want. For our solver, we’ll just consider sets of size 2, 3, or 4. It’s okay to do this because the final step in our solution strategy is to exhaustively check every remaining possibility until a solution is found.

preSets :: Board -> [Idx] -> [PreSet]
preSets board range = ps 2 ++ ps 3 ++ ps 4
  where
    ps n = findPreSets board n range

The punchline

Now we finally get to the point of finding the preemptive sets in the first place: we can now cross out numbers not in the set. We go range to range, find a preemptive set in that range, and cross out those numbers from other cells. This has a completely straightforward translation in code:

applyPreSets :: Board -> Maybe Board
applyPreSets board =
  flip execStateT board $ do
    go rows
    go cols
    go boxes
  where
    go ranges =
      forM_ ranges $ \ijs -> do
        b <- get
        forM_ (preSets b ijs) $ \ps -> do
          let otherCells = Set.fromList ijs \\ psCells ps
          crossOut otherCells (psNumbers ps)

Since go here operates inside the BoardState monad, we can avoid repetitively mentioning board – it is implied that we’re be modifying it. The return type here is Maybe Board because crossOut can fail on an invalid puzzle, and this return type is enforced by the type of the monad so we can’t accidentally forget.

Now solve it!

This is the home stretch! The first step in our strategy is to try solving the puzzle by (1) crossing out as much as possible by propagating the constraints and then (2) applying our preemptive set logic. For simple puzzles, that’s all it will take to find a solution.

But not every puzzle can be solved this way. We haven’t ruled out the possibility that doing (1) followed by (2) will open up new possibilities for crossing things out. To handle this, we will continue applying (1) followed by (2) until nothing further gets crossed out.

Now notice that we have been writing code in a stateful style up to now, and if we had actually been overwriting board states, introducing the intention to compare sequential board states at this late stage is potentially problematic. Where would get go get the previous board state that we overwrote?

But in Haskell, although we indeed wrote in a stateful style out of convenience, we can nevertheless easily refer to previous states because nothing was modified. Thus it is trivial to implement this algorithm:changed.

simplify :: Board -> Maybe Board
simplify board = go (Just board) Nothing
  where
    go a b
      | a == b = a
      | otherwise = go (a >>= markup >>= applyPreSets) a

But even this will not solve the most stubborn boards. For those, we must still resort to guessing. So we will fall back to guessing: identify an unsolved cell in some manner (we just pick a cell with the fewest remaining answer choices) and try each choice until we either reach a contradiction or find a solution.

solve :: Board -> Maybe Board
solve board = do
  simplifiedBoard <- verify =<< simplify board
  if boardIsSolved simplifiedBoard
    then Just simplifiedBoard
    else do
      let (ij, cell) = chooseUnsolvedCell simplifiedBoard
      let solvedBoards =
            map
              (solve <=< boardSetCellValue simplifiedBoard ij)
              (cellValues cell)
      firstValid solvedBoards
  where
    firstValid = asum

You can see that the list solvedBoards in this function actually contains every solution, even though we only ask for the first valid one. Because of Haskell is lazy, the computation will stop once the first valid solution is found. But by writing it this way, we get the ability to enumerate all the solutions for free!

Conclusion

So we’ve seen that we can implement a fairly intricate algorithm via largely straightforward translations from some informal descriptions of what we wanted to do. We rarely needed to introduce extra book-keeping items like loop counters, and checks for board validity were mostly hidden behind the BoardState monad.

In fact, the BoardState monad gave us a whole host of convenient features that allowed us to talk about crossing out numbers in a stateful way, while providing a type-safe and pure way for dealing with the underlying data representation. Purity came in handy when we wanted to define simplify to iterate until the board’s previous state matched its current state. And type-safety meant that we could never forget that crossing out a number could lead to an invalid board. We used Maybe to represent this state here, though we could have gone even further with some more advanced techniques that we’ll talk about later.

The key point is that most of the time, the code we wrote dealt with the real business logic of solving a Sudoku puzzle, almost as if we were writing in some pseudo-code language that had been designed to solve logic puzzles.

February 11, 2018