Ordered Reduced Binary Decision Diagrams.
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., CUDDHaskell bindings, see this example.