[Haskell-cafe] ANN: incremental-sat-solver
dbueno at gmail.com
Thu Jan 29 00:45:01 EST 2009
On Wed, Jan 28, 2009 at 13:32, Sebastian Fischer
<sebf at informatik.uni-kiel.de> wrote:
> 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
> 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.
Funsat is also a library.
The code is structured in a way that it would possibly be
straightforward to do incremental solving, but it is not designed for
it. (If interested, see the function `Funsat.Solver.solveStep'. It
is not exported, but it could be.)
If you're interested, my code is also on github, and includes some
benchmark CNF problems in the bench/ subdirectory.
More information about the Haskell-Cafe