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.