Portability | portable |
---|---|
Stability | experimental |
Maintainer | Sebastian Fischer (sebf@informatik.uni-kiel.de) |
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.
- data Boolean
- data SatSolver
- newSatSolver :: SatSolver
- isSolved :: SatSolver -> Bool
- lookupVar :: Int -> SatSolver -> Maybe Bool
- assertTrue :: MonadPlus m => Boolean -> SatSolver -> m SatSolver
- branchOnVar :: MonadPlus m => Int -> SatSolver -> m SatSolver
- selectBranchVar :: SatSolver -> Int
- solve :: MonadPlus m => SatSolver -> m SatSolver
Documentation
Boolean formulas are represented as values of type Boolean
.
newSatSolver :: SatSolverSource
A new SAT solver without stored constraints.
lookupVar :: Int -> SatSolver -> Maybe BoolSource
We can lookup the binding of a variable according to the currently
stored constraints. If the variable is unbound, the result is
Nothing
.
assertTrue :: MonadPlus m => Boolean -> SatSolver -> m SatSolverSource
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
.
selectBranchVar :: SatSolver -> IntSource
We select a variable from the shortest clause hoping to produce a unit clause.