Sudoku as a SAT problem
April 8th, 2007 at 9:51 amI have just posted a new program (a collection of Ruby scripts, really) to the programs and code page. It is an implementation of a Sudoku solver - an unusual one. The Sudoku is converted into a boolean satisfiability problem (SAT), which is then solved with a SAT solver.
Once I had a task at work of doing some coding for a SAT solver.
To learn more about SAT solvers, I read some papers and tutorials about DPLL - an algorithm to solve SAT which is used as the basis for many modern solvers. To consolidate my understanding of the algorithm, I wrote a short document (dpll.pdf in the package) and coded the algorithm in Perl. The implementation is very simplistic because no heuristic is used. Real SAT solvers are all about complex, sophisticated heuristics.
When Sudoku became popular, I solved a few and quickly reached a conclusion that I don’t find these puzzles interesting. The solution process just felt too mechanic, and reminded me of manually solving a boolean formula for satisfiability (SAT) - the same approach of applying clearly defined inference rules over and over again until a solution is reached. So I searched the net a little (the Google search “sudoku sat” should get you started) and
came upon a few interesting websites and articles that discuss representing Sudoku as a SAT problem. Since I already had a (very) modest SAT solver of my own, I decided to implement the other half of the problem and make it all work together to actually solve Sudokus.
At the same time I started being interested in Ruby, so I wanted to combine the interests and code the solver in that language. I’ve rewritten my Perl SAT solver in Ruby and added a Sudoku solver, which is capable of solving even the hardest Sudokus without any guessing, as far as I know of.
Download the package from here.
Related posts:
April 8th, 2007 at 12:23
very good point!
April 25th, 2007 at 20:39
Looking at the code, where do you perform the rule 3 resolution?
April 25th, 2007 at 21:37
Phil,
I don’t implement the resolution in my SAT solving code, because the data structure I currently use makes it very inefficient. My SAT solving code is trivial, and the data structure is trivial - a mere array of arrays. Real SAT solvers keep separate track for each literal of its appearances. Then, resolution can be actually applied efficiently.
October 24th, 2007 at 06:17
Sudoku is very funny
September 4th, 2008 at 11:38
can u give a good reference for satisfiability problem?
this is because i have to report for this and i want to have a thorough understanding on it first
September 5th, 2008 at 08:25
Loi,
Start with Wikipedia: http://en.wikipedia.org/wiki/Boolean_satisfiability_problem