# Global rebuilding of OBDDs avoiding memory requirement maxima

## Abstract

It is well-known that the size of an ordered binary decision diagram (OBDD) may depend crucially on the order in which the variables occur. In the paper, we describe an implementation of an outputefficient algorithm that transforms an OBDD *P* representing a Boolean function *f* with respect to one variable ordering *π* into an OBDD *Q* that represents *f* with respect to another variable ordering *σ*. The algorithm runs in average time *O(¦P∥Q¦)* and requires *O(¦P¦+n¦Q¦)* space.

The importance of the algorithm is demonstrated by means of experimental results on basically two different applications. In one of them, the algorithm is used merely once. Such transformations are needed to test equivalence or to perform synthesis on OBDDs in which variables appear in different orders. The other application shows a way how to decrease the size of intermediate representations in the course of the construction of OBDDs from a given circuit. Here the algorithm is used dynamically, whenever the size of the manipulated OBDDs becomes too large.

## Keywords

Boolean Function Equivalence Test Binary Decision Diagram Partial Assignment Ordered Binary Decision Diagram## References

- [BCW80]M. Blum, A. K. Chandra, M. N. Wegman: Equivalence of Free Boolean Graphs Can Be Decided Probabilistically in Polynomial Time, Inf. Process. Lett. 10, 2 (Mar.), 80–82, 1980.Google Scholar
- [BMS94]J. Bern, Ch. Meinel, A. Slobodová: Trust — a Programming Environment for the FBDD-package, in print, Univ. Trier, 1994.Google Scholar
- [BRB90]K. S. Brace, R. L. Rudell, R. E. Bryant: Efficient Implementation of a BDD Package, Proc. of 27th ACM/IEEE Design Automation Conference (Orlando, June), 40–45, 1990.Google Scholar
- [BRKM91]K. M. Butler, D. E. ross, R. Kapur, M. R. Mercer: Heuristics to Compute Variable Orderings for Efficient Manipulation of Ordered Binary Decision Diagrams. Proc. 28th ACM/IEEE DAC, 417–420, 1991.Google Scholar
- [Bry86]R. E. Bryant: Graph-Based Algorithms for Boolean Function Manipulation, IEEE Trans. Comput. C-35, 6 (Aug.), 677–691, 1986.Google Scholar
- [BW94]B. Bollig, I. Wegener: Improving the Variable Ordering of OBDDs is NP-Complete, Forschungsbericht Nr. 542, 1994.Google Scholar
- [FFK88]M. Fujita, H. Fujisawa, N. Kawato: Evaluation and Improvements of Boolean Comparison Method Based on Binary Decision Diagrams. Proc. of IEEE ICCAD, 2–5, 1988.Google Scholar
- [FMK91]M. Fujita, Y. Matsunaga, T. Kakuda: On Variable Ordering of Binary Decision Diagrams for the Application of Multi-Valued Logic Synthesis. Proc. of EDAC, 502–53, 1991.Google Scholar
- [FS90]S. J. Friedman, K. J. Supowit: Finding the Optimal Variable Ordering for binary Decision Diagrams. IEEE Trans. on Computers 39, 710–713, 1990.Google Scholar
- [MIY90]S. Minato, N. Ishiura, S. Yajima: Shared Binary Decision Diagrams with Attributed edges for Efficient Boolean Function Manipulation. Proc. of the 27th ACM/IEEE Design Automation Conference, 52–57, 1990.Google Scholar
- [MKR92]M. R. Mercer, R. Kapur, D. E. Ross: Functional Approaches to Generating Orderings for Efficient Symbolic Representation. Proc. of 29th ACM/IEEE DAC, 614–619, 1992.Google Scholar
- [MWBS88]S. Malik, A. Wang, R. K. Brayton, A. Sangiovanni-Vincentelli: Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment, Proc. of the IEEE International Conference on Computer-Aided Design (Santa Clara, Calif., Nov.), 6–9, 1988.Google Scholar
- [MS94]Ch. Meinel, A. Slobodová: On the Complexity of Constructing optimal Ordered Binary Decision Diagrams, Proc. of MFCS'94, LNCS 841, 515–524, 1994.Google Scholar
- [Rud93]R. Rudell: Dynamic Variable Ordering for Ordered Binary Decision Diagrams. Proc. of IEEE ICCAD, 42–47, 1993.Google Scholar
- [SW94]P. Savický, I. Wegener: Efficient Algorithms for the Transformation Between Different Types of Binary Decision Diagrams. Proc. FST&TCS, 1994.Google Scholar
- [THY93]S. Tani, K. Hamaguchi, S. Yajima: The Complexity of the Optimal Variable Ordering of a Shared Binary Decision Diagram. Proc. 4th ISAAC, LNCS 762, 389–398, 1993.Google Scholar
- [TI94]S. Tani, H. Imai: A Reordering for an Ordered Binary Decision Diagram and an Extended Framework for Combinatorics of Graphs. Proc. of 5th ISAAC, LNCS, 1994.Google Scholar