{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T00:18:13Z","timestamp":1771978693226,"version":"3.50.1"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2019,1,18]],"date-time":"2019-01-18T00:00:00Z","timestamp":1547769600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2019,1,31]]},"abstract":"<jats:p>Binary Decision Diagrams (BDDs) and in particular ROBDDs (Reduced Ordered BDDs) are a common data structure for manipulating Boolean expressions, integrated circuit design, type inferencers, model checkers, and many other applications. Although the ROBDD is a lightweight data structure to implement, the behavior, in terms of memory allocation, may not be obvious to the program architect. We explore experimentally, numerically, and theoretically the typical and worst-case ROBDD sizes in terms of number of nodes and residual compression ratios, as compared to unreduced BDDs. While our theoretical results are not surprising, as they are in keeping with previously known results, we believe our method contributes to the current body of research by our experimental and statistical treatment of ROBDD sizes. In addition, we provide an algorithm to calculate the worst-case size. Finally, we present an algorithm for constructing a worst-case ROBDD of a given number of variables. Our approach may be useful to projects deciding whether the ROBDD is the appropriate data structure to use, and in building worst-case examples to test their code.<\/jats:p>","DOI":"10.1145\/3274279","type":"journal-article","created":{"date-parts":[[2019,1,18]],"date-time":"2019-01-18T21:39:00Z","timestamp":1547847540000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["A Theoretical and Numerical Analysis of the Worst-Case Size of Reduced Ordered Binary Decision Diagrams"],"prefix":"10.1145","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1595-8655","authenticated-orcid":false,"given":"Jim","family":"Newton","sequence":"first","affiliation":[{"name":"EPITA, Le Kremlin-Bic\u00eatre, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6315-052X","authenticated-orcid":false,"given":"Didier","family":"Verna","sequence":"additional","affiliation":[{"name":"EPITA, Le Kremlin-Bic\u00eatre, France"}]}],"member":"320","published-online":{"date-parts":[[2019,1,18]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2444851.2444862"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1978.1675141"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Gerold Alsmeyer. 2011. Chebyshev\u2019s Inequality. Springer Berlin 239--240.  Gerold Alsmeyer. 2011. Chebyshev\u2019s Inequality. Springer Berlin 239--240.","DOI":"10.1007\/978-3-642-04898-2_167"},{"key":"e_1_2_1_5_1","unstructured":"Ansi. 1994. American National Standard: Programming Language\u2014Common Lisp. ANSI X3.226:1994 (R1999).  Ansi. 1994. American National Standard: Programming Language\u2014Common Lisp. ANSI X3.226:1994 (R1999)."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-016-9239-9"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/123186.123222"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"e_1_2_1_10_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Bryant Randal E.","unstructured":"Randal E. Bryant . 2018. Chain reduction for binary and zero-suppressed decision diagrams . In Tools and Algorithms for the Construction and Analysis of Systems , Dirk Beyer and Marieke Huisman (Eds.). Springer International Publishing , Cham , 81--98. Randal E. Bryant. 2018. Chain reduction for binary and zero-suppressed decision diagrams. In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer and Marieke Huisman (Eds.). Springer International Publishing, Cham, 81--98."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110285"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008695706493"},{"key":"e_1_2_1_14_1","unstructured":"Maximilien Colange. 2013. Symmetry Reduction and Symbolic Data Structures for Model Checking of Distributed Systems. Th\u00e8se de doctorat. Laboratoire de l\u2019Informatique de Paris VI Universit\u00e9 Pierre-et-Marie-Curie France.  Maximilien Colange. 2013. Symmetry Reduction and Symbolic Data Structures for Model Checking of Distributed Systems. Th\u00e8se de doctorat. Laboratoire de l\u2019Informatique de Paris VI Universit\u00e9 Pierre-et-Marie-Curie France."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 28th International Conference Computer Aided Verification (CAV\u201916)","author":"Fried Dror","unstructured":"Dror Fried , Lucas M. Tabajara , and Moshe Y. Vardi . 2016. BDD-based boolean functional synthesis . In Proceedings of the 28th International Conference Computer Aided Verification (CAV\u201916) . 402--421. Dror Fried, Lucas M. Tabajara, and Moshe Y. Vardi. 2016. BDD-based boolean functional synthesis. In Proceedings of the 28th International Conference Computer Aided Verification (CAV\u201916). 402--421."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/646513.695507"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00148-4"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.286311"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1053468.1053470"},{"key":"e_1_2_1_20_1","volume-title":"The Art of Computer Programming","author":"Knuth Donald E.","unstructured":"Donald E. Knuth . 2009. The Art of Computer Programming , Volume 4 , Fascicle 1: Bitwise Tricks 8 Techniques; Binary Decision Diagrams (12th ed.). Addison-Wesley Professional . Donald E. Knuth. 2009. The Art of Computer Programming, Volume 4, Fascicle 1: Bitwise Tricks 8 Techniques; Binary Decision Diagrams (12th ed.). Addison-Wesley Professional."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218127404010709"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 29th ACM\/IEEE Design Automation Conference (DAC\u201992)","author":"Lai Y.-T.","unstructured":"Y.-T. Lai and S. Sastry . 1992. Edge-valued binary decision diagrams for multi-level hierarchical verification . In Proceedings of the 29th ACM\/IEEE Design Automation Conference (DAC\u201992) . IEEE Computer Society Press, Los Alamitos, CA, 608--613. http:\/\/dl.acm.org\/citation.cfm?id=113938.149642. Y.-T. Lai and S. Sastry. 1992. Edge-valued binary decision diagrams for multi-level hierarchical verification. In Proceedings of the 29th ACM\/IEEE Design Automation Conference (DAC\u201992). IEEE Computer Society Press, Los Alamitos, CA, 608--613. http:\/\/dl.acm.org\/citation.cfm?id=113938.149642."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39724-3_32"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1923102.1923108"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/272991.272995"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/850983.855325"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/157485.164890"},{"key":"e_1_2_1_28_1","unstructured":"William H. Newman. 2015. Steel Bank Common Lisp User Manual. Retrieved from http:\/\/www.sbcl.org.  William H. Newman. 2015. Steel Bank Common Lisp User Manual. Retrieved from http:\/\/www.sbcl.org."},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the European Lisp Symposium.","author":"Newton Jim","year":"2018","unstructured":"Jim Newton and Didier Verna . 2018 . Strategies for typecase optimization . In Proceedings of the European Lisp Symposium. Jim Newton and Didier Verna. 2018. Strategies for typecase optimization. In Proceedings of the European Lisp Symposium."},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the European Lisp Symposium.","author":"Newton Jim","year":"2017","unstructured":"Jim Newton , Didier Verna , and Maximilien Colange . 2017 . Programmatic manipulation of common lisp type specifiers . In Proceedings of the European Lisp Symposium. Jim Newton, Didier Verna, and Maximilien Colange. 2017. Programmatic manipulation of common lisp type specifiers. In Proceedings of the European Lisp Symposium."},{"key":"e_1_2_1_31_1","volume-title":"Purely Functional Data Structures","author":"Okasaki Chris","unstructured":"Chris Okasaki . 1998. Purely Functional Data Structures . Cambridge University Press, New York , NY. Chris Okasaki. 1998. Purely Functional Data Structures. Cambridge University Press, New York, NY."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.588065"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1949.tb03624.x"},{"key":"e_1_2_1_34_1","volume-title":"Object-oriented Common LISP","author":"Slade S.","unstructured":"S. Slade . 1998. Object-oriented Common LISP . Prentice Hall PTR. S. Slade. 1998. Object-oriented Common LISP. Prentice Hall PTR."},{"key":"e_1_2_1_35_1","volume-title":"CUDD: BDD package","author":"Somenzi Fabio","unstructured":"Fabio Somenzi . {n.d.}. CUDD: BDD package , University of Colorado , Boulder. Fabio Somenzi. {n.d.}. CUDD: BDD package, University of Colorado, Boulder."},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD\u201990)","author":"Srinivasan A.","year":"2002","unstructured":"A. Srinivasan . 2002 . Algorithms for discrete function manipulation . In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD\u201990) . A. Srinivasan. 2002. Algorithms for discrete function manipulation. In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD\u201990)."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/288548.289117"},{"key":"e_1_2_1_38_1","volume-title":"The Complexity of Boolean Functions","author":"Wegener Ingo","unstructured":"Ingo Wegener . 1987. The Complexity of Boolean Functions . John Wiley 8 Sons, Inc., New York, NY. Ingo Wegener. 1987. The Complexity of Boolean Functions. John Wiley 8 Sons, Inc., New York, NY."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3274279","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3274279","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:44:06Z","timestamp":1750207446000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3274279"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,18]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,1,31]]}},"alternative-id":["10.1145\/3274279"],"URL":"https:\/\/doi.org\/10.1145\/3274279","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,18]]},"assertion":[{"value":"2018-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-01-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}