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!


Welcome Research Software Publications Photos Music Fun	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!