How to Solve the Sudoku Puzzle with programming

A picture of a computer that has nothing to do with sudoku

A Sudoku Puzzle is a famous Japanese puzzle. In it you solve a 9 by 9 grid of numbers, but you don’t need to do any math to solve the sudoku puzzle! In each number you put a row and column, and also a number in each box.

A sudoku puzzle. The steps below do not use it.

We will solve the Sudoku Puzzle with programming, by writing a program that solves the Sudoku Puzzle. This can be done in any programming language. For a junior programmer, a programming language is something like Angular or Blockchain, while for a senior developer, a language is Ruby or Python.

Solving the Sudoku Puzzle is three easy steps.

2. Find the right data structure

data structure quote

A program is data structure + algorithm. To solve the Sudoku Puzzle, you need a data structure and algorithm. A data structure is a linked list, a red-black tree, or another data structure.

The Sudoku Puzzle is a 9x9 grid, so an array is the right data structure. What goes in the array? If the Sudoku Puzzle has “a four is in the first row, first column”, then it also has:

A one is not in the first row, first column.
A two is not in the first row, first column.
A three is not in the first row, first column.
A five is not in the first row, first column.
A six is not in the first row, first column.
A seven is not in the first row, first column.
A eight is not in the first row, first column.
A nine is not in the first row, first column.

Or, in programming:

!911 & !811 & !711 & !611 & !511 & 411 & !311 & !211 & !111

So the right data structure is one 9x9 array of booleans per number. Senior engineers who use Ruby or Python, which have 3D arrays, will use arrays of arrays, for a 9x9x9 array of booleans. We will use this data structure with an algorithm to solve the Sudoku Puzzle.

3. Write the requirements

'There are two hard problems in CS: Cache invalidation and naming things', with a picture of Albert Einstein.

A program is data structure + requirements + algorithm. The requirements of a Japanese Sudoku Puzzle are:

Each number cell has exactly one number
Each number appears exactly once in every row, column, and 3x3 box
Each number appears exactly once in every column.

As programmer’s start with a simpler problem (rule 1): the requirement that there’s exactly one 3 in the top row of a Sudoku Puzzle. That is

There is a 3 in the top row of a Sudoku Puzzle, AND

(311 | 312 | 313 | 314 | 315 | 316 | 317 | 318 | 319) &

3 isn’t in columns 12345678, OR 3 isn’t in columns 12345679, etc

(
  (!311 & !312 & !313 & !314 & !315 & !316 & !317 & !318       ) |
  (!311 & !312 & !313 & !314 & !315 & !316 & !317 &        !319) |
  (!311 & !312 & !313 & !314 & !315 & !316 &        !318 & !319) |
  (!311 & !312 & !313 & !314 & !315 &        !317 & !318 & !319) |
  (!311 & !312 & !313 & !314 &        !316 & !317 & !318 & !319) |
  (!311 & !312 & !313 &        !315 & !316 & !317 & !318 & !319) |
  (!311 & !312 &        !314 & !315 & !316 & !317 & !318 & !319) |
  (!311 &        !313 & !314 & !315 & !316 & !317 & !318 & !319) |
  (       !312 & !313 & !314 & !315 & !316 & !317 & !318 & !319) 
)

This is good, but it’s wrong: it’s not SOLID. SOLID says that programmers should write Clean Code, and nested boolean expressions are not Clean Code. The very last clause is an AND inside of an OR inside of another AND. To make Clean Code, put the requirements in conjunctive normal form (CNF), with all the clauses written as ANDS of ORs.

The second clause is equivalent to “there is at most one three in the top row”. This is equivalent to saying “of any two elements of the top row, at least one is not a 3.” As an example, take (!311 | !312). If the first element is a 3, then !312 and the clause is true. If the second column is a 3, then !311 and the clause is true.

With this, the requirements in CNF are every pair of disjunctions, which is Clean Code.

( 311 | 312 | 313 | 314 | 315 | 316 | 317 | 318 | 319) & 
(!311 | !312) &
(!311 | !313) &
(!311 | !314) &
(!311 | !315) &
(!311 | !316) &
(!311 | !317) &
(!311 | !318) &
(!311 | !319) &
(!312 | !313) &
(!312 | !314) &
(!312 | !315) &
(!312 | !316) &
(!312 | !317) &
(!312 | !318) &
(!312 | !319) &
(!313 | !314) &
(!313 | !315) &
(!313 | !316) &
(!313 | !317) &
(!313 | !318) &
(!313 | !319) &
(!314 | !315) &
(!314 | !316) &
(!314 | !317) &
(!314 | !318) &
(!314 | !319) &
(!315 | !316) &
(!315 | !317) &
(!315 | !318) &
(!315 | !319) &
(!316 | !317) &
(!316 | !318) &
(!316 | !319) &
(!317 | !318) &
(!317 | !319) &
(!318 | !319)

The suspicious boyfriend meme, with the CNF mess on the left and the original mess on the right.

There are more clauses, but each one is just a conjunct of ors, so the formula is in CNF, which means it is Clean Code, which means it is SOLID. Doing the same for every row, column, and box, gets all of the constraints for the Sudoku Puzzle. Also in a Sudoku Puzzle, two numbers can’t be in the same cell:

(111 | 211 | 311 | 411 | 511 | 611 | 711 | 811 | 911)  &

(!111 | !211) &
 ...

Finally there are clues. These are the Sudoku Puzzle cells that are already filled in. These are also a requirements. Here is how to add “there is a four in the first row and first column” to the CNF.

The Sudoku Puzzle requirements are now in a program. Now we need to write the algorithm for solving a Sudoku Puzzle.

4. Write the algorithm to solve the puzzle

Convert to DIMACS and run PLingeling.

…

Wait, what?

Let’s zoom out a bit. Sudoku is an example of a constraint problem. Most “solving sudoku” tutorials use either backtracking or constraint propagation. These same techniques apply to all constraint problems, and since such problems are so widespread, it doesn’t make sense to custom build an algorithm for every single one. Rather, we want general-purpose constraint solvers we can apply to arbitrary problems.

Real-world constraints, though, get arbitrarily complex. There’s an expressiveness/tractability tradeoff here: the more complex the constraints our solver can handle, the slower it will be (as a rule). Much like we have assembly languages for code, we have data formats for constraint problems. As a rule of thumb, representing a problem in simpler formats lets us use faster solvers.

Fortunately, the constraints for sudoku are extremely simple. As we saw with our inane data structure and requirements, it’s possible to represent every constraint as a boolean formula. This makes Sudoku a Boolean Satisfiability Problem (SAT), meaning we can use a SAT solver to find solutions.

You might have heard that SAT is NP-complete: there’s no polynomial time algorithm we know of to solve it. This is usually presented to CS students as meaning “we can’t solve it in practice”. But SAT problems appear everywhere in industry, meaning there’s a lot of money in making fast SAT solvers.¹ How fast? One of the problems in the 2019 SAT Race had 900,000 variables and seventeen million clauses.² Representing a 9x9 Sudoku takes just 729 variables and 12,000 expressions. That’s child’s play.

First we have to enumerate all of the constraints. They’re all of the form we kinda-sorta-talked about in the last section, so it’s not that hard to write a program to do that bit. I put mine in the appendix if you want to see how it works. After that we just need to put it in the proper format (DIMACS), drop it into a SAT solver (like PLingeling), and we’re done.

If you don’t believe me, you can try it out for yourself! Here’s the CNF for the sudoku up top. You can run it in any sat solver, like this one, and get a solution.

This works for any arbitrary Sudoku. We only need to write the uniqueness constraints once: after that, we can append any particular problem’s set of clues to the base constraints to make the SAT solver work.

Discussion

So should you go and convert all your constraint problems to SAT? Probably not. There’s a couple reasons why this is a bad idea.

First of all, SAT solvers are general purpose solvers. They can’t get as fast as an algorithm specialized to a particular problem. It’s usually easier to learn how to encode a problem in SAT and get something fast enough than it is to master the problem deeply enough to make a solution faster than the SAT solver. But if performance is your #1 priority you’ll be better off writing a custom algorithm.

Second, encoding SAT problems yourself is like writing low-level code. It makes sense in many contexts but most people prefer a higher-level abstraction. That’d be something like an SMT verifier or constraint solver that uses SAT on the back-end. Once again you’re trading devtime for runtime.

Nonetheless SAT solvers are a neat and undercapitalized tool. There’s plenty of people out there that would benefit from knowing about them but don’t. Plus figuring out how to translate your problem domain into “piles ‘n piles of booleans” is a surprisingly fun puzzle.

Did you solve the Japanese Sudoku Puzzle? If so, you may be a senior engineer. We are hiring for senior engineers in Agile, Blockchain, and Full Stack. [Apply Here]().

Thanks to Richard Whaling, Richard Feldman, and Predrag Gruevski for feedback. Hero image by Glenn Carstens-Peters on Unsplash.

Appendix: Getting the SAT

The standard SAT format is DIMACS. Here’s a sample DIMACS format:

c this is a comment
c the line starting with p is the config
p cnf 3 2
1 2 0
3 -1 0

The p line says we have 3 variables and 2 clauses, where each clause is in CNF. Clauses are separated by 0s, and negative numbers represent negations. This SAT problem translates to (x1 | x2) & (x3 | !x1).

As a quick back-of-the-napkin calculation, there are 37 clauses that represent “there is exactly one 1 in the top row”. Multiply by 9 for each row, then triple that to get the constraints for each column and box two, then nonuple that for each number. That gives us ~9000 constraint clauses. We need another (37 * 81) for the “exactly one number per cell” constraint, so we’re looking at maybe 12k total. In practice the number will be slightly smaller, as some of these constraints are redundant, but not many.³ We’re need to programmatically generate them, mostly by repetitive combinatorial transformations over subarrays.

You know what that means? That’s right, it’s J time! I have a love-hate relation with this dang language but it actually, for once my life, is the appropriate choice here. So let’s sling some J! If this is your first exposure, then 1) I envy you, and 2) you can read more about it here.

The J should be self explanatory:

ns =: (~:/"1) # ]
dd =: ~.@:(_2 ]\ ,)@:(/:"1~)
uniq =: ns@:dd@:(>@{@;~@,)"1


NB. what is WRONG with me

On second thought, maybe I should write an explanation of how this all works. That’ll be another 1500+ words, though, and this post is long enough as it is, so I put it at this link here.

And this one, click me to see how the J script works!

This surprises a lot of people: if the only algorithms are nonpolynomial time, how can it be so fast? Two ways. First of all, NP-complete is about asymptotic complexity: if we can drive down the constants, it takes longer for the complexity to blow up. Second, it’s the worst-case complexity. The average time complexity can be extremely low as long as at least some inputs have exponential blowup. Most real world problems are “well-behaved”. ^[return]
ex175_17. Most of the 400 problems are smaller, being somewhere between 10k-100k variables and 100k-1mm clauses. ^[return]
the constraint that “there’s only one 3 in the first box” overlaps slightly with “there’s only one 3 in the first row”. ^[return]