minisat-solver: High-level Haskell bindings for the MiniSat SAT solver.

[ library, logic, mit ] [ Propose Tags ]

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 [faq] 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
Category Logic
Home page
Uploaded by PeterSelinger at Mon Oct 24 19:15:28 UTC 2016
Distributions NixOS:0.1
Downloads 514 total (16 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs uploaded by user [build log]
All reported builds failed as of 2016-11-19 [all 2 reports]




Maintainer's Corner

For package maintainers and hackage trustees