@hackage minisat-solver0.1
High-level Haskell bindings for the MiniSat SAT solver.
Categories
License
MIT
Maintainer
selinger@mathstat.dal.ca
Links
- Homepage
- Documentation
- No source repository
- Changelog
- Security
Versions
- 0.1 Mon, 24 Oct 2016
Installation
Dependencies (3)
- base >=4.6 && <5
- containers
- transformers Show all…
Dependents (2)
@hackage/haskell-tools-builtin-refactorings, @hackage/acme-everything
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 with the '--enable-benchmarks' option.