Binary Decision Diagrams and the Multiple Variable Order Problem

Ordered Binary Decision Diagrams (OBDDs) are the first choice in manipulating and representing Boolean functions in CAD. Since the size of an OBDD heavily depends on the chosen variable order, much effort is spent in finding good and improving existing variable orders. If these optimizing techniques are used in OBDD applications, one has to cope with OBDDs of different variable orders very often (e.g., representing the transition relation and the reachable state set in sequential verification). For an efficient manipulation and represention of OBDDs as a multi rooted OBDD, a common variable order is desired. In this paper we present approaches for the solution of the multiple variable order problem, i.e., we present heuristics that compute a well suited intermediate variable order based on the original variable orders of the involved OBDD