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.

Properties

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
Maintainer selinger@mathstat.dal.ca
Category Logic
Home page http://www.mathstat.dal.ca/~selinger/minisat-solver/
Uploaded Mon Oct 24 19:15:28 UTC 2016 by PeterSelinger
Distributions NixOS:0.1
Downloads 48 total (7 in the last 30 days)
Votes
0 []
Status Docs not available [build log]
All reported builds failed as of 2016-11-19 [all 2 reports]

Modules

  • SAT
    • SAT.MiniSat

Downloads

Maintainer's Corner

For package maintainers and hackage trustees