Abstract
Reduced Ordered Binary Decision diagrams (ROBDDs) are nowadays one of the most common dynamic data structures for Boolean functions. Among the many areas of application are verification, model checking, and computer aided design. In the last few years, SAT checkers, based on the CNF representation of Boolean functions are getting more and more attention as an alternative to the ROBDD based methods. We show the difference between the CNF representation and the ROBDD representation in one of the most degenerate cases – random monotone 2CNF formulas. We examine this model and give almost matching lower and upper bounds for the ROBDD size in different cases, and show that as soon as the formulas are non-trivial the ROBDD size becomes exponential, thus showing perhaps one of the most fundamental advantages of SAT solvers over ROBDDs.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Berman, C.L.: Ordered binary decision diagrams and circuit structure. In: International Conference on Computer Design 1989 (1989)
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computing (1986)
Biere, A., Cimatti, A., Clarke, E.M., Fujita, M.: Symbolic model checking using SAT procedures instead of BDDs. In: Design Automation Conference DAC 1999 (1999)
Bollig, B., Wegener, I.: Asymptotically optimal bounds for OBDDs and the solution of some basic OBDD problems. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, p. 187. Springer, Heidelberg (2000)
Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge
Gropl, C., Promel, H.J., Srivastav, A.: On the evolution of worst case OBDD size. Information processing letters 77 (2001)
Groote, J.F., Zantema, H.: Resolution and Binary decision diagrams cannot simulate each other polynomially. In: Ershov Memorial Conference 2001 (2001)
Janson, S., Luczak, T., Rucinski, A.: Random graphs. Wiley interscience series in discrete mathematics and optimization
Robertson, N., Seymour, P.D.: Graph minors. 1. excluding a forest. Journal of Combinatorial Theory, Series B, 35 (1983)
Woelfel, P.: New bounds on the OBDD-size of integer multiplication via universal hashing. IEEE Transactions on Computing (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Langberg, M., Pnueli, A., Rodeh, Y. (2003). The ROBDD Size of Simple CNF Formulas. In: Geist, D., Tronci, E. (eds) Correct Hardware Design and Verification Methods. CHARME 2003. Lecture Notes in Computer Science, vol 2860. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39724-3_32
Download citation
DOI: https://doi.org/10.1007/978-3-540-39724-3_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20363-6
Online ISBN: 978-3-540-39724-3
eBook Packages: Springer Book Archive