Construct, combine and query OBDDs;
an efficient representation for formulas in propositional logic.
.
This is mostly educational.
The BDDs do not share nodes (there is no persistent BDD base) and this might introduce inefficiencies.
.
An important (for me, in teaching) feature is
that I can immediately draw the BDD to an X11 window (via graphviz).
For example, to show the effect of different variable orderings,
try this in ghci (type q to close the drawing windows).
.
> import Prelude hiding (not,(&&),(||),and,or,any,all)
> import OBDD
> let f [] = false; f (x:y:zs) = x && y || f zs
> display $ f $ map variable [1,2,3,4,5,6]
> display $ f $ map variable [1,4,2,5,3,6]
.
OBDD implements Ersatz.Boolean which re-defines
Boolean operations from the Prelude. The recommended way of using this
is shown in the previous example.
.
If you want better performance, use a library with a persistent BDD base,
e.g., CUDD
Haskell bindings,
see this example.
