On Wed, Jan 28, 2009 at 13:32, Sebastian Fischer <[email protected]> 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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
