Data.Boolean

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

data Boolean

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 Literal

Literals are variables that occur either positively or negatively.

Constructors

Pos Int

Neg Int

Instances

Eq Literal

Data Literal

Ord Literal

Show Literal

Negatable Literal

Typeable * Literal

ClauseNormalFormula CNF Literal

literalVar :: Literal -> Int

This function returns the name of the variable in a literal.

invLiteral :: Literal -> Literal

This function negates a literal.

isPositiveLiteral :: Literal -> Bool

This predicate checks whether the given literal is positive.

type CNF = [Clause]

Conjunctive normalforms are lists of lists of literals.

type Clause = [Literal]

booleanToCNF :: Boolean -> CNF

We convert boolean formulas to conjunctive normal form by pushing negations down to variables and repeatedly applying the distributive laws.