[Haskell-cafe] ANN: incremental-sat-solver

[Denis Bueno]

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
> incrementally.

Nice!

> The implementation is not sophisticated at all but uses the basic DPLL
> algorithm with unit propagation.
>
> The package is available at:
>
>  <http://hackage.haskell.org/cgi-bin/hackage-scripts/package/incremental-sat-solver>
>
> 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.

    http://hackage.haskell.org/cgi-bin/hackage-scripts/package/funsat

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.

    http://github.com/dbueno/funsat/tree/master

                                  Denis