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 with the '--enable-benchmarks' option.
Downloads
- minisat-solver-0.1.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
Versions [RSS] | 0.1 |
---|---|
Change log | ChangeLog |
Dependencies | base (>=4.6 && <5), containers, transformers [details] |
License | MIT |
Copyright | Copyright (c) 2016 Peter Selinger, Copyright (c) 2015 Takahisa Toda, Copyright (c) 2005 Niklas Sorensson |
Author | Peter Selinger |
Maintainer | selinger@mathstat.dal.ca |
Category | Logic |
Home page | http://www.mathstat.dal.ca/~selinger/minisat-solver/ |
Uploaded | by PeterSelinger at 2016-10-24T19:15:28Z |
Distributions | LTSHaskell:0.1, NixOS:0.1, Stackage:0.1 |
Reverse Dependencies | 2 direct, 4 indirect [details] |
Downloads | 1609 total (20 in the last 30 days) |
Rating | (no votes yet) [estimated by Bayesian average] |
Your Rating | |
Status | Docs uploaded by user [build log] All reported builds failed as of 2016-11-19 [all 2 reports] |