@hackage / incremental-sat-solver

Simple, Incremental SAT Solving as a Library

Latest0.1.8

About

Metadata

  • Last updated , by SebastianFischer
  • License BSD-3-Clause
  • Categories Algorithms

  • Maintained by: sebf@informatik.uni-kiel.de

  • Lottery factor: 0

Links

Installation

Readme

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.