High-level Haskell bindings for the MiniSat SAT solver. http://www.mathstat.dal.ca/~selinger/minisat-solver/
|Latest on Hackage:||0.1|
This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.
This package provides high-level Haskell bindings for the well-known
MiniSat satisfiability solver. It solves the boolean satisfiability
problem, i.e., the input is a boolean formula, and the output is a
list of all satisfying assignments.
MiniSat is a fully automated, well-optimized general-purpose SAT
solver written by Niklas Een and Niklas Sorensson, and further
modified by Takahisa Toda.
Unlike other similar Haskell packages, we provide a convenient
high-level interface to the SAT solver, hiding the complexity of the
underlying C implementation. It can be easily integrated into other
programs as an efficient turn-key solution to many search problems.
To illustrate the use of the library, two example programs are
included in the "examples" directory; one program solves Sudoku
puzzles, and the other solves a 3-dimensional block packing
problem. These programs can be built manually, or by invoking Cabal
Initial public release.