Hackage :: [Package]

incremental-sat-solver: Simple, Incremental SAT Solving as a Library

[ algorithms, bsd3, library ] [ Propose Tags ] [ Report a vulnerability ]

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]

Modules

[Index]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 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 (<5), containers, mtl [details]
License BSD-3-Clause
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 repo head: git clone git://github.com/sebfisch/incremental-sat-solver.git
Uploaded by SebastianFischer at 2016-08-31T08:21:51Z
Distributions
Reverse Dependencies 3 direct, 0 indirect [details]
Downloads 7326 total (12 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2016-11-20 [all 1 reports]

Readme for incremental-sat-solver-0.1.8

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