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: <http://hackage.haskell.org/cgi-bin/hackage-scripts/package/incremental-sat-s...
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: http://github.com/sebfisch/incremental-sat-solver Cheers, Sebastian
On Wed, Jan 28, 2009 at 13:32, Sebastian Fischer
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-s...
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
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.
By saying 'libsat' I actually meant 'funsat' ;) I have considered using it instead of writing 'incremental-sat-solver'. But after looking at your code briefly, I couldn't see easily how to add an interface for incremental solving and decided to do another package.
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.)
Thanks for your hint. It would be nice to have the efficiency of your library with the interface of mine. Cheers, Sebastian
participants (2)
-
Denis Bueno -
Sebastian Fischer