{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,17]],"date-time":"2026-02-17T11:48:14Z","timestamp":1771328894425,"version":"3.50.1"},"reference-count":72,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,5,2]],"date-time":"2024-05-02T00:00:00Z","timestamp":1714608000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"crossref","award":["N00014-00-1-0607, and N00014-19-1-2318"],"award-info":[{"award-number":["N00014-00-1-0607, and N00014-19-1-2318"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"crossref"}]},{"name":"National Science Foundation","award":["CCR-9986308, and CCF-2212559"],"award-info":[{"award-number":["CCR-9986308, and CCF-2212559"]}]},{"DOI":"10.13039\/100005712","name":"Missile Defense Agency","doi-asserted-by":"crossref","award":["DASG60-01-P-0048"],"award-info":[{"award-number":["DASG60-01-P-0048"]}],"id":[{"id":"10.13039\/100005712","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Facebook"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2024,6,30]]},"abstract":"<jats:p>\n            This article presents a new compressed representation of Boolean functions, called\n            <jats:italic>CFLOBDDs<\/jats:italic>\n            (for Context-Free-Language Ordered Binary Decision Diagrams). They are essentially a plug-compatible alternative to BDDs (Binary Decision Diagrams), and hence are useful for representing certain classes of functions, matrices, graphs, relations, and so forth in a highly compressed fashion. CFLOBDDs share many of the good properties of BDDs, but\u2014in the best case\u2014the CFLOBDD for a Boolean function can be\n            <jats:italic>exponentially smaller than any BDD for that function<\/jats:italic>\n            . Compared with the size of the decision tree for a function, a CFLOBDD\u2014again, in the best case\u2014can give a\n            <jats:italic>double-exponential reduction in size<\/jats:italic>\n            . They have the potential to permit applications to (i) execute much faster and (ii) handle much larger problem instances than has been possible heretofore.\n          <\/jats:p>\n          <jats:p>We applied CFLOBDDs in quantum-circuit simulation and found that for several standard problems, the improvement in scalability, compared to BDDs, is quite dramatic. With a 15-minute timeout, the number of qubits that CFLOBDDs can handle are 65,536 for Greenberger-Horne-Zellinger, 524,288 for Bernstein-Vazirani, 4,194,304 for Deutsch-Jozsa, and 4,096 for Grover\u2019s algorithm, besting BDDs by factors of 128\u00d7, 1,024\u00d7, 8,192\u00d7, and 128\u00d7, respectively.<\/jats:p>","DOI":"10.1145\/3651157","type":"journal-article","created":{"date-parts":[[2024,3,4]],"date-time":"2024-03-04T12:25:55Z","timestamp":1709555155000},"page":"1-82","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["CFLOBDDs: Context-Free-Language Ordered Binary Decision Diagrams"],"prefix":"10.1145","volume":"46","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4215-0651","authenticated-orcid":false,"given":"Meghana Aparna","family":"Sistla","sequence":"first","affiliation":[{"name":"The University of Texas at Austin, Austin, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6859-1391","authenticated-orcid":false,"given":"Swarat","family":"Chaudhuri","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin, Austin, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5676-9949","authenticated-orcid":false,"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,5,2]]},"reference":[{"key":"e_1_3_4_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/1075382.1075387"},{"key":"e_1_3_4_3_2","doi-asserted-by":"crossref","unstructured":"Anuchit Anuchitanukul Zohar Manna and Tom\u00e1s E. Uribe. 1995. Differential BDDs. In Computer Science Today: Recent Trends and Developments. Lecture Notes in Computer Science Vol. 1000. Springer 218\u2013233.","DOI":"10.1007\/BFb0015246"},{"key":"e_1_3_4_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"e_1_3_4_5_2","doi-asserted-by":"publisher","DOI":"10.5555\/243846.243857"},{"key":"e_1_3_4_6_2","doi-asserted-by":"publisher","unstructured":"Thomas Ball and Sriram K. Rajamani. 2001. Automatically validating temporal safety properties of interfaces. In Model Checking Software. Lecture Notes in Computer Science Vol. 2057. Springer 103\u2013122. DOI:10.1007\/3-540-45139-0_7","DOI":"10.1007\/3-540-45139-0_7"},{"key":"e_1_3_4_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/379605.379690"},{"key":"e_1_3_4_8_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.102.240603"},{"key":"e_1_3_4_9_2","article-title":"Circuit for Shor\u2019s algorithm using 2n+3 Qubits","author":"Beauregard Stephane","year":"2002","unstructured":"Stephane Beauregard. 2002. Circuit for Shor\u2019s algorithm using 2n+3 Qubits. arXiv preprint quant-ph\/0205095 (2002).","journal-title":"arXiv preprint quant-ph\/0205095"},{"key":"e_1_3_4_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48224-5_54"},{"key":"e_1_3_4_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/123186.123222"},{"key":"e_1_3_4_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_4_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/217474.217583"},{"key":"e_1_3_4_14_2","doi-asserted-by":"publisher","DOI":"10.21236\/ADA296684"},{"key":"e_1_3_4_15_2","doi-asserted-by":"publisher","DOI":"10.5555\/865056"},{"key":"e_1_3_4_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/157485.164569"},{"key":"e_1_3_4_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-1385-4_4"},{"key":"e_1_3_4_18_2","doi-asserted-by":"publisher","DOI":"10.1137\/0201006"},{"key":"e_1_3_4_19_2","volume-title":"Proceedings of the 22nd International Joint Conference on Artificial Intelligence","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."},{"key":"e_1_3_4_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/1159876.1159880"},{"key":"e_1_3_4_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/1236463.1236468"},{"key":"e_1_3_4_22_2","article-title":"Implementation of Shor\u2019s algorithm on a linear nearest neighbour qubit array","author":"Fowler Austin G.","year":"2004","unstructured":"Austin G. Fowler, Simon J. Devitt, and Lloyd C. L. Hollenberg. 2004. Implementation of Shor\u2019s algorithm on a linear nearest neighbour qubit array. arXiv preprint quant-ph\/0402196 (2004).","journal-title":"arXiv preprint quant-ph\/0402196"},{"key":"e_1_3_4_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(73)80040-6"},{"key":"e_1_3_4_24_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_4_25_2","doi-asserted-by":"publisher","DOI":"10.21105\/joss.00819"},{"key":"e_1_3_4_26_2","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_3_4_27_2","volume-title":"Inductive Boolean Function Manipulation: A Hardware Verification Methodology for Automatic Induction","author":"Gupta Aarti","year":"1994","unstructured":"Aarti Gupta. 1994. Inductive Boolean Function Manipulation: A Hardware Verification Methodology for Automatic Induction. Ph.D. Dissertation. Carnegie Mellon University."},{"key":"e_1_3_4_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1993.580055"},{"key":"e_1_3_4_29_2","volume-title":"Digital Design and Computer Architecture","author":"Harris David","year":"2010","unstructured":"David Harris and Sarah Harris. 2010. Digital Design and Computer Architecture. Morgan Kaufmann."},{"key":"e_1_3_4_30_2","unstructured":"Xin Hong Xiangzhen Zhou Sanjiang Li Yuan Feng and Mingsheng Ying. 2020. A tensor network based decision diagram for representation of quantum circuits. arXiv:2009.02618 (2020)."},{"key":"e_1_3_4_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/77606.77608"},{"key":"e_1_3_4_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446750"},{"key":"e_1_3_4_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/577200"},{"key":"e_1_3_4_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/12.644298"},{"key":"e_1_3_4_35_2","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."},{"key":"e_1_3_4_36_2","article-title":"Version space algebras are acyclic tree automata","volume":"2107","author":"Koppel James","year":"2021","unstructured":"James Koppel. 2021. Version space algebras are acyclic tree automata. CoRR abs\/2107.12568 (2021). https:\/\/arxiv.org\/abs\/2107.12568","journal-title":"CoRR"},{"key":"e_1_3_4_37_2","doi-asserted-by":"publisher","DOI":"10.5555\/113938.149642"},{"key":"e_1_3_4_38_2","doi-asserted-by":"publisher","DOI":"10.5555\/1293203"},{"key":"e_1_3_4_39_2","unstructured":"Richard J. Lipton. 2009. G\u00f6del\u2019s Lost Letter and P=NP: BDD\u2019s and Factoring. Retrieved March 12 2024 from https:\/\/rjlipton.wpcomstaging.com\/2009\/06\/16\/bdds-and-factoring"},{"key":"e_1_3_4_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01776573"},{"key":"e_1_3_4_41_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90020-G"},{"key":"e_1_3_4_42_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.1202374"},{"key":"e_1_3_4_43_2","unstructured":"David Melski. 1998. Personal communication."},{"key":"e_1_3_4_44_2","doi-asserted-by":"publisher","DOI":"10.5555\/935616"},{"key":"e_1_3_4_45_2","doi-asserted-by":"crossref","unstructured":"David Melski and Thomas Reps. 1999. Interprocedural path profiling. In Compiler Construction. Lecture Notes in Computer Science Vol. 1575. Springer 47\u201362.","DOI":"10.1007\/978-3-540-49051-7_4"},{"key":"e_1_3_4_46_2","volume-title":"Memo Functions: A Language Feature with \u2018Rote-Learning\u2019 Properties","author":"Michie Donald","year":"1967","unstructured":"Donald Michie. 1967. Memo Functions: A Language Feature with \u2018Rote-Learning\u2019 Properties. Technical Report MIP-R-29. Department of Machine Intelligence and Perception, University of Edinburgh, Edinburgh, Scotland."},{"key":"e_1_3_4_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISMVL.2006.35"},{"key":"e_1_3_4_48_2","article-title":"Variable shift SDD: A more succinct sentential decision diagram","author":"Nakamura Kengo","year":"2020","unstructured":"Kengo Nakamura, Shuhei Denzumi, and Masaaki Nishino. 2020. Variable shift SDD: A more succinct sentential decision diagram. arXiv preprint arXiv:2004.02502 (2020).","journal-title":"arXiv preprint arXiv:2004.02502"},{"key":"e_1_3_4_49_2","doi-asserted-by":"crossref","unstructured":"C. Nandi M. Willsey A. Zhu Y. R. Wang B. Saiki A. Anderson A. Schulz D. Grossman and Z. Tatlock. 2021. Rewrite rule inference using equality saturation. Proceedings of the ACM on Programming Languages 5 OOPSLA (2021) Article 119 28 pages.","DOI":"10.1145\/3485496"},{"issue":"2","key":"e_1_3_4_50_2","first-page":"60","article-title":"Quantum computation and quantum information","volume":"54","author":"Nielsen Michael A.","year":"2001","unstructured":"Michael A. Nielsen and Isaac L. Chuang. 2001. Quantum computation and quantum information. Physics Today 54, 2 (2001), 60.","journal-title":"Physics Today"},{"key":"e_1_3_4_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/1344551.1344563"},{"key":"e_1_3_4_52_2","doi-asserted-by":"crossref","unstructured":"O. Polozov and S. Gulwani. 2015. FlashMeta: A framework for inductive program synthesis. ACM SIGPLAN Notices 50 10 (2015) 107\u2013126.","DOI":"10.1145\/2858965.2814310"},{"key":"e_1_3_4_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46674-6_25"},{"key":"e_1_3_4_54_2","volume-title":"Proceedings of the International Logic Programming Symposium (ILPS\u201997)","author":"Reps T.","year":"1997","unstructured":"T. Reps. 1997. Program analysis via graph reachability. In Proceedings of the International Logic Programming Symposium (ILPS\u201997). 5\u201319."},{"key":"e_1_3_4_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_4_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_4_57_2","unstructured":"Thomas W. Reps. 2002. Method for Representing Information in a Highly Compressed Fashion. (June 20 2002). Retrieved March 12 2024 from https:\/\/patentimages.storage.googleapis.com\/ab\/f4\/17\/2bbd2a0fad32f6\/US20020078431A1.pdf"},{"key":"e_1_3_4_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-1385-4"},{"key":"e_1_3_4_59_2","volume-title":"Program Flow Analysis: Theory and Applications","author":"Sharir Micha","year":"1981","unstructured":"Micha Sharir and Amir Pnueli. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications. Prentice Hall."},{"key":"e_1_3_4_60_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2211.06818"},{"key":"e_1_3_4_61_2","article-title":"CUDD: CU Decision Diagram Package\u2013Release 2.4.0","author":"Somenzi Fabio","year":"2012","unstructured":"Fabio Somenzi. 2012. CUDD: CU Decision Diagram Package\u2013Release 2.4.0. University of Colorado at Boulder.","journal-title":"University of Colorado at Boulder."},{"key":"e_1_3_4_62_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008691605584"},{"key":"e_1_3_4_63_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.93.207204"},{"key":"e_1_3_4_64_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.91.147902"},{"key":"e_1_3_4_65_2","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898719789"},{"key":"e_1_3_4_66_2","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_8"},{"key":"e_1_3_4_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996859"},{"key":"e_1_3_4_68_2","unstructured":"M. Willsey. 2021. Fast and Extensible Equality Saturation with Egg. Retrieved March 12 2024 from https:\/\/blog.sigplan.org\/2021\/04\/06\/equality-saturation-with-egg\/"},{"key":"e_1_3_4_69_2","volume-title":"Matrix Product Operator Simulations of Quantum Algorithms","author":"Woolfe Kieran","year":"2015","unstructured":"Kieran Woolfe. 2015. Matrix Product Operator Simulations of Quantum Algorithms. Ph.D. Dissertation. School of Physics, University of Melbourne."},{"key":"e_1_3_4_70_2","doi-asserted-by":"publisher","DOI":"10.1145\/298514.298576"},{"key":"e_1_3_4_71_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_3_4_72_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2834427"},{"key":"e_1_3_4_73_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-41753-6"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3651157","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3651157","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:49:53Z","timestamp":1750286993000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3651157"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,2]]},"references-count":72,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,6,30]]}},"alternative-id":["10.1145\/3651157"],"URL":"https:\/\/doi.org\/10.1145\/3651157","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,5,2]]},"assertion":[{"value":"2023-05-12","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-02-23","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-05-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}