Portability | portable |
---|---|
Stability | experimental |
Maintainer | Sebastian Fischer (sebf@informatik.uni-kiel.de) |
Safe Haskell | Safe-Inferred |
This library provides a representation of boolean formulas that is used by the solver in Data.Boolean.SatSolver.
We also define a function to simplify formulas, a type for conjunctive normalforms, and a function that creates them from boolean formulas.
Documentation
Boolean formulas are represented as values of type Boolean
.
Literals are variables that occur either positively or negatively.
literalVar :: Literal -> IntSource
This function returns the name of the variable in a literal.
invLiteral :: Literal -> LiteralSource
This function negates a literal.
isPositiveLiteral :: Literal -> BoolSource
This predicate checks whether the given literal is positive.
booleanToCNF :: Boolean -> CNFSource
We convert boolean formulas to conjunctive normal form by pushing negations down to variables and repeatedly applying the distributive laws.