Fast exact minimization of BDD's

We present a new exact algorithm for finding the optimal variable ordering for reduced ordered binary decision diagrams (BDD's), The algorithm makes u se of a lower bound technique known from very large scale integration desig n. Up to now this technique has been used only for theoretical consideratio ns and it is adapted here for this purpose. Furthermore, the algorithm supp orts symmetry aspects and uses a hashing based data structure. Experimental results are given to demonstrate the efficiency of our approach. We succee ded in minimizing several functions, including adders with up to 64 variabl es, for which all other previously presented approaches fail.