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 8___3___6 _95____4_ ___1_4_9_ __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
... 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!