Ordered binary decision diagrams (BDDs) are a data structure for the repres
entation and manipulation of Boolean functions, which is often applied in v
ery large scale integration (VLSI) computer-aided design (CAD). The choice
of variable ordering largely influences the size of the BDD; its size may v
ary from linear to exponential. The most successful methods to find good or
derings are based on dynamic variable reordering, i.e., exchanging neighbor
ing variables. This basic operation has been used in various variants, like
sifting and window permutation.
In this paper, we show that lower bounds computed during the minimization p
rocess can speed up the computation significantly, First, lower hounds are
studied from a theoretical point of view. Then these techniques are incorpo
rated in dynamic minimization algorithms. By the computation of good lower
bounds, large parts of the search space ran he pruned, resulting in very fa
st computations. Experimental results are given to demonstrate the efficien
cy of our approach.