Fast exact minimization of BDDs

We present a new exact algorithm for finding the optimal variable ordering for reduced ordered Binary Decision Diagrams (BDDs). The algorithm makes use of a lower bound technique known from VLSI design. Up to now this technique has been used only for theoretical considerations and if is adapted here for our purpose. Furthermore, the algorithm supports symmetry aspects and makes use of a hashing based data structure. Experimental results are given to demonstrate the efficiency of our approach. We succeeded in minimizing adder functions with up to 64 variables, while all other previously presented approaches fail.