Global rebuilding of OBDDs avoiding memory requirement maxima

  • Jochen Bern
  • Christoph Meinel
  • Anna Slobodová
Session 2: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)


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.


Boolean Function Equivalence Test Binary Decision Diagram Partial Assignment Ordered Binary Decision Diagram 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [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
  2. [BMS94]
    J. Bern, Ch. Meinel, A. Slobodová: Trust — a Programming Environment for the FBDD-package, in print, Univ. Trier, 1994.Google Scholar
  3. [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
  4. [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
  5. [Bry86]
    R. E. Bryant: Graph-Based Algorithms for Boolean Function Manipulation, IEEE Trans. Comput. C-35, 6 (Aug.), 677–691, 1986.Google Scholar
  6. [BW94]
    B. Bollig, I. Wegener: Improving the Variable Ordering of OBDDs is NP-Complete, Forschungsbericht Nr. 542, 1994.Google Scholar
  7. [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
  8. [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
  9. [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
  10. [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
  11. [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
  12. [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
  13. [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
  14. [Rud93]
    R. Rudell: Dynamic Variable Ordering for Ordered Binary Decision Diagrams. Proc. of IEEE ICCAD, 42–47, 1993.Google Scholar
  15. [SW94]
    P. Savický, I. Wegener: Efficient Algorithms for the Transformation Between Different Types of Binary Decision Diagrams. Proc. FST&TCS, 1994.Google Scholar
  16. [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
  17. [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

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Jochen Bern
    • 1
  • Christoph Meinel
    • 1
  • Anna Slobodová
    • 1
  1. 1.University of TrierTrierGermany

Personalised recommendations