Lecture 26: A Sudoku Generator

The Solver

In this lecture, we're going to revisit the problem of solving Sudokus, following a logic-based approach. Recall that Sudokus 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 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 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. For various reasons, we're going to want to preserve (or at least, stay close to) some of the representation decisions we made in writing the backtracking solver in Lecture 20 e.g.,

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

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 Var = (Position,Int) mkVar :: Int -> Int -> Int -> Var mkVar row col val = ((row,col),val)

This choice simplifies moving back and forth between [Var] and Board.

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

type OneClause = Set Var type Theory = [OneClause]

One of the things we're going to need to do is keep track of sets of variables, and to manipulate them via the Monoid interface, where (<>) is implemented via Set.union. To that end, we define

newtype Union a = Union { getUnion :: Set a } instance Ord a => Semigroup (Union a) where x <> y = Union (getUnion x `Set.union` getUnion y) instance Ord a => Monoid (Union a) where mempty = Union empty

using Union as a type-wrapper to select this particular Monoid instance.

We can now describe the initial theory, which describes the $324$ constraints that determine Sudoku:

initialTheory :: Theory initialTheory = concatMap genTheory [rvc,pvc,cvc,bvc] where rvc row val idx = mkVar row idx val cvc col val idx = mkVar idx col val pvc row col idx = mkVar row col idx bvc blk val idx = mkVar (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 idx | idx <- [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., bvc is used to build a clause that corresponds to a block-value constraint. These lists are then concatenated together to construct the initial theory.

The bulk of the logical work is going to be done by two mutually recursive functions, reduceAsserts and reduceDenials, which return values of the Reduction () type:

type Reduction = StateT Theory (Writer (Union Var))

The idea here is that we use the StateT aspect of the Reduction to hold a Theory, which is going to be successively thinned out through the use of assertion and denial eliminations, and that the Writer aspect will be used to retain the set of variables asserted through the reduction.

Before moving on the implementation of reduceAsserts and reduceDenials, we'll introduce one more utility function, used by both:

eitherMap :: (a -> Either b c) -> [a] -> ([b],[c]) eitherMap f = partitionEithers . map f

This function seems so natural that you'd all but assume it was already defined in either Data.Either or even the Prelude, but alas, it is defined in neither.

We're now ready for the core of the logic solver:

reduceAsserts :: Set Var -> Reduction () reduceAsserts asserts = do tell $ Union asserts theory <- get let (reducedTheory,denials) = eitherMap reduceClause theory put reducedTheory unless (null denials) $ do reduceDenials (unions denials) where reduceClause clause = case Set.size (asserts `intersection` clause) of 0 -> Left clause 1 -> Right (clause \\ asserts) _ -> error "inconsistent problem" reduceDenials :: Set Var -> Reduction () reduceDenials denials = do theory <- get let (reducedTheory,asserts) = eitherMap reduceClause theory put reducedTheory unless (null asserts) $ do reduceAsserts (unions asserts) where reduceClause clause = case Set.size diffs of 0 -> error "inconsistent problem" 1 -> Right diffs _ -> Left diffs where diffs = clause \\ denials

Let's step through the reduceAsserts function line-by-line.

First, we write the asserted variables using tell:

tell $ Union vars

Next, we grab the theory from our state using get:

theory <- get

Next comes a tricky part. Our theory is just a list of clauses. We're going to map across that list using the local reduceClause function:

let (reducedTheory,denials) = eitherMap reduceClause theory

The reduceClause function wants to return one of two kinds of results for each clause it processes: either a set of variables to be denied, if the clause contains a newly asserted variable, or the unaltered clause itself, if it does not. We use Either to distinguish these different kinds of results, using eitherMap to partition the resulting lists in to a reduced theory, and a list of sets of variables to be denied.

We then adjust our state:

put reducedTheory

and make the next call if there were any denials made:

unless (null denials) $ reduceDenials (unions denials)

An analysis of reduceDenials is similar.

Finally, our top-level solver does little more than provides the necessary shims around a call to reduceAsserts:

lsolve :: Solver lsolve board = [mkBoard . execReduction $ reduceAsserts vars] where vars = Map.foldMapWithKey (curry Set.singleton) . getMap $ board execReduction r = execWriter $ execStateT r initialTheory mkBoard = Board . foldMap (uncurry Map.singleton) . getUnion

The Solver :: Board -> [Board] is general enough to handle the case of a backtracking solver working on an underdetermined problem (i.e., one that admits multiple solutions). The current lsolve function has to conform to this type, and so it returns its result in a seemingly unnecessary list. It's following a convention.

While it's clear that any Sudoku that the logic based solver can solve can also be solved by humans using simple logic without backtracking, the converse is not entirely clear. I.e., there may be logical deductions that a human reasoner could use that can't be captured by this simple system. Still, in my experience, every published Sudoku I've encountered (excepting those few that specifically mention the need for backtracking) can be solved by this solver. Of course, this may only mean that the people who are publishing Sudokus are using generators built according to the same principle's we're using here.

The Generator

There's a simple approach for transforming a Sudoku solver into a generator:

There is actually very little code involved. First, we'll need our usual random state monad:

type RandState = State StdGen Which we use to write a function for generating a random permutation:

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

This code implements a simple idea. For each element a of the original list, we'll create a pair ($r_a$,a) where $r_a$ is a random integer. We'll then sort the list of pairs on their first element, which will have the effect that the random $r_a$'s will “carry” their associated a's. We then extract the carried elements from the pairs.

A minor subtlety is in deciding what it means for a solver to solve a Sudoku instance. The complexity comes because the backtracking solver and the logic-based solver “fail” on consistent boards in different ways: the backtracking solver returns multiple solutions, the logic solver returns a single, incomplete solution. We'll unify this via:

solves :: Solver -> Board -> Bool solves solver board = case solver board of [x] -> isComplete x _ -> False

There's a minor subtlety in the code. We don't try to count the number of solutions, because the backtracking solver may return a combinatorial number of solutions on an underspecified board, and there's not enough time in the history of the world for today's computers to generate and count them all. The code as written generate at most two solutions.

Finally, we have the search routine itself:

generate :: Solver -> RandState Board generate solver = do constraints <- Map.unions <$> ( for positions $ \pos -> do Map.singleton pos <$> permute [1..9] ) let answer = head $ backtrack (constraints Map.!) (Board Map.empty) prune answer <$> permute positions where prune = foldl $ \board pos -> let newBoard = Board . Map.delete pos . getMap $ board in if solver `solves` newBoard then newBoard else board

This is fairly simple code. First, we generate a random set of constraints for our modified backtracking solver to use in searching for a solution, and use them in finding a solution to the empty board. This is our random answer. Then we generate a random permutation of the positions, which the prune function does a foldl over, deleting positions from the board doing so results in a solvable instance. Note that foldl seems natural here, as we're not building recursive structure.

Code

The code for this lecture can be found on GitHub:stuartkurtz/Sudoku. The state of this code is a bit rough, especially the top-level driver, but it is useful as it stands. Note that the program can be used to generate "hard" instances of Sudoku, i.e., instances that can be solved by a backtracking solver, but not the logic based solver. This might be useful if you want to frustrate your sudoku-playing friends. The instance sudoku-3.txt is particularly interesting in this regards: the logic based solver makes almost no progress at all towards a solution.

Also note that the code is designed for pedagogical purposes rather than efficiency. Still, it's not bad—on my main work machine (a 2010 Mac Pro—still a very capable machine!), it will generate a Sudoku problem in a little less than a quarter of a second. This compares very favorably with the first version of this code, written in about 2000 in C++, which took about 2 1/2 minutes to run, but it's a sloth compared to my most efficient version—also written in Haskell—which runs in about 1/40th of a second!