Sudoku solver using reduction to boolean satisfiability (CNF) and MiniSat to solve - written in Haskell.

A full description of the approach can be found here: http://www.lukedodd.com/?p=5

The only dependency in addition to MiniSat is the Data.List.Split, install with cabal:
$ cabal install Split

A MiniSat binary, version 2.2.0, built on 64-bit linux (ubuntu 10.4) is included.
You can replace this with your own. See http://minisat.se/.

An example puzzle file is included in "puzzles", the format should be self explanatory.
This contains 50 sudoku puzzles - it is from http://projecteuler.net/.
The file "harder-puzzles" contains harder sudoku problems.
This solver performs well on these instances, where other simple solvers may perform very slowly.
The solver also identifies unsolvable puzzles quickly.

=== Compile and Run ===
To compile: ghc sudoku.hs
Run the solver by passing it a puzzle file in the first argument.
i.e. $./sudoku puzzles
The solver expects to find "minisat" in the working directory.