Copyright | Sebastian Fischer |
---|---|
License | BSD3 |
Maintainer | Sebastian Fischer (sebf@informatik.uni-kiel.de) |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell98 |
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
- data Literal
- literalVar :: Literal -> Int
- invLiteral :: Literal -> Literal
- isPositiveLiteral :: Literal -> Bool
- type CNF = [Clause]
- type Clause = [Literal]
- booleanToCNF :: Boolean -> CNF
- newSatSolver :: SatSolver
- isSolved :: SatSolver -> Bool
- lookupVar :: Int -> SatSolver -> Maybe Bool
- assertTrue :: MonadPlus m => Boolean -> SatSolver -> m SatSolver
- assertTrue' :: MonadPlus m => CNF -> SatSolver -> m SatSolver
- branchOnVar :: MonadPlus m => Int -> SatSolver -> m SatSolver
- selectBranchVar :: SatSolver -> Int
- solve :: MonadPlus m => SatSolver -> m SatSolver
- isSolvable :: SatSolver -> Bool
Documentation
Boolean formulas are represented as values of type Boolean
.
Literals are variables that occur either positively or negatively.
literalVar :: Literal -> Int Source
This function returns the name of the variable in a literal.
invLiteral :: Literal -> Literal Source
This function negates a literal.
isPositiveLiteral :: Literal -> Bool Source
This predicate checks whether the given literal is positive.
booleanToCNF :: Boolean -> CNF Source
We convert boolean formulas to conjunctive normal form by pushing negations down to variables and repeatedly applying the distributive laws.
newSatSolver :: SatSolver Source
A new SAT solver without stored constraints.
lookupVar :: Int -> SatSolver -> Maybe Bool Source
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 SatSolver Source
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 SatSolver Source
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 -> Int Source
We select a variable from the shortest clause hoping to produce a unit clause.
solve :: MonadPlus m => SatSolver -> m SatSolver Source
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
.
isSolvable :: SatSolver -> Bool Source
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.