SAT based Sudoku solver in Python

(Ilan Schnell, Continuum Analytics, April 2nd, 2013)

The Boolean satisfiability problem can be solved extremely efficiently using SAT solvers. Over the past 20 years, SAT solvers have drastically improved. In the early 90’s SAT solvers could only handle a few hundred variables and clauses, whereas today problems with millions of variables and clauses can be solved quickly. Most of these advances are due to better algorithms, not due to better hardware. A large set of problems, ranging from logistics, planning, and verification can now be solved using SAT solvers, of which there are many competitive open source implementations. PicoSAT is one of those solvers written in pure C, to which I recently wrote the pycosat Python bindings on the C level. The pycosat package is already available in Anaconda by using the install command conda install pycosat.

The SAT-based Sudoku solver is an example, which demonstrates the usefulness of the pycosat package. It is based on a paper from 2005, which explains in detail how the Sudoku problem is translated into a satisfiability problem. Basically, for each possible digit (1-9) in the 81 Sudoku cells, we assign a Boolean variable. It turns out that the Sudoku problem translates to (up to) 729 variables and 11,745 clauses. The pycosat source code contains the Sudoku solver (less than 100 lines of Python code with many comments — 40 lines of actual code).

Solving a hard Sudoku puzzle only takes 40 milliseconds on my laptop. However, half of that time is spent setting up the Sudoku clauses, so that solving the actual SAT problem only takes 20 milliseconds. In contrast, when solving Euler project problem 96 many years ago, I wrote a backtracking based Sudoku solver which chews for 15 seconds on the same puzzle.

Summary

The Sudoku problem translates quite nicely into a SAT problem. Having a fast SAT solver available in the Python runtime makes it easy to write a very efficient Sudoku solver in pure Python, which can solve even hard Sudoku puzzles in a matter of tens of milliseconds. Given the extensive research that has been devoted to the SAT problem, it is worth revisiting applications which require solving constraint problems. In many cases, translating the problem into a SAT problem will require less effort than solving the original problem yourself. Moreover, using a SAT solver will allow you to take advantage of the extensive research which has been done in this field over the last 20 years. In addition, your code will most likely be shorter, easier to reason about, more readable, easier to maintain, and run faster.