Combining ordered best-first search with branch and bound for exact BDD minimization

Reduced ordered Binary Decision Diagrams (BDDs) are frequently used in logic synthesis. In this paper we present a new algorithm to determine an optimal variable ordering of BDDs. In this, we combine ordered best-first search, i.e. the A^*-algorithm, with a classical Branch and Bound (B&B) algorithm. A^* operates on a state space, large parts of which are pruned by a best-first strategy expanding only the most promising states. Combining A^* with B&B allows to avoid unnecessary computations and to save memory. Experimental results demonstrate the efficiency of our new approach.