Lecture: Generating Sudoku

Overview

Writing a sudoku solver is a fairly routine programming exercise. But the next step, writing a sudoku generator is less frequently taken, but that's what we'll do today.

The essential observation is that it's surprisingly straightforward to produce a generator from a solver. The basic approach is that of the TV game show Jeopardy: first we generate the answer, and then we generate the question.

  1. Generate a random solved sudoku.
  2. Say that an entry in the sudoku is essential if the sudoku can't solved if that entry is removed, and it is inessential otherwise.
  3. Iteratively select an inessential entry at random, and remove it, until only essential entries remain.

But there is a problem with this simple plan: the only guarantee we can make is that the resulting sudoku can be solved by our solver. If the solver we've used to generate the sudoku is a simple backtracking solver, then the sudoku's we produce may not be solvable by simple forward-based inferencing, which human solvers demand. So our first task is to try to formalize how humans solve sudoku, and to generate a solver based on that formalization.

A Logic Based Approach to Solving Sudoku

Recall that sudoku consist of partially completed 9x9 arrays of numbers, partitioned into 3x3 blocks, e.g.,

6 9 2 8
8 5 6 9
4 2
3
9 4
46 831
1 76
7 39
7

The fundamental constraints on a sudoku board are that each square is to be filled with a number from $1$ through $9$ such that each row, column, and bold-edged 3x3 block contains each of the numbers from 1 through 9, and so (via the pigeon-hole principle), contains each precisely once. We can describe instances of sudoku via propositional logic, introducing propositional variables $v_{rcv}$, which will be true when the digit to be written in row $r$ and column $c$ has value $v$. The fundamental constraints of sudoku can be expressed in propositional logic, most easily by adding a new multi-ary connective $1[\dots]$, such that $1[a,b,\ldots,z]$ is true when exactly one of $a,b,\ldots,z$ is. This is not a standard propositional connective, but it is an exemplar of a common class of propositional count-connectives which are often used in informal reasoning, as anyone who's developed any skill in playing Minesweeper can attest.

We will have four basic types of constraints:

All told, there $729 = 9^3$ distinct variables, and $324 = 4 \times 9^2$ distinct clauses, each of which contains $9$ variables, for $2916 = 4 \times 9^2 \times 9$ distinct variable occurrences. These are big numbers if we have to manage them by hand, but they're small numbers for a computer.

In working with this system, there are three simple rules of inference:

The idea behind the logic-based solver is start with the initial theory, the conjunction of $324$ clauses, and to assert the variables that correspond to the problem instance we're given. We can then apply the assertion elimination rule of inference, eliminating the asserted variables from the theory, while obtaining a number of variables that can be denied. They, in turn, are used to further simplify the theory by the denial elimination rule, perhaps resulting in clauses that are subject to simplification, and thereby the assertion of other variables. This process goes back and forth until no further progress can be made.

Of course, there are many representation and coding decisions that have to be made. In this lecture, we're going to try to make the simplest representation decisions that result in a reasonable efficient solver/generator.

type Position = (Int,Int) newtype Board = Board { getBoard :: Map Position Int } positions :: [Position] positions = (,) <$> [1..9] <*> [1..9] makePosition :: Int -> Int -> Position makePosition = (,)

Note here that we're providing the function makePosition as a kind of abstraction barrier, against the day when we want want a different (possibly more efficient) representation.

We'll also provide Read and Show instances for Board, which can be found in the code.

Because a Board is basically a virtual wrapper around a Map Position Int, it is going to turn out convenient for us to represent a variable as a (Position,Int) pair, as this is the type of the associations of the map.

type Variable = (Position,Int) makeVariable :: Int -> Int -> Int -> Variable makeVariable r c v = (makePosition r c, v)

This will make it easy for us to move back and forth between a Board and a [Variable].

boardToVariables :: Board -> [Variable] boardToVariables = Map.toList . getBoard variablesToBoard ::[Variable] -> Board variablesToBoard = Board . Map.fromList

Next, we'll represent a 1-clause by a set of variables, and a theory by a list of clauses.

type OneClause = Set Variable type Theory = [OneClause]

Our use of Set rather than [] is made for efficiency reasons.

We can now describe the initial theory, which describes the constraints that determine sudoku:

initialTheory :: Theory initialTheory = concatMap genTheory [rvt,rct,cvt,bvt] where rvt row val idx = makeVariable row idx val rct row col idx = makeVariable row col idx cvt col val idx = makeVariable idx col val bvt blk val idx = makeVariable (3*mjr+mnr+1) (3*mjc+mnc+1) val where (mjr,mjc) = divMod (blk-1) 3 (mnr,mnc) = divMod (idx-1) 3 genTheory f = Set.fromList <$> [ f a b <$> [1..9] | a <- [1..9] , b <- [1..9] ]

This code is a bit hairy, but it can be understood. The genTheory function takes an argument that describes how to build the list of clauses that correspond one of the four constraint types, e.g., bvt builds the clauses that represent block-value constraints. These lists are then concatenated together.

The bulk of the logical work is going to be done by two mutually recursive functions, reduceAsserts and reduceDenials. What's going to make this all a bit hairy is that, depending on circumstances, we might want one of two possible return results (a simplified Theory, or Set Variable of the variables that were asserted during the reduction). This suggests that we want types something like this:

type VarSet = Set Variable reduceAsserts :: VarSet -> Theory -> (Theory,VarSet) reduceAsserts theory asserts = ... reduceDenials :: VarSet -> Theory -> (Theory,VarSet) reduceDenials theory denials = ...

Note here that VarSet is the same type as OneClause, but we introduce a new name, because the roles are distinct, i.e., a VarSet is just a set of variables, and shouldn't be interpreted as a clause in our theory.

We can simplify the flow of information by building a Deduction monad. Let's start with some preliminary analysis.

Accumulating assertions

Consider the role of assertions. We need to gather up all of the assertions that get made through calls (including recursive calls) to reduceAsserts, to return as a part of our final answer.

One way to do this is by adding an accumulator variable to the arguments of reduceAsserts and reduceDenials, e.g.,

reduceAsserts :: VarSet -> VarSet -> Theory -> (Theory,VarSet) reduceAsserts oldAsserts asserts theory = case ... of ... -> (theory,asserts `Set.union` oldAsserts) ... -> reduceDenials (asserts `Set.union` oldAsserts) denials reducedTheory reduceDenials :: VarSet -> VarSet -> Theory -> (Theory,VarSet) reduceDenials oldAsserts denials theory = case ... of ... -> (theory,oldAsserts) ... -> reduceAsserts oldAsserts asserts reducedTheory

This isn't terrible, but this explicit handling of an accumulator commits reduceDenials to accepting and passing along an argument it doesn't need. Note too that even reduceAsserts doesn't depend oldAsserts except as a constituent of the accumulated values it passes or returns. So we have a pattern in which a value of interest at the end of the calculation is built up incrementally, and the accumulated pattern isn't needed until the end. This is a pattern we can exploit via the Writer monad, and this is further facilitated by the fact that Set a is a Monoid, whose combining function most happily for our present needs is Set.union. Thus, we could handle the accumulated asserts as follows:

type Deduction = Writer VarSet reduceAsserts :: VarSet -> Theory -> Deduction Theory reduceAsserts asserts theory = do tell asserts ... case ... of ... -> return theory ... -> reduceDenials denials reducedTheory reduceDenials :: VarSet -> Theory -> Deduction Theory reduceDenials denials theory = do ... case ... of ... -> return theory ... -> reduceAsserts asserts reducedTheory

This obligates us to “post-process” the initial call of reduceAsserts via runWriter, but it seems a worthwhile price for such a simplification.

Handling the theory

Much as it's possible to hide the accumulation of asserts, we could also hide the theory from the parameter lists of our functions via the State monad, e.g., (note that we're ignoring the issue of accumulating asserts in this analysis)

type Deduction = State Theory reduceAsserts :: VarSet -> Deduction VarSet reduceDenials :: VarSet -> Deduction VarSet

Unfortunately, this doesn't buy us much: we'd have to get the theory at the beginning of each call, and then put an updated value before making a recursive call. This actually results in more work, rather than less! So we'll stick with using an ordinary parameter.

Error Handling

Let's consider error handling, while we're at it. Our solver can run into trouble if it's given an inconsistent sudoku to solve, e.g., one that contains a duplicated value in the last column. One way to handle this would be to call error, throwing an exception. For example,

reduceAsserts :: VarSet -> Theory -> (Theory,VarSet) reduceAsserts asserts theory = ... where reduceClause clause = case Set.size (clause `Set.intersect` asserts) of 0 -> ... -- the clause is unchanged, and no new denied variables are inferred 1 -> ... -- the clause is eliminated, and new denied variables are inferred _ -> error "unexpected inconsistency"

This comes with a few problems, not the least of which is that exceptions can only be called in IO code, and this could make life difficult for our caller. We could handle this in pure code, using the Either type, but this can muddy up our code, since everything we do has to be aware of the Either wrapping. But we can get around this issue, too, by using the Except monad, which handles the wrapping and interpretation of Either for us. [Note, for Grabmüller aficionados, that he used Control.Monad.Error, which has been superseded by Control.Monad.Except.] Thus,

type Deduction = Except String reduceAsserts :: VarSet -> Theory -> Deduction (Theory,VarSet) reduceAsserts asserts theory = do ... where reduceClause clause = case Set.size (clause `Set.intersect` asserts) of 0 -> ... -- the clause is unchanged, and no new denied variables are inferred 1 -> ... -- the clause is eliminated, and new denied variables are inferred _ -> throwError "unexpected inconsistency"

The difference here is pretty subtle: throwError replaces error, and we have to deal with the more complex monadic type. On the whole, this seems worthwhile, as very limited changes give us the possibility of handing errors in pure code, which we're going to want to do!

Putting it together

We've considered using the Writer, State, and Except monads, and would like to use Writer and Except, and not State. Of course, this presents us with the quandary that monads don't compose, and the natural workaround that we can often obtain the effect of composed monads by using monad transformers.

This raise the question of the order of composition. It's useful here to think about what we want the underlying (non-monadic) types to be. Do we want

Either String (Theory,VarSet) or (Either String Theory,VarSet)

The answer, of course, is the former: we either have an error, or we get back a pair consisting of a theory and set of variables. We can experiment with compositions, but it's useful to remember as a mnemonic that monad transformers build from the outside, in. Thus, the combination we want is

type Deduction = WriterT VarSet (Except String)

It's useful to provide convenience functions to unwrap the monad, in analogy with Control.Monad.State's runState, evalState, and execState:

runDeduction :: Deduction a -> Either String (a,VarSet) runDeduction = runExcept . runWriterT evalDeduction :: Deduction a -> Either String a evalDeduction = fmap fst . runDeduction execDeduction :: Deduction a -> Either String VarSet execDeduction = fmap snd . runDeduction

Note here that we compose our run functions from outside to inside (as viewed in terms of the definition via monad transformers), and that the uses of fmap in the eval and exec functions is to map us through the Either String monad and not through the Deduction monad itself. The eager pattern matchers will want to replace fmap by <$>, but this is a bit tricky, enough to make it of dubious value, e.g.,

evalDeduction = (fst <$>) . runDeduction

We now have most of the pieces necessary to implement reduceAsserts and reduceDenials. Let's consider reduceAsserts. Here's our template thus far:

reduceAsserts :: VarSet -> Theory -> Deduction Theory reduceAsserts asserts theory = do tell asserts ... case ... of ... -> return reducedTheory ... -> reduceDenials denials reducedTheory where reduceClause clause = case Set.size (clause `Set.intersect` asserts) of 0 -> ... -- the clause is unchanged, and no new denied variables are inferred 1 -> ... -- the clause is eliminated, and new denied variables are inferred _ -> throwError "unexpected inconsistency"

Consider reduceClause. Notice that because reduceClause calls throwError, it must return a monadic value. Let's supply the type, which will help organize our thoughts (and for reasons that are at best unclear, GHC 7.10 can't infer it):

reduceClause :: OneClause -> Deduction ... reduceClause clause = case Set.size (clause `Set.intersect` asserts) of 0 -> ... -- the clause is unchanged, and no new denied variables are inferred 1 -> ... -- the clause is eliminated, and new denied variables are inferred _ -> throwError "unexpected inconsistency"

A practical problem here is that it seems we want to return two different types out of the 0 and 1 cases. If none of our clause's variables are asserted, we want to preserve (and therefore return) the clause itself. But if one of the variables is asserted, then we want to return the other variables of the clause as a set to be denied. We'll want to do this for all of the clauses, combining the retained clauses into a reduced theory, and the denied variables into a set be passed along to reduceDenials.

An elegant way to deal with this is to note that “combining” hints at a monoid, and that cartesian products of monoids are monoids. Thus,

reduceClause :: OneClause -> Deduction (Theory,VarSet) reduceClause clause = case Set.size (asserts `Set.intersection` clause) of 0 -> return ([clause],mempty) 1 -> return (mempty,clause \\ asserts) _ -> throwError "unexpected inconsistency"

Note here how we're using mempty for the “uninvolved” coordinate in each case, albeit with different meanings: [] in the first coordinate, and Set.empty in the second.

We then want to map reduceClause across each of the clauses in theory, but we can't use the ordinary map function because reduceClause returns its result in the Deduction monad, and so we must use mapM. The resulting values are combined via mconcat, and then we dispatch into the two cases depending on whether or not any variables were denied:

reduceAsserts :: VarSet -> Theory -> Deduction Theory reduceAsserts asserts theory = do tell asserts reductions <- mapM reduceClause theory case mconcat reductions of (reducedTheory,denials) | Set.null denials -> return reducedTheory | otherwise -> reduceDenials denials reducedTheory where reduceClause :: OneClause -> Deduction (Theory,OneClause) reduceClause clause = case Set.size (asserts `Set.intersection` clause) of 0 -> return ([clause],mempty) 1 -> return (mempty,clause \\ asserts) _ -> throwError "++ inconsistent ++"

The reduceDenials function is very similar, but note the different inner reduceClause function:

reduceDenials :: VarSet -> Theory -> Deduction Theory reduceDenials denials theory = do reductions <- mapM reduceClause theory case mconcat reductions of (reducedTheory,asserts) | Set.null denials -> return reducedTheory | otherwise -> reduceAsserts asserts reducedTheory where reduceClause :: OneClause -> Deduction (Theory,OneClause) reduceClause clause = case Set.size remainder of 0 -> throwError "-- inconsistent --" 1 -> return (mempty,remainder) _ -> return ([remainder],mempty) where remainder = clause \\ denials

The change in error messages is driven by a desire for pretty output, but note the subtle difference between the two.

We're now in a position to write two crucial functions:

type RandState = State StdGen solve :: Board -> Either String Board minimize :: Board -> RandState (Either String Board)

The solve function will take a Board that's partially full, and use logic to complete as much of it as it can. The minimize function will try to eliminate entries from an input board while preserving solvability. The solve function is fairly straightforward:

solve :: Board -> Either String Board solve = fmap (variablesToBoard . Set.toList) . execDeduction . flip reduceAsserts initialTheory . Set.fromList . boardToVariables

We swizzle a Board into a VarSet, and then use reduceAsserts together with our initialTheory to derive what we can. The asserted values are extracted from the resulting monadic value via execDeduction, resulting in a value of type Either String VarSet, which is then swizzled back into a Board.

The minimize function is a bit more intense:

minimize :: Board -> RandState (Either String Board) minimize = fmap (evalDeduction . iter []) . permute . boardToVariables where iter essential [] = return $ variablesToBoard essential iter essential (v:vs) = do sv <- solvable (essential ++ vs) iter (if sv then essential else v:essential) vs solvable = fmap null . flip reduceAsserts initialTheory . Set.fromList

To understand this, let's start with the permute function:

permute :: [a] -> RandState [a] permute as = map fst . sortBy (comparing snd) . zip as <$> replicateM (length as) (state next)

The permute function lives in the RandState monad, and produces a random permutation of a list by pairing it up with a randomly generated list, sorting on the random elements, carrying the elements of the original list into a random order.

The expression permute . boardToVariables is thus seen to have type Board -> RandState [Variable]. We then convert the inner [Variable] to a Either String Board by use of a pure function, via reduceAsserts and the Deduction monad. The key to this is the local function iter, which analyzes each variable in order for “essentialness.“ Note that iter calls solvable, which calls the monadic function reduceAsserts, and so both iter and solvable end up living in the Deduction monad, too, specifically,

iter :: [Variable] -> [Variable] -> Deduction Board solvable :: [Variable] -> Deduction Bool

which explains the use of evalDeduction to get us from Deduction Theory to Either String Board as required.

Code Organization

The remaining code contains few surprises, but the way it's organized is worth some discussion. There are a total of four source files (not including the sudoku.cabal file, etc.), organized into the Main, Sudoku.Base, Sudoku.Solve, and Sudoku.Generate modules.

The Sudoku.Base module contains definition of the Position and Board types, the Read and Show instances of Board, the definition of RandState, and the permute function.

The Sudoku.Solve module is where most of the heavy lifting is done. It includes the definitions of the Variable type, of the Deduction monad, of initialTheory, reduceAsserts, reduceDenials, solve, and minimize, exporting only the solve, and minimize function. Thus, much of the complexity of this code (including the Deduction monad and functions that involve this type) is hidden from the rest of the program.

The Sudoku.Generate module exports a single function: genSudoku :: RandState Board, which generates a fully solved instance of sudoku within the RandState monad. It does this via a simple back-tracking solver, which fixes a random permutation of the values at each position, and returns the lexically least fully solved sudoku within the order defined by these permutations. This is much easier than it sounds.

The Main module, which handles all IO. Briefly, with no arguments given, the program generates a new sudoku, and if one or more arguments are given, they are interpreted as paths to files that contain sudoku problems, which are then solved via the logic-based solver. One nice feature of this is that "-" is interpreted as stdio, so it is possible to test the program using:

$ sudoku | sudoku - =================== . . 7 . 5 . . . 9 . . . . . 3 . . . 4 . . 7 . . . 3 . 2 . . 6 . . . 8 . . . 1 . 3 . . 4 . 3 6 . . . 1 . 2 5 . 2 . . . 5 7 . 8 8 . . . . . . . . . . . . . . 4 . . ------------------- 6 3 7 4 5 8 2 1 9 5 9 2 1 6 3 8 7 4 4 1 8 7 2 9 5 3 6 2 7 5 6 9 4 1 8 3 9 8 1 5 3 2 6 4 7 3 6 4 8 7 1 9 2 5 1 2 9 3 4 5 7 6 8 8 4 6 9 1 7 3 5 2 7 5 3 2 8 6 4 9 1 =================== $

i.e., generate a problem, then solve it, printing both.

Code

A tarball for this program can be found at sudoku-0.1.0.0.