{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T07:41:08Z","timestamp":1768722068782,"version":"3.49.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031757778","type":"print"},{"value":"9783031757785","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-75778-5_12","type":"book-chapter","created":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T12:09:11Z","timestamp":1731845351000},"page":"252-273","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Compiling Binary Decision Diagrams with\u00a0Interrupt-Based Downsizing"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5718-8276","authenticated-orcid":false,"given":"Clemens","family":"Dubslaff","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joshua","family":"Wirtz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,18]]},"reference":[{"issue":"12","key":"12_CR1","doi-asserted-by":"publisher","first-page":"1562","DOI":"10.3217\/jucs-010-12-1562","volume":"10","author":"FA Aloul","year":"2004","unstructured":"Aloul, F.A., Markov, I.L., Sakallah, K.A.: MINCE: a static global variable-ordering heuristic for SAT search and BDD manipulation. JUCS 10(12), 1562\u20131596 (2004). https:\/\/doi.org\/10.3217\/jucs-010-12-1562","journal-title":"JUCS"},{"key":"12_CR2","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking, chap. 6.7.3 Ordered Binary Decision Diagrams, pp. 395\u2013407. The MIT Press (2008)"},{"key":"12_CR3","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"713","DOI":"10.1007\/978-3-031-06773-0_38","volume-title":"NFM 2022","author":"D Basg\u00f6ze","year":"2022","unstructured":"Basg\u00f6ze, D., Volk, M., Katoen, J., Khan, S., Stoelinga, M.: BDDs strike back - efficient analysis of static and dynamic fault trees. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NFM 2022. LNCS, vol. 13260, pp. 713\u2013732. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_38"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA336","DOI":"10.3233\/FAIA336"},{"issue":"9","key":"12_CR5","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"B Bollig","year":"1996","unstructured":"Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993\u20131002 (1996). https:\/\/doi.org\/10.1109\/12.537122","journal-title":"IEEE Trans. Comput."},{"issue":"3","key":"12_CR6","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992). https:\/\/doi.org\/10.1145\/136035.136043","journal-title":"ACM Comput. Surv."},{"issue":"2","key":"12_CR7","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10$$^{20}$$ states and beyond. Inform. Comp. 98(2), 142\u2013170 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90017-A","journal-title":"Inform. Comp."},{"key":"12_CR8","unstructured":"Cadoli, M., Donini, F.M.: A survey on knowledge compilation. AI Commun. 10, 137\u2013150 (1997). https:\/\/api.semanticscholar.org\/CorpusID:16746005"},{"key":"12_CR9","unstructured":"Clarke, E.M., Fujita, M., McGeers, P.C., McMillan, K.L., Yang, J.C., Zhao, X.: Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. In: IWLS (1993)"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"de\u00a0Colnet, A.: Separating incremental and non-incremental bottom-up compilation. In: Mahajan, M., Slivovsky, F. (eds.) 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, 4\u20138 July 2023, Alghero, Italy. LIPIcs, vol.\u00a0271, pp. 7:1\u20137:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2023.7","DOI":"10.4230\/LIPIcs.SAT.2023.7"},{"key":"12_CR11","unstructured":"Compile! Project: Benchmarks (2023). https:\/\/www.cril.univ-artois.fr\/kc\/benchmarks.html. Accessed 11 Jan 2023"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Coudert, O., Madre, J.: A unified framework for the formal verification of sequential circuits. In: 1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers, pp. 126\u2013129 (1990). https:\/\/doi.org\/10.1109\/ICCAD.1990.129859","DOI":"10.1109\/ICCAD.1990.129859"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Coudert, O., Madre, J.: Fault tree analysis: 1020 prime implicants and beyond, pp. 240\u2013245 (1993). https:\/\/doi.org\/10.1109\/RAMS.1993.296849","DOI":"10.1109\/RAMS.1993.296849"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Crama, Y., Hammer, P.L.: Boolean Functions: Theory, Algorithms, and Applications. Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge (2011). https:\/\/doi.org\/10.1017\/CBO9780511852008","DOI":"10.1017\/CBO9780511852008"},{"key":"12_CR15","unstructured":"Darwiche, A.: A compiler for deterministic, decomposable negation normal form. In: AAAI, pp. 627\u2013634. AAAI Press, USA (2002). https:\/\/dl.acm.org\/doi\/10.5555\/777092.777189"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Int. Res. 17(1), 229\u2013264 (2002)","DOI":"10.1613\/jair.989"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"van Dijk, T., van de Pol, J.: Sylvan: multi-core framework for decision diagrams. Int. J. Softw. Tools Technol. Transfer 19(6), 675\u2013696 (2017)","DOI":"10.1007\/s10009-016-0433-2"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Dubslaff, C., Husung, N., K\u00e4fer, N.: Configuring BDD compilation techniques for feature models. In: Proceedings of the 28th ACM International Systems and Software Product Line Conference - Volume A, SPLC 2024, pp. 209\u2013216. Association for Computing Machinery, New York (2024). https:\/\/doi.org\/10.1145\/3646548.3676538","DOI":"10.1145\/3646548.3676538"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Fernandez-Amoros, D., Bra, S., Aranda-Escol\u00e1stico, E., Heradio, R.: Using extended logical primitives for efficient BDD building. Mathematics 8(8) (2020). https:\/\/doi.org\/10.3390\/math8081253. https:\/\/www.mdpi.com\/2227-7390\/8\/8\/1253","DOI":"10.3390\/math8081253"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/3-540-08860-1_17","volume-title":"Automata, Languages and Programming","author":"S Fortune","year":"1978","unstructured":"Fortune, S., Hopcroft, J., Schmidt, E.M.: The complexity of equivalence and containment for free single variable program schemes. In: Ausiello, G., B\u00f6hm, C. (eds.) ICALP 1978. LNCS, vol. 62, pp. 227\u2013240. Springer, Heidelberg (1978). https:\/\/doi.org\/10.1007\/3-540-08860-1_17"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/11527695_13","volume-title":"Theory and Applications of Satisfiability Testing","author":"J Huang","year":"2005","unstructured":"Huang, J., Darwiche, A.: Using DPLL for efficient OBDD construction. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 157\u2013172. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11527695_13"},{"key":"12_CR23","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57256-2_13","volume-title":"TACAS 2024","author":"N Husung","year":"2024","unstructured":"Husung, N., Dubslaff, C., Hermanns, H., K\u00f6hl, M.A.: OxiDD: a safe, concurrent, modular, and performant decision diagram framework in Rust. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) TACAS 2024. LNCS, vol. 14572. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_13"},{"key":"12_CR24","unstructured":"Jain, J., et al.: Combining top-down and bottom-up approaches for ROBDD. Technical report, USA (1995)"},{"key":"12_CR25","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume 4, Fascicle 1: Bitwise Tricks & Techniques; Binary Decision Diagrams, 12th edn. Addison-Wesley Professional (2009)"},{"key":"12_CR26","doi-asserted-by":"publisher","unstructured":"Lagniez, J.M., Marquis, P.: Preprocessing for propositional model counting. In: AAAI, pp. 2688\u20132694. AAAI Press (2014). https:\/\/doi.org\/10.1609\/AAAI.V28I1.9116","DOI":"10.1609\/AAAI.V28I1.9116"},{"key":"12_CR27","unstructured":"Lind-Nielsen, J.: BuDDy: a binary decision diagram package, version 2.4 (2004). https:\/\/buddy.sourceforge.net\/manual\/"},{"key":"12_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-58940-9","volume-title":"Algorithms and Data Structures in VLSI Design","author":"C Meinel","year":"1998","unstructured":"Meinel, C., Theobald, T.: Algorithms and Data Structures in VLSI Design, 1st edn. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/978-3-642-58940-9","edition":"1"},{"key":"12_CR29","unstructured":"O\u2019Donnell, R.: Analysis of Boolean Functions. Cambridge University Press, Cambridge (2014)"},{"key":"12_CR30","unstructured":"Popov, M., Balyo, T., Iser, M., Ostertag, T.: Construction of decision diagrams for product configuration. In: Horcas, J.M., Galindo, J.A., Comploi-Taupe, R., Fuentes, L. (eds.) ConfWS. CEUR Workshop Proceedings, vol.\u00a03509, pp. 108\u2013117. CEUR-WS.org (2023). https:\/\/ceur-ws.org\/Vol-3509\/paper15.pdf"},{"key":"12_CR31","doi-asserted-by":"publisher","unstructured":"Qayyum, K., Mahzoon, A., Drechsler, R.: Monitoring the effects of static variable orders on the construction of BDDS (2022). https:\/\/doi.org\/10.1109\/mesiicon55227.2022.10093493","DOI":"10.1109\/mesiicon55227.2022.10093493"},{"key":"12_CR32","doi-asserted-by":"publisher","unstructured":"Ravi, K., McMillan, K.L., Shiple, T.R., Somenzi, F.: Approximation and decomposition of binary decision diagrams. In: Proceedings of the 35th Annual Design Automation Conference, DAC 1998, pp. 445\u2013450. Association for Computing Machinery, New York (1998). https:\/\/doi.org\/10.1145\/277044.277168","DOI":"10.1145\/277044.277168"},{"key":"12_CR33","doi-asserted-by":"publisher","unstructured":"Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Lightner, M.R., Jess, J.A.G. (eds.) Proceedings of the 1993 IEEE\/ACM International Conference on Computer-Aided Design, pp. 42\u201347. IEEE Computer Society\/ACM (1993). https:\/\/doi.org\/10.1109\/ICCAD.1993.580029","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"12_CR34","unstructured":"Shiple, T.R.: Formal Analysis of Synchronous Circuits. University of California, Berkeley (1996)"},{"key":"12_CR35","unstructured":"Shiple, T.R.: Deciding state reachability for large FSMs. Electronics Research Laboratory, College of Engineering, University of .. (1997)"},{"key":"12_CR36","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-031-45332-8_4","volume-title":"Automated Technology for Verification and Analysis","author":"SC S\u00f8lvsten","year":"2023","unstructured":"S\u00f8lvsten, S.C., van de Pol, J.: Predicting memory demands of BDD operations using maximum graph cuts. In: Andr\u00e9, \u00c9., Sun, J. (eds.) ATVA 2023. LNCS, vol. 14216, pp. 72\u201392. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45332-8_4"},{"key":"12_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-030-99527-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"SC S\u00f8lvsten","year":"2022","unstructured":"S\u00f8lvsten, S.C., de Pol, J., Jakobsen, A.B., Thomasen, M.W.B.: Adiar binary decision diagrams in external memory. In: Andre, E., Sun, J. (eds.) TACAS 2022. LNCS, vol. 13244, pp. 295\u2013313. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_16"},{"key":"12_CR38","unstructured":"Somenzi, F.: CUDD: CU decision diagram package. Technical report, University of Colorado at Boulder (2015)"},{"key":"12_CR39","doi-asserted-by":"publisher","unstructured":"Yang, B., Chen, Y.A., Bryant, R., O\u2019Hallaron, D.: Space- and time-efficient BDD construction via working set control. In: Proceedings of 1998 Asia and South Pacific Design Automation Conference, pp. 423\u2013432 (1998). https:\/\/doi.org\/10.1109\/ASPDAC.1998.669515","DOI":"10.1109\/ASPDAC.1998.669515"}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75778-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T13:03:01Z","timestamp":1731848581000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75778-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,18]]},"ISBN":["9783031757778","9783031757785"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75778-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,18]]},"assertion":[{"value":"18 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}