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

Portability portable experimental Sebastian Fischer (sebf@informatik.uni-kiel.de)

Data.Boolean.SatSolver

Description

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.

Synopsis

# Documentation

data Boolean Source

Boolean formulas are represented as values of type `Boolean`.

Constructors

 Var Int Variables are labeled with an `Int`, Yes `Yes` represents true, No `No` represents false, Not Boolean `Not` constructs negated formulas, Boolean :&&: Boolean and finally we provide conjunction Boolean :||: Boolean and disjunction of boolean formulas.

Instances

 Show Boolean

data SatSolver Source

A `SatSolver` can be used to solve boolean formulas.

Instances

 Show SatSolver

A new SAT solver without stored constraints.

This predicate tells whether all constraints are solved.

We can lookup the binding of a variable according to the currently stored constraints. If the variable is unbound, the result is `Nothing`.

We can assert boolean formulas to update a `SatSolver`. The assertion may fail if the resulting constraints are unsatisfiable.

branchOnVar :: MonadPlus m => Int -> SatSolver -> m SatSolverSource

This function guesses a value for the given variable, if it is currently unbound. As this is a non-deterministic operation, the resulting solvers are returned in an instance of `MonadPlus`.

We select a variable from the shortest clause hoping to produce a unit clause.

solve :: MonadPlus m => SatSolver -> m SatSolverSource

This function guesses values for variables such that the stored constraints are satisfied. The result may be non-deterministic and is, hence, returned in an instance of `MonadPlus`.

This predicate tells whether the stored constraints are solvable. Use with care! This might be an inefficient operation. It tries to find a solution using backtracking and returns `True` if and only if that fails.