This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Improving the Variable Ordering of OBDDs Is NP-Complete
September 1996 (vol. 45 no. 9)
pp. 993-1002

Abstract—Ordered binary decision diagrams are a useful representation of Boolean functions, if a good variable ordering is known. Variable orderings are computed by heuristic algorithms and then improved with local search and simulated annealing algorithms. This approach is based on the conjecture that the following problem is NP-complete. Given an OBDD G representing f and a size bound s, does there exist an OBDD G* (respecting an arbitrary variable ordering) representing f with at most s nodes? This conjecture is proved.

[1] B. Bollig, M. Löbbing, and I. Wegener, "Simulated Annealing to Improve Variable Orderings for OBDDs," Proc. Int'l Workshop Logic Synthesis, pp. 5.1-5.10, 1995.
[2] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C-35, No. 8, Aug. 1986, pp. 667-690.
[3] R.E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams," ACM Computing Surveys, vol., 24 no. 3, pp. 293-318, 1992.
[4] K.M. Butler, D.E. Ross, R. Kapur, and M.R. Mercer, "Heuristics to Compute Variable Orderings for Efficient Manipulation of Ordered Binary Decision Diagrams," Proc. 28th ACM/IEEE Design Automation Conf., pp. 417-420, 1991.
[5] L. Fortune, J. Hopcroft, and E.-M. Schmidt, "The Complexity of Equivalence and Containment for Free Single Variable Program Schemes," Goos, Hartmanis, Ausiello, and Bohm, eds., Lecture Notes in Computer Science 62, pp. 227-240. Springer-Verlag, 1978.
[6] S.J. Friedman and K.J. Supowit, "Finding the Optimal Variable Ordering for Binary Decision Diagrams," IEEE Trans. Computers, vol. 39, no. 5, pp. 710-713, May 1990.
[7] M. Fujita, H. Fujisawa, and N. Kawato, "Evaluation and Improvements of Boolean Comparison Method Based on Binary Decision Diagrams," Proc. ICCAD, IEEE CS Press, 1988, pp. 2-5.
[8] M. Fujita, Y. Matsunaga, and T. Kakuda, "On variable Ordering of Binary Decision Diagrams for the Application of Multi-Level Logic Synthesis," Proc. European Design Automation Conf., pp. 50-54, 1991.
[9] M.R. Garey and D.S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness.New York: W.H. Freeman, 1979.
[10] N. Ishiura, H. Sawada, and S. Yajima, "Minimization of Binary Decision Diagrams Based on Exchanges of Variables," Proc. IEEE Int'l Conf. Computer Aided Design, pp. 472-475, 1991.
[11] S. Malik, A.R. Wang, R.K. Brayton, and A. Sangiovanni-Vincentelli, Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment Proc. IEEE Int'l Conf. Computer-Aided Design (ICCAD-88), pp. 6-9, 1988.
[12] M.R. Mercer, R. Kapur, and D.E. Ross, "Functional Approaches to Generating Orderings for Efficient Symbolic Representation," Proc. 29th ACM/IEEE Design Automation Conf, pp. 614-619, 1992.
[13] S. Minato, N. Ishiura, and S. Yajima, Shared Binary Decision Diagrams with Attributed Edges for Efficient Boolean Function Manipulation Proc. Design Automation Conf., pp. 52-57, 1990.
[14] D.E. Ross, K. M. Butler, R. Kapur, and M.R. Mercer, "Fast Functional Evaluation of Candidate OBDD Variable Ordering," Proc. European Design Automation Conf., pp. 4-10, 1991.
[15] R. Rudell, "Dynamic Variable Ordering for Ordered Binary Decision Diagrams," Proc. ICCAD-93, pp. 42-47, 1993.
[16] D. Sieling and I. Wegener, "Reduction of OBDDs in Linear Time," Information Processing Letters, vol. 48, pp. 139-144, 1993.
[17] D. Sieling and I. Wegener, "NC-Algorithms for Operations on Binary Decision Diagrams," Parallel Processing Letters, vol. 3, no. 1, pp. 3-12, 1993.
[18] S. Tani, K. Hamaguchi, and S. Yajima, "The Complexity of the Optimal Variable Ordering Problems of a Shared Binary Decision Diagram," Proc. 4th Int'l Symp. Algorithms and Computation, Lecture Notes in Computer Science 762, pp. 389-398, 1993.

Index Terms:
Ordered binary decision diagrams, NP-completeness, variable orderings, verification, graph algorithms.
Citation:
Beate Bollig, Ingo Wegener, "Improving the Variable Ordering of OBDDs Is NP-Complete," IEEE Transactions on Computers, vol. 45, no. 9, pp. 993-1002, Sept. 1996, doi:10.1109/12.537122
Usage of this product signifies your acceptance of the Terms of Use.