Copyright (c) 2011 Bart Massey
This is a mostly-Haskell (some Bourne Shell) solver for 9x9 Sudoku instances. It works by encoding the instance as a CNF SAT instance, invoking an off-the-shelf SAT solver, and translating the resulting SAT assignment back into a Sudoku solution.
Thus, the software consists of a very simplistic encoder of 9x9 Sudoku instances into CNF SAT instances, together with a very simplistic decoder of SAT assignments of these instances into solved Sudoko instances, and a shell script that automates the whole process.
The solvers currently supported by the shell script are
picosat and minisat2, which are available in
Debian. However, most any decent SAT solver should be
workable. You will also need an installation of ghc,
including the runghc command. Once you have that, you can
try, for example:
sh sudoku-sat.sh sudoku-9x9/sudoku-skiena-prob.txt
Take a look at the sudoku-9x9 directory for examples of the
input format. The output format is the same. The sample
problems are autogenerated by me using software I wrote and
had lying around somewhere, with the exception of
sudoku-skiena-prob.txt. That one was taken from
Skiena's Algorithms book.
-
The decoder should check that the solution returned is a valid Sudoku, and probably should check that it is valid for the input instance.
-
Standard 9x9 Sudoku is currently hardwired in. You could easily change it to 16x16, but only by changing a constant in the encoder and in the decoder. You'd also have to change the input and output to deal with e.g. letters instead of digits.
This work is licensed under the "MIT License". Please see
the file COPYING in the source distribution of this
software for license terms.