The minisat-solver package

[Tags:benchmark, library, mit]

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.


Versions 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
Stability Unknown
Category Logic
Home page
Uploaded Mon Oct 24 19:15:28 UTC 2016 by PeterSelinger
Distributions NixOS:0.1
Downloads 44 total (9 in the last 30 days)
0 []
Status Docs not available [build log]
All reported builds failed as of 2016-11-19 [all 2 reports]


  • SAT
    • SAT.MiniSat


Maintainer's Corner

For package maintainers and hackage trustees