Redwood forest

Fun

Sudoku

The translation between Sudoku and Boolean Satisfiability is actually very straightforward, even if it at first may seem a stretch to view Sudoku as an instance of some esoteric problem involving Boolean logic. I wrote a couple of scripts to do the translation & automate the solution using MiniSat, and I thought they might be fun for people interested in using SAT for weird things like Sudoku. To run them, transcribe the Sudoku puzzle into a text file like medium25.sdk:

9x9
836
95____4
149
__69_52
9___1___8
73_26
_2_8_1___
_7____96_
5___7___2

Make sure MiniSat is on your $PATH, then run * sudoku.sh medium25.sdk

In the same directory as the translation scripts * sudokuTranslator.pl * sudokuExtractor.pl

... and you'll see the puzzle solved as text:

841 539 726 
295 768 341 
763 124 895 

386 945 217 952 617 438 417 382 659

624 891 573 178 253 964 539 476 182

If you're interested in viewing the CNF which the Sudoku puzzle is transformed into, just take a look at the .cnf file generated by the sudokuTranslator.pl script.

That's it!