minisat-solver: High-level Haskell bindings for the MiniSat SAT solver.
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
|Dependencies||base (>=4.6 && <5), containers, transformers [details]|
|Copyright||Copyright (c) 2016 Peter Selinger, Copyright (c) 2015 Takahisa Toda, Copyright (c) 2005 Niklas Sorensson|
|Uploaded||by PeterSelinger at 2016-10-24T19:15:28Z|
|Downloads||841 total (12 in the last 30 days)|
|Rating||(no votes yet) [estimated by Bayesian average]|
Docs uploaded by user [build log]
All reported builds failed as of 2016-11-19 [all 2 reports]
For package maintainers and hackage trustees