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

Reduced-ordered binary decision diagrams (BDDs) are a data structure for efficient representation and manipulation of Boolean functions. They are frequently used in logic synthesis. The size of BDDs depends on a chosen variable ordering, i.e., the size may vary from linear to exponential, and the problem of improving the variable ordering is known to be NP-complete. In this paper, a new exact BDD minimization algorithm called A^stute is presented. Here, ordered best-first search, i.e., the A^* algorithm, is combined 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 approach.