The incremental-sat-solver package

[ Tags: algorithms, bsd3, library ] [ Propose Tags ]

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, 0.1.8
Dependencies base, containers, mtl [details]
License BSD3
Author Sebastian Fischer
Maintainer sebf@informatik.uni-kiel.de
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 Fri Jan 30 17:38:33 UTC 2009 by SebastianFischer
Distributions NixOS:0.1.8
Downloads 2043 total (12 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]
Hackage Matrix CI

Modules

[Index]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for incremental-sat-solver-0.1.5

[back to package description]
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.