The incremental-sat-solver package
This Haskell library provides an implementation of the Davis-Putnam-Logemann-Loveland algorithm (cf. http://en.wikipedia.org/wiki/DPLL_algorithm) for the boolean satisfiability problem. It not only allows to solve boolean formulas in one go but also to add constraints and query bindings of variables incrementally.
Properties
| Versions | 0.1, 0.1.1, 0.1.2, 0.1.3, 0.1.4, 0.1.5, 0.1.6, 0.1.7 |
|---|---|
| Dependencies | base, containers, mtl |
| License | BSD3 |
| Author | Sebastian Fischer |
| Maintainer | sebf@informatik.uni-kiel.de |
| Stability | experimental |
| Category | Algorithms |
| Home page | http://github.com/sebfisch/incremental-sat-solver |
| Bug tracker | mailto:sebf@informatik.uni-kiel.de |
| Source repository | git clone git://github.com/sebfisch/incremental-sat-solver.git |
| Upload date | Wed Jan 28 20:16:07 UTC 2009 |
| Uploaded by | SebastianFischer |
| Built on | ghc-6.10, ghc-6.12 |
Modules
- Data
- Boolean
Downloads
- incremental-sat-solver-0.1.tar.gz (Cabal source package)
- package description (included in the package)