The incremental-sat-solver package

[Tags:bsd3, 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.


[Skip to Readme]

Properties

Versions 0.1, 0.1.1, 0.1.2, 0.1.3, 0.1.4, 0.1.5, 0.1.6, 0.1.7
Dependencies base, containers, mtl [details]
License BSD3
Author Sebastian Fischer
Maintainer sebf@informatik.uni-kiel.de
Stability experimental
Category Algorithms
Home page http://github.com/sebfisch/incremental-sat-solver
Bug tracker mailto:sebf@informatik.uni-kiel.de
Source repository head: git clone git://github.com/sebfisch/incremental-sat-solver.git
Uploaded Sat Jan 31 13:15:23 UTC 2009 by SebastianFischer
Distributions NixOS:0.1.7
Downloads 1695 total (21 in the last 30 days)
Votes
0 []
Status Docs uploaded by user
Build status unknown [no reports yet]

Modules

[Index]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees

Readme for incremental-sat-solver

Readme for incremental-sat-solver-0.1.6

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.