Combination of Lower Bounds in Exact BDD Minimization
Rüdiger Ebendt, Wolfgang H. H. Gunther, Rolf Drechsler · 2003
Ordered Binary Decision Diagrams (BDDs) are a data structure for efficient representation and manipulation of Boolean functions. They are frequently used in logic synthesis and formal verification. 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