Sudoku Satisfiability

Modern neural networks are becoming increasingly powerful perceptual machines but their ability to perform logic is still rudimentary at best. The early days of AI research focused on logic and symbol manipulation and for many decades computers have had super human logical capabilities (in some respects anyway). Recently there has been a surge of interest in trying combine modern neural architectures with classical symbolic/logical AI. These sorts of systems are starting to be described as "neuro symbolic AI". I think the general idea of incorporating sophisticated exact logical systems into a framework alongside fuzzier more "intuitive" perceptual systems is a very interesting idea.

What does this have to do with Sudoku you ask? Sudoku is exactly the sort of problem that is relatively easy to tackle with classical AI techniques and somewhat awkward to tackle using nothing but neural networks (not that it isn't fun and interesting to try see for example the many notebooks using tthis million puzzle sudoku dataset).

But with a little work you can encode sudoku as one of a standard sort of constraint satisfaction problem like a linear program or a boolean satisfiability problem. With such systems you can quickly and efficiently find solutions which you can be extremely confident will be 100% correct. By contrast if I were presented with for example a multi-layer perceptron or convolutional neural net which showed 100% prediction accuracy on a test set of a few hundred thousand boards I would not be convinced that the network truly had learned a function which was actually a perfect sudoku solver, it would be much more likely that it had somehow learned a close (but imperfect) approximation to such a thing. I certainly would not say that such a neural network would "understand" sudoku in any meaningful way. Though if I'm being honest I also do not think that the expression of the rules of sudoku in propositional logic represents a much stronger form of "understanding" in the human sense.

I have a lot more knowledge and experience with neural networks than I do with logical inference. But I have been wanting to add some logic based tools to my toolbox. The ability to do complex exact logical inference is useful even if I never apply it in my work as an ML practitioner. I have some experience with linear programming but I have never used a satisfiability solver before for anything and thinking through how to encode sudoku into a satisfiability problem seemed like it would be a good exercise to help me become more familiar with those sorts of logical systems.

Sudoku as a Linear Program¶

Lets start with how to encode sudoku as a linear program. A linear program is a type of constrained optimization problem where both the constraints and the objective function are linear functions of the variables. In this particular case there is no objective other than to satisfy the constraints and so any objective function will do. It may not at first seem like sudoku would be the sort of thing which you could "linearize". But it is possible to do if we take advantage of the fact that we have complete freedom in terms of what variables we use to represent a board.

The natural way to represent a sudoku board, solved or unsolved, is of course a 9x9 grid of integers between 1 and 9. Or perhaps I should say that is how you would likely present a sudoku board to a human. But that is not the only possible representation and not necessarily the most convenient way to represent a sudoku board to a computer and it isn't what we will mostly use in this post.

A More Algorithm Friendly Representation¶

nstead of a 9x9 grid of variables whose values are between 1 and 9 it turns out to be much nicer to work with a vector of $9*9*9=729$ variables with values between 0 and 1. These varaibles correspond to every possible combination of row, column, and digit. With a 1 representing that the particular combination of row, column, and digit actually occurs in a given board and a 0 indicates that combination does not occur.

Lets denote these variables as

$x_{r,c,d}$

So for example $x_{1,2,5}=1$ would indicate that the second column of the first row contained the digit 5. and likewise $x_{2,5,3}=0$ would indicate that the digit contained in row 2 column 5 is not a 3. We want these indicator variables to be either exactly 0 or exactly 1 but linear programs only work on convex spaces so we will make do with constraininng the values of x to lie between 0 and 1 inclusive.

$$0 \leq x_{r,c,d} \leq 1$$

Represented in this way a valid sudoku board is one such that for the set of digits,

$$ D = \{1,2,3,4,5,6,7,8,9\} $$

We can express the constraint that each row have at least one of each digit by summing up indicator variables over columns with one such sum constraint per digit.

$${\large \sum_{c \in D} x_{r,c,d} = 1 ~{\rm for}~r,d~\in D}$$

We can incorporate the same sort ofconstraint for columns by summing over row indexes,

$${\large \sum_{r \in D} x_{r,c,d} = 1~{\rm for}~c,d~\in D} $$

and finally we can ensure that each box contains at least one digit by summing over the (row, column) pairs corresponding to each box,

$${\large \sum_{(r,c) \in box_i} x_{r,c,d} = 1 ~{\rm for}~i,d~\in D}$$

The first time through this excercise those three sets of constraints seemed like enough. After all those three constraints are the rules of sudoku as we tend to explain them to other humans. But strictly speaking there is nothing in the above set of constraints that requires that we assign only a single number to any particular location in the grid. For that we neeed to also add a set of constraints for each grid position that ensures that at least one digit is assigned to it.

$${\large \sum_{d \in D} x_{r,c,d} = 1~{\rm for}~r,c~\in D} $$

This last constraint taken together with the others imply that each cell will be assigned exactly one digit.

Initial Board Constraints and Fractional Solutions¶

But "wait a minute" I can almost hear you say, what is to prevent us from finding "solution" which have entries somewhere between 0 and 1? There is seemingly nothing to prevent us from for example considering a solution with $x_{1,1,1} = 1/2$ and $x_{1,1,2}=1/2$ or any other such fractional solution?. You would be correct in thinking that such solution vectors might indeed be able to satisfy the linear constraints without yeilding proper sudoku boards. You would be right to worry since in fact the above linear equalities actually hold not just for any one particular sudoku board but for all valid sudoku boards.

The $x$ vector corresponding to any valid sudoku solution will satisfy the above equalities. If that vector consists only of entries which are either exactly 0 or 1 then that vector corresponds to one possible sudoku board. However, any convex combination of two (or more) such vectors will also satisfy the same set of constraints but will have fractional entries and doesn't have any clear interpretation as a proper sudoku board.

In other words the above linear constraints describe the convex hull of valid sudoku boards instead of a unique sudoku board. But we haven't yet considered the constraints that come from knowing the cells on the board which have already been filled in. Each cell whose value we know adds 9 additional linear constraints specifying the 9 associated entries in the board vector. If the sudoku board in question is well posed then it must have a single unique solution. In terms of the admissible region of solutions for our linear program this translates to the requirement that when we add the extra constraints coming from the known initial cells of the problem the admissible region must shrink down to a single point! To see that this must be the case suppose that the admissible region of the linear program had some amount of extension. If it isn't exactly 0 dimensional (a single point) then the permissible region must be at least 1 dimensional. All of the constraint hyper planes cut exactly through some subset of the vertexes of the convex hull of possible boards and each of these vertexes represent completely valid sudoku boards. Which means that if our constraints are loose enough to include some interior region of improper fractional solutions then that set of permissible solutions must also contain at least 2 vertexes of the convex hull of all sudoku boards, but that would mean that the initial board conditions permitted more than one solution.

Or to put it simply the requirement that our initial board contains enough information to solve the puzzle is exactly the same as saying that the linear constraints are tight enough to restrict the space of admissible solution vectors to just one point, neat!

Variable Indexing¶

It is helpful to be able to translate between any particular combination of row, column, and digit to a single flat variable index (and back). Since this is very much like indexing into a multi dimensional array of shape (9, 9, 9) we can use the numpy utilities for translating between multi dimensional indexes and flat "raveled" indexes. The numpy function ravel_multi_index takes us from a tuple of indexes into a multi dimensional array to an index into a flat array of a given shape, and we can reverse that transform and go from a flat index back to a multi dimensional index using the numpy function unravel_index. This trick is very useful every once in a while.

Doing things this way it is more convenient to begin the indexing at 0 for the digits so we will index what would normally be the digit "1" on the board as number index 0.

using the same trick we can also easily calculate an index for the 3x3 boxes that each digit belongs to.

The sudoku rules can be succinctly restated in that each row, column, and box must have exactly one of each digit contained in it. In our expanded set of indicator variables for each (row, column, digit) triplet we can re express this as a sum over certain subsets of indicator variables which are mutually exclusive with each other. Namely exactly one of the indicator variables for any given row and digit combination may be "turned on" and likewise for each column and box.

For reasons that will become clear later we will compute our constraints in terms of the indexes of these sets of mutually exclusive indicator variables. These will be the indexes of the non-zero entries in our linear constraint matrix for our linear program.

Lets translate these sets into the coefficients of a set of vectors in dense matrix and take a look.

Test Board¶

The dot product of the vector of indicator variables with each one of these constraint vectors tests one of the sum constraints mentioned at the beginning of this post. If the dot product of the vector corresponding to a particular board with each of the constraint vectors is equal to 1 then that board is a valid sudoku board (assuming that the entries in the vector can be equal to either 0 or 1).

Lets take a look at a real sudoku puzzle and solution and check that the corresponding vector of indicator variables has a dot product of 1 with each of our constraint vectors. The below puzzle is gleaned from the million puzzle dataset I mentioned above.

As mentioned earlier it simplifies our indexing to subtract 1 from the entries on the sudoku board so we will let the entries on a sudoku board run from 0 to 8 instead of 1 to 9, and let an entry of -1 indicate an unknown entry.

The vector corresponding to the solved board does indeed satisfy all our linear constraints. That is a nice little sanity check on our above code.

Now lets see if we can coax a linear program solver into finding this solution starting from the partially filled in puzzle.

Scipy Optimize Linprog¶

There is a modestly powerful linear program solver available in the scipy.optmize module linprog. Since most people will already have this in their python distribution of choice lets start there.

Conveniently we can encode the initial board conditions as additional existence + uniqueness constraints on individual indicator variables so we can just reuse the same code we used for generating the shared row/colmn/box constraints.

Great! the linear program found a solution which satisfies all our constraints which should mean that we have solved the puzzle! This is a well formed puzzle so there can be just one solution and so the solution vector should be exactly equal to the indicator vector we calculated above.

Lets make a transform which accepts a valid indicator variable vector and returns a the corresponding board so that we can take a look at the result and see if it is indeed correct.

First as a sanity check lets make sure that this acts as an inverse of our board to indicator vector encoding up above by passing a few hundred random boards through them.

So far so good, now lets appy this same transform to the prospective solution vector and see what we found.

Woot! The solution to the linear program netted us the correct solution to the sudoku puzzle.

Like I mentioned above this works because the linear constraints are tight and so there is only a single unique point in the space of 729 indicator variables that satisfies them all. However if the puzzle being posed had more than one answer then we would get back a vector which could be any vector within the convex hull of the vectors corresponding to possible solutions.

Lets get rid of enough of the initial cell value conditions to make sure that the puzzle doesn't have a unique solution and solve the linear program again and see what happens.

Sudoku and Boolean Satisfiability¶

Even though we can encode the constraints of a sudoku problem as a linear program the fact that we haven't even used the objective function is certainly a sign that the language of linear program optimization is a little bit of an awkward match for sudoku.

Sudoku is at its core a very particular kind of logic puzzle. Any (finite) logic puzzle can be rewritten into an equivalent set of logical statements which deal only with binary true/false variables. The general class of such problems is called a boolean satisfiability problem. In fact any sort of problem for which a computer can compute a solution can be translated into a boolean satisfiability problem or more precisely boolean satisfiability problems are NP-complete.

In order to translate sudoku into a boolean satisfiability problem we need to do three things.

• Encode the board state into a series of true/false statements which we call "variables"
• Encode sudoku game rules as boolean logic statements in terms of the board state variables
• Translate all these statements into Conjunctive Normal Form

Thankfully we have already done the first step of figuring out a good way to encode the board state in a series of indicator variables up above. The second and third steps will require a little additional work on our part. Lets start with the third.

Conjunctive Normal Form (CNF) is a standard way to encode a series of logical statements over boolean variables in order to make manipulation and solving algorithms easier to code and reason about. In boolean algebra the OR'ing together of two statements is called a "disjunction" denoted by $\lor$ and the AND'ing together of variables is called a "Conjunction" and is denoted by $\land$ and the negation of a variable (NOT) is denoted $\lnot$.

In a general boolean statement we can apply conjunction, disjunction, and negation to any variables or any combination of variables in any order. A statement is said to be in CNF if it looks like a conjunction of disjunctions of base variables or their negations.

So for example let A and B be our basic boolean variables

$$\lnot(A \lor B)$$

is not in CNF because we can only negate the base variables not whole statements. The equivalent CNF statement in this particular case happens to be one of de Morgan's laws.

$$ \lnot(A \lor B) = \lnot A \land \lnot B $$

and something like

We can always translate any boolean statement into an equivalent statement in CNF though figuring out exactly how to do so can be a little tricky.

Pycosat¶

The boolean satisfiability tool that we will be using is pycosat, which is a python wrapper for the picosat solver. The pycosat documentation seemed a little opaque to me and it took me a little while to figure out how to translate between its list of lists of integers format and the associated CNF.

For pycosat we specify a list of clauses with each clause being a list of integers. A positive integer represents a base boolean variable and the negative of that integer represents the negation of the corresponding variable. The individual clauses are then combined together by conjunction.

So the python list,

Represents the statement

$$ (\lnot x_1 \lor x_2) \land (\lnot x_2 \lor x_3) \land \lnot x_3 $$

Which can only be true if all three of $x_1, x_2, x_3$ are false.

Quantified Logic¶

When I first sat down to figure out how to try and encode the rules of sudoku into a set of boolean statements (any statements not necessarily in CNF) I completely drew a blank. I tried a few different things but I simply couldn't wrap my head around the problem at all. Eventually I realized that what I needed was a set of higher level statement which would be more useful to me as a human and which I could also compile down into a collection of low level boolean clauses.

It is often much more natural to deal in terms of quantifiers which are logical statements about the sizes of sets. The most common quantifiers, which you are almost certain to be famiiliar with are "there exists" $\exists$ and "for all" $\forall$.

In the case of sudoku I realized that what I really needed was a high level statement that in particular groups of indicator variables that there was exactly one of them that was true. In the language of linear programming this worked out to saying that the sum over those groups of indicator variables was equal to 1.

The "Exactly One Of " Quantifier¶

Translating the statement that a particular set of indicator variables $\{x_1, x_2...\}$ has exactly one true member into CNF turns out to be a little tricky. We can decompose the statement into two parts, at least one of the variables must be true and at most one of the variables can be true.

Expressing "at least one of these variables is true in CNF is easy it is just the disjunction of all the variables in that set.

$x_1 \lor x_2 \lor x_3 \dots$

But the statement "at most one of these variables is true" doesn't have an immediately obvious translation into CNF. But a little googling reveals a good trick for this.

Suppose that more than one of the variables were to be true. Is there an easy way that we can detect that situation via some statements in CNF? Well if there is a pair of statements both of which are true then for that pair of statements $(\lnot x_i \lor \lnot x_j)$ will be false. But if only one of the base variables is true then all such negation pairs cannot be true since at least one variable in each clause containing more than one variable must be false.

Therefore the conjunction of the negations of all possible pairings of the base variables is true if and only if at most one of the base variables is true. That is quite a moutful but fortunately it is maybe a little easier to put succinctly into code than it is to say in words.

Lets make a set of helper functions which take lists of integer variable indentifiers and translate them into the appropriate lists of clauses in CNF.

With these functions in hand we can easily leverage the same set of constraint sets that we generated up above to create a set of clauses in CNF which encode the rules of sudoku as a satisfiability problem.

There is just one additional wrinkle to deal with which is that because we chose to 0 index the variables the indicator variable that corresponds to labeling row=0,col=0,num=0 is indexed by variable 0. But because pycosat uses the sign of the integer label for each variable to indicate negation it does not allow variables to be referred to by the integer 0. So to fix this we will need to add 1 to all of the variable indexes we used above for the linear program solving stuff.

A Sudoku Generator¶

Now that we have made a couple of sudoku solvers lets go one step further and figure out how to generate random sudoku puzzles which have a unique solution and a minimal unique set of cells specified. I first pick a random valid solution board and then do a random sweep through all the cells removing them if that doesn't make the puzzle have a non-unique solution.

The resulting puzzles mostly have a number of specified cells somewhere in the range of 22 to 26. The absolute minimum number of cells that can be specified in a 9x9 sudoku puzzle is 17 (something that was just recently proved). So these puzzles are perhaps not the absolutely most minimal possible for each corresponding solution board but they aren't too far off either.

And we can also generate examples of expanded sudoku for larger boards. Though these take quite a while to generate. 16x16 doesn't take too long but 25x25 takes quite a while and I didn't even try 36x36 or larger.