Quasi-exact BDD minimization using relaxed best-first search

In this paper, we present a new method for quasi-exact optimization of BDDs using relaxed ordered best-first search. This general method is applied to BDD minimization. In contrast to a known relaxation of A*, the new method guarantees to expand every state exactly once if guided by a monotone heuristic function. By that, it effectively accounts for aspects of run time while still guaranteeing that the cost of the solution does not exceed the optimal cost by a factor greater than (1 + ε)^└<span>n/2┘/ where n is the maximal length of a solution path. E.g., for 25 BDD variables and using a degree of relaxation of 5%, the BDD size is guaranteed to be not greater than 1.8 times the optimal size. Within a range of reasonable choices for ε, the method allows the user to trade off run time for solution quality. Experimental results demonstrate large reductions in run time when compared to the best known exact approach. Moreover, the quality of the obtained solutions is much better than the quality guaranteed by the theory.