Effect of improved lower bounds in dynamic BDD reordering

In this paper, we present new lower bounds on binary decision diagram (BDD) size. These lower bounds are derived from more general lower bounds that recently were given in the context of exact BDD minimization. The results presented in this paper are twofold. First, we gain deeper insight by looking at the theory behind the new lower bounds. Examples lead to a better understanding, showing that the new lower bounds are effective in situations where this is not the case for previous lower bounds and vice versa. Following the constraints in practice, we then compromise between run time and quality of the lower bounds. Finally, a clever combination of old and new lower bounds results in a final tight lower bound, yielding a significant improvement. Experimental results show the efficiency of our approach.