OBDD (Randal Bryant)

The size of BDD's is sensitive to the ordering of variables.
- With linear arrangment, the size is bounded by 2^(wf * 2^wr).
- where wf is the size (# of wires) of the forward cross section
- and wr = reversed cross section.

At every node of a BDD, there is a boolean function (e.g. P = v*L + !vR).

Prove BDD is cannonical
- prove by induction
- (n + 1) case:

BDD implementation:
-

APPLY is a generalization of operations on two boolean functions:
- f*g = x(fx op

Reordering
- sifting

Possible questions:
- Analyze the BDD size for a given function
- explain the effect of variable ordering on BDD size