[Haskell-cafe] ANN: incremental-sat-solver
sebf at informatik.uni-kiel.de
Wed Jan 28 15:32:16 EST 2009
Simple, Incremental SAT Solving as a Library
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.
The implementation is not sophisticated at all but uses the basic DPLL
algorithm with unit propagation.
The package is available at:
Unlike 'sat' and 'sat-micro-hs' it is a library, and unlike 'libsat'
it provides an interface for incremental solving. On the other hand,
the implementation is much simpler (and probably less efficient) than
'libsat's. You are invited to improve on that, if you like. The code
is on github:
More information about the Haskell-Cafe