This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Streaming BDD Manipulation
May 2002 (vol. 51 no. 5)
pp. 474-485

Binary Decision Diagrams (BDDs) are now commonly used for handling Boolean functions because of their excellent efficiency in terms of time and space. However, the conventional BDD manipulation algorithm is strongly based on the hash table technique, so it always encounters the memory overflow problem when handling large-scale BDD data. This paper proposes a new streaming BDD manipulation method that never causes memory overflow or swap out. This method allows us to handle very large-scale BDD stream data beyond the memory limitation. Our method can be characterized as follows: 1) it gives a continuous tradeoff curve between memory usage and stream data length, 2) valid solutions for a partial Boolean space can be obtained if we break the process before finishing, and 3) easily accelerated by pipelined multiprocessing. An experimental result demonstrates that we can succeed in finding a number of solutions to a SAT problem using commodity PC with a 64 MB memory, where as the conventional BDD manipulator would have required a 100GB memory. BDD manipulation has been considered as an intensively memory-consuming procedure, but now we can also utilize the hard disk and network resources as well. The method leads to a new approach to BDD manipulation.

[1] T. Bell, I.H. Witten, and J.G. Cleary, “Modeling for Text Compression,” ACM Computing Surveys, vol. 21, no. 4, pp. 557-591, Dec. 1989.
[2] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, Symbolic Model Checking without BDDs Proc. Tools and Algorithms for the Construction and Analysis of Systems, 1999.
[3] K.S. Brace, R.L. Rudell, and R.E. Bryant, Efficient Implementation of a BDD Package Proc. Design Automation Conf., pp. 40-45, 1990.
[4] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C-35, No. 8, Aug. 1986, pp. 667-690.
[5] J. Burch, E. Clarke, K. McMillan, and D. Dill, "Sequential Circuit Verification Using Symbolic Model Checking," Proc. 27th Design Automation Conf., pp. 46-51, 1990.
[6] E.M. Clarke, K.L. McMillan, X. Zhao, M. Fujita, and J. Yang, "Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping," Proc. 30th Design Automation Conf., pp. 54-60, 1993.
[7] G. Janssen, “Design of a Pointerless BDD Package,” Note of Int'l Workshop Logic and Synthesis (IWLS-2001), May 2001.
[8] S. Kimura and E.M. Clarke, “A Parallel Algorithm for Constructing Binary Decision Diagrams,” Proc. IEEE/ACM Int'l Conf. Computer Design (ICCD-90), pp. 220-223, Sept. 1990.
[9] Y-T. Lai, M. Pedram, and S. Sastry (S.B.K. Vrudhula), "FGILP: An integer linear program solver based on function graphs," Proc. Int'l Conf. Computer Aided Design, 1993.
[10] M. Löbbing, and I. Wegener, “The Number of Knight's Tour Equals$33,439,123,484,294$—Counting with Binary Decision Diagrams,” The Electric J. Combinatorics, vol. 3, no. R5, 1996.
[11] D.E. Long, “The Design of a Cache-Friendly BDD Library,” Proc. IEEE/ACM Int'l Conf. Computer-Aided Design (ICCAD-98), pp. 639-645, Nov. 1998.
[12] J.C. Madre and O. Coudert, “A Logically Complete Reasoning Maintenance System Based on a Logical Constraint Solver,” Proc. Int'l Joint Conf. Artificial Intelligence (IJCAI), pp. 294-299, 1991.
[13] K. Milvang-Jensen and A.J. Hu, “BDDNOW: A Parallel BDD Package,” Formal Method in Computer-Aided Design (Proc. FMCAD-98), pp. 501-507, June 1998.
[14] S. Minato, “BEM-II: An Arithmetic Boolean Expression Manipulator Using BDDs,” IEICE Trans. Fundamentals, vol. E76-A, no. 10, pp. 1721-1729, Oct. 1993.
[15] 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.
[16] M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and A. Malik, “Chaff: Engineering an Efficient SAT Solver,” Proc. 38th ACM/IEEE Design Automation Conf. (DAC-2001), pp. 530-535, June 2001.
[17] H. Ochi, Y. Kouichi, and S. Yajima, “Breadth-First Manipulation of Very Large Binary-Decision Diagrams,” Proc. IEEE/ACM Int'l Conf. Computer-Aided Design (ICCAD-93), pp. 48-55, Nov. 1993.
[18] H.G. Okuno, “Reducing Combinatorial Explosions in Solving Search-Type Combinatorial Problems with Binary Decision Diagram,” Trans. of Information Processing Soc. Japan (IPSJ), (in Japanese), vol. 35, no. 5, pp. 739-753, May 1994.
[19] R.K. Ranjan, J.V. Sanghavi, R.K. Brayton, and A. Sangiovanni-Vincentelli, “Binary Decision Diagrams on Network of Workstations,” Proc. IEEE/ACM Int'l Conf. Computer Design (ICCD-96), Oct. 1996.
[20] B. Selman, H. Levesque, and D. Mitchell, “A New Method for Solving Hard Satisfiability Problems,” Proc. Am. Assoc. Artificial Intelligence, (AAAI '92), pp. 440-446, July 1992.
[21] J.P. Marques-Silva and K.A. Sakallah, "Grasp: A New Search Algorithm for Satisfiability," Proc. Int'l Conf. Computer-Aided Design (ICCAD 96), IEEE CS Press, 1996, pp. 220-227.
[22] F. Somenzi, “Efficient Manipulation of Decision Diagrams,” Int'l J. Software Tools for Technology Transfer (STTT), vol. 3, no.2, pp. 171-181, May 2001.
[23] F. Somenzi et al. “CUDD: CU Decision Diagram Package,” Public Software,http://vlsi.colorad.edu/fabioCUDD,YEAR???
[24] T. Stornetta and F. Brewer, “Implementation of an Efficient Paralell BDD Package,” Proc. 33th ACM/IEEE Design Automation Conf. (DAC '96), June 1996.
[25] M.N. Velev and R.E. Bryant, “Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessor,” Proc. 38th ACM/IEEE Design Automation Conf. (DAC-2001), pp. 226-231, June 2001.
[26] B. Yang, Y.-A. Chen, R.E. Bryant, and D.R. O'Hallaron, “Space- and Time-efficient BDD Construction via Working Set Control,” Proc. Asia and South Pacific Design Autonation Conf. (ASPDAC-98), pp. 423-432, Feb. 1998.
[27] J. Ziv and A. Lempel, "A Universal Algorithm for Sequential Data Compression," IEEE Trans. Information Theory, vol. 23, no. 3, pp. 337-343, 1977.

Index Terms:
BDD, binary decision diagram, VLSI CAD, logic design, verification, testing, data structure, algorithm, combinatorial problem
Citation:
S.-i. Minato, "Streaming BDD Manipulation," IEEE Transactions on Computers, vol. 51, no. 5, pp. 474-485, May 2002, doi:10.1109/TC.2002.1004587
Usage of this product signifies your acceptance of the Terms of Use.