{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T17:15:25Z","timestamp":1777396525213,"version":"3.51.4"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2025,4,11]],"date-time":"2025-04-11T00:00:00Z","timestamp":1744329600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2025,6,30]]},"abstract":"\n Binary Decision Diagrams (BDDs) are widely used for the representation of Boolean functions. Context-Free-Language Ordered Decision Diagrams (CFLOBDDs) are a plug-compatible replacement for BDDs\u2014roughly, they are BDDs augmented with a certain form of procedure call. A natural question to ask is, \u201cFor a given family of Boolean functions\n F<\/jats:italic>\n , what is the relationship between the size of a BDD for\n \n \\(f\\in F\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n and the size of a CFLOBDD for\n f<\/jats:italic>\n ?\u201d Sistla et al. established that there are\n best-case families of functions<\/jats:italic>\n , which demonstrate an inherently exponential separation between CFLOBDDs and BDDs. They showed that there are families of functions\n \n \\(\\{f_{n}\\}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n for which, for all\n \n \\(n=2^{k}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n , the CFLOBDD for\n \n \\(f_{n}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n (using a particular variable order) is exponentially more succinct than\n any<\/jats:italic>\n BDD for\n \n \\(f_{n}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n (i.e., using any variable order). However, they did not give a\n worst-case bound<\/jats:italic>\n \u2014i.e., they left open the question, \u201cIs there a family of functions\n \n \\(\\{g_{i}\\}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n for which the size of a CFLOBDD for\n \n \\(g_{i}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n must be substantially larger than a BDD for\n \n \\(g_{i}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n ?\u201d For instance, it could be that there is a family of functions for which the BDDs are exponentially more succinct than any corresponding CFLOBDDs.\n <\/jats:p>\n \n This article studies such questions, and answers the second question posed above in the negative. In particular, we show that by using the same variable ordering in the CFLOBDD that is used in the BDD, the size of a CFLOBDD for any function\n h<\/jats:italic>\n cannot be far worse than the size of the BDD for\n h<\/jats:italic>\n . The bound that relates their sizes is polynomial:\n <\/jats:p>\n \n The article also shows that the bound is tight: there is a family of functions for which\n \n \\(|C|\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n grows as\n \n \\(\\Omega(|B|^{3})\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n .\n <\/jats:p>","DOI":"10.1145\/3716313","type":"journal-article","created":{"date-parts":[[2025,2,4]],"date-time":"2025-02-04T15:57:20Z","timestamp":1738684640000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Polynomial Bounds of CFLOBDDs against BDDs"],"prefix":"10.1145","volume":"47","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-7257-5124","authenticated-orcid":false,"given":"Xusheng","family":"Zhi","sequence":"first","affiliation":[{"name":"Computer Sciences, University of Wisconsin-Madison, Madison, Wisconsin, USA and Peking University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5676-9949","authenticated-orcid":false,"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"Computer Sciences, University of Wisconsin-Madison, Madison, Wisconsin, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,11]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/1075382.1075387"},{"key":"e_1_3_2_3_2","unstructured":"Henrik Reif Andersen. 1998. An introduction to binary decision diagrams. Unpublished Lecture Notes. Retrieved from https:\/\/www.cs.utexas.edu\/\u223cisil\/cs389L\/bdd.pdf"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.5555\/259794.259826"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/123186.123222"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.5555\/865056"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/157485.164569"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48068-4_8"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/11562436_32"},{"key":"e_1_3_2_11_2","first-page":"709","volume-title":"Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI \u201911)","author":"Darwiche Adnan","year":"2011","unstructured":"Adnan Darwiche. 2011. SDD: A new canonical representation of propositional knowledge bases. In Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI \u201911). International Joint Conferences on Artificial Intelligence Organization, 709\u2013716."},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1613\/JAIR.989"},{"key":"e_1_3_2_13_2","volume-title":"Monocopy and Associative Algorithms in Extended Lisp","author":"Goto Eiichi","year":"1974","unstructured":"Eiichi Goto. 1974. Monocopy and Associative Algorithms in Extended Lisp. Technical Report TR 74-03. University of Tokyo, Tokyo, Japan."},{"key":"e_1_3_2_14_2","unstructured":"Aarti Gupta. 1994. Inductive Boolean Function Manipulation: A Hardware Verification Methodology for Automatic Induction. Ph.D. Dissertation. Technical Report CMU-CS-94-208 Carnegie Mellon University."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1993.580055"},{"key":"e_1_3_2_16_2","unstructured":"N. D. Jones C. K. Gomard and P. Sestoft. 1993. Partial Evaluation and Automatic Program Generation. Prentice-Hall International. Retrieved from https:\/\/www.itu.dk\/sestoft\/pebook\/jonesgomardsestoft-letter.pdf"},{"key":"e_1_3_2_17_2","first-page":"558","volume-title":"Proceedings of the 14th International Conference on the Principles of Knowledge Representation and Reasoning","author":"Kisa Doga","year":"2014","unstructured":"Doga Kisa, Guy Van den Broeck, Arthur Choi, and Adnan Darwiche. 2014. Probabilistic sentential decision diagrams. In Proceedings of the 14th International Conference on the Principles of Knowledge Representation and Reasoning, 558\u2013567. DOI: https:\/\/dl.acm.org\/doi\/10.5555\/3031929.3031996"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISMVL.2006.35"},{"key":"e_1_3_2_19_2","unstructured":"Kengo Nakamura Shuhei Denzumi and Masaaki Nishino. 2020. Variable shift SDD: A more succinct sentential decision diagram. In 18th International Symposium on Experimental Algorithms (SEA 2020). Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik Leibniz International Proceedings in Informatics (LIPIcs) Vol. 160 22:1\u201322:13. DOI: https:\/\/doi.org\/10.4230\/LIPIcs.SEA.2020.22"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2459034"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(98)00093-7"},{"issue":"2","key":"e_1_3_2_22_2","first-page":"7:1","article-title":"CFLOBDDs: Context-free-language ordered binary decision diagrams","volume":"46","author":"Sistla Meghana","year":"2024","unstructured":"Meghana Sistla, Swarat Chaudhuri, and Thomas Reps. 2024. CFLOBDDs: Context-free-language ordered binary decision diagrams. Trans. Prog. Lang. Syst. 46, 2 (2024), 7:1\u20137:82. DOI: https:\/\/dl.acm.org\/doi\/10.1145\/3651157","journal-title":"Trans. Prog. Lang. Syst"},{"key":"e_1_3_2_23_2","unstructured":"Meghana Sistla Swarat Chaudhuri and Thomas Reps. 2024. CFLOBDDs: Context-free-language ordered binary decision diagrams. arXiv:2211.06818v4. Retrieved from https:\/\/arxiv.org\/abs\/2211.06818v4"},{"key":"e_1_3_2_24_2","doi-asserted-by":"crossref","unstructured":"Meghana Sistla Swarat Chaudhuri and Thomas W. Reps. 2023. Weighted context-free-language ordered binary decision diagrams. arXiv:2305.13610. Retrieved from https:\/\/doi.org\/10.48550\/ARXIV.2305.13610","DOI":"10.1145\/3689760"},{"key":"e_1_3_2_25_2","doi-asserted-by":"crossref","unstructured":"Meghana Sistla Swarat Chaudhuri and Thomas W. Reps. 2024. CFLOBDDs: Context-free-language ordered binary decision diagrams (software implementation). Retrieved from https:\/\/github.com\/trishullab\/cflobddComputer.","DOI":"10.1145\/3651157"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_1"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2004.1269084"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.22331\/Q-2023-09-11-1108"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898719789"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/298514.298576"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2834427"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3716313","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3716313","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:42Z","timestamp":1750272222000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3716313"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,11]]},"references-count":30,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6,30]]}},"alternative-id":["10.1145\/3716313"],"URL":"https:\/\/doi.org\/10.1145\/3716313","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,11]]},"assertion":[{"value":"2024-05-29","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-10","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}