{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:31:13Z","timestamp":1759638673651,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030802226"},{"type":"electronic","value":"9783030802233"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-80223-3_36","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"535-544","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["DQBDD: An Efficient BDD-Based DQBF Solver"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7454-3751","authenticated-orcid":false,"given":"Juraj","family":"S\u00ed\u010d","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5873-403X","authenticated-orcid":false,"given":"Jan","family":"Strej\u010dek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"key":"36_CR1","unstructured":"Balabanov, V., Roland Jiang, J.-H.: Reducing satisfiability and reachability to DQBF, 2015. Talk given at International Workshop on Quantified Boolean Formulas - QBF 2015 (2015)"},{"issue":"1","key":"36_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2017","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. 21(1), 1\u201329 (2017). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"36_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A.: Picosat essentials. J. Satisfiability, Boolean Model. Comput. (JSAT). 4, 75\u201397 (2008)","DOI":"10.3233\/SAT190039"},{"key":"36_CR4","doi-asserted-by":"crossref","unstructured":"Bloem, R., K\u00f6nighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: Verification, Model Checking, and Abstract Interpretation, pp. 1\u201320 (2014)","DOI":"10.1007\/978-3-642-54013-4_1"},{"issue":"8","key":"36_CR5","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"36_CR6","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1109\/12.73590","volume":"40","author":"RE Bryant","year":"1991","unstructured":"Bryant, R.E.: On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Trans. Comput. 40(2), 205\u2013213 (1991)","journal-title":"IEEE Trans. Comput."},{"key":"36_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-09284-3_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"B Finkbeiner","year":"2014","unstructured":"Finkbeiner, B., Tentrup, L.: Fast DQBF refutation. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 243\u2013251. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_19"},{"key":"36_CR8","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A.: A DPLL algorithm for solving DQBF. In: Pragmatics of SAT (PoS 2012, aff. to SAT 2012) (2012)"},{"key":"36_CR9","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A., Veith, H.: iDQ: instantiation-based DQBF solving. In: Le Berre, D. (ed.) POS-14. Fifth Pragmatics of SAT Workshop, A Workshop of the SAT 2014 Conference, part of FLoC 2014 during the Vienna Summer of Logic, 13 July, 2014, Vienna, Austria, volume 27 of EPiC Series in Computing, pp. 103\u2013116. EasyChair (2014)"},{"key":"36_CR10","unstructured":"Ge-Ernst, A., Scholl, C., S\u00ed\u010d, J., Wimmer, R.: Solving dependency quantified Boolean formulas using quantifier localization. Theoretical Computer Science (2021). Submitted. Preprint available as arXiv:1905.04755v2"},{"key":"36_CR11","doi-asserted-by":"crossref","unstructured":"Ge-Ernst, A., Scholl, C., Wimmer, R.: Localizing quantifiers for DQBF. In: Barrett, C.W., Yang, J. (eds.) 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, 22\u201325 October, 2019, pp. 184\u2013192. IEEE (2019)","DOI":"10.23919\/FMCAD.2019.8894269"},{"key":"36_CR12","doi-asserted-by":"crossref","unstructured":"Gitina, K., Reimer, S., Sauer, M., Wimmer, R., Scholl, C., Becker, B.: Equivalence checking of partial designs using dependency quantified Boolean formulae. In: 2013 IEEE 31st International Conference on Computer Design, ICCD 2013, Asheville, NC, USA, 6\u20139 October, 2013, pp. 396\u2013403. IEEE Computer Society (2013)","DOI":"10.1109\/ICCD.2013.6657071"},{"key":"36_CR13","doi-asserted-by":"crossref","unstructured":"Gitina, K., Wimmer, R., Reimer, S., Sauer, M., Scholl, C., Becker, B.:. Solving DQBF through quantifier elimination. In: Nebel, W., Atienza, D. (eds.) Proceedings of the 2015 Design, Automation and Test in Europe Conference and Exhibition, DATE 2015, Grenoble, France, 9\u201313 March, 2015, pp. 1617\u20131622. ACM (2015)","DOI":"10.7873\/DATE.2015.0098"},{"key":"36_CR14","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009)","DOI":"10.1017\/CBO9780511576430"},{"key":"36_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-319-40970-2_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"M Jon\u00e1\u0161","year":"2016","unstructured":"Jon\u00e1\u0161, M., Strej\u010dek, J.: Solving quantified bit-vector formulas using binary decision diagrams. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 267\u2013283. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_17"},{"key":"36_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-030-25543-5_4","volume-title":"Computer Aided Verification","author":"M Jon\u00e1\u0161","year":"2019","unstructured":"Jon\u00e1\u0161, M., Strej\u010dek, J.: Q3B: an efficient BDD-based SMT solver for quantified bit-vectors. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 64\u201373. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_4"},{"key":"36_CR17","unstructured":"Jordan, C., Klieber, W., Seidl, M.: Non-CNF QBF solving with QCIR. Beyond NP. In: AAAI Workshop (2016)"},{"key":"36_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292\u2013298. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_24"},{"key":"36_CR19","unstructured":"Kov\u00e1sznai, G.: What is the state-of-the-art in DQBF solving. In: MaCS-16. Joint Conference on Mathematics and Computer Science (2016)"},{"key":"36_CR20","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.: FRAIGs: a unifying representation for logic synthesis and verification. EECS Dept., UC Berkeley, Technical report (2005)"},{"key":"36_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/978-3-642-23786-7_51","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"O Olivo","year":"2011","unstructured":"Olivo, O., Emerson, E.A.: A more efficient BDD-based QBF solver. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 675\u2013690. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23786-7_51"},{"issue":"7","key":"36_CR22","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1016\/S0898-1221(00)00333-3","volume":"41","author":"G Peterson","year":"2001","unstructured":"Peterson, G., Reif, J., Azhar, S.: Lower bounds for multiplayer noncooperative games of incomplete information. Comput. Math. Appl. 41(7), 957\u2013992 (2001)","journal-title":"Comput. Math. Appl."},{"key":"36_CR23","unstructured":"Pulina, L., Seidl, M.: QBF evaluation 2018 (2018)"},{"key":"36_CR24","unstructured":"Pulina, L., Seidl, M., Shukla, A.: QBF evaluation 2019 (2019)"},{"key":"36_CR25","unstructured":"Pulina, L., Seidl, M., Shukla, A.: QBF evaluation 2020 (2020)"},{"key":"36_CR26","unstructured":"Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of 1993 International Conference on Computer Aided Design (ICCAD), pp. 42\u201347 (1993)"},{"key":"36_CR27","doi-asserted-by":"crossref","unstructured":"Scholl, C., Becker, B.: Checking equivalence for partial implementations. In: Proceedings of the 38th Design Automation Conference (IEEE Cat. No.01CH37232), pp. 238\u2013243 (2001)","DOI":"10.1145\/378239.378471"},{"key":"36_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-94144-8_1","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"C Scholl","year":"2018","unstructured":"Scholl, C., Wimmer, R.: Dependency quantified Boolean formulas: an overview of solution methods and applications. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 3\u201316. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_1"},{"key":"36_CR29","unstructured":"Schubert, T., Lewis, M., Becker, B.: Antom - solver description (2010)"},{"key":"36_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1007\/978-3-030-53288-8_24","volume-title":"Computer Aided Verification","author":"F Slivovsky","year":"2020","unstructured":"Slivovsky, F.: Interpolation-based semantic gate extraction and its applications to QBF preprocessing. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 508\u2013528. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_24"},{"key":"36_CR31","unstructured":"Somenzi, F.: CUDD: CU decision diagram package release 3.0.0 (2015)"},{"key":"36_CR32","unstructured":"S\u00ed\u010d, J.: Satisfiability of DQBF using binary decision diagrams. Master\u2019s thesis, Masaryk University, Faculty of Informatics (2020)"},{"key":"36_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-030-24258-9_27","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"L Tentrup","year":"2019","unstructured":"Tentrup, L., Rabe, M.N.: Clausal abstraction for DQBF. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 388\u2013405. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_27"},{"key":"36_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-319-66263-3_21","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"R Wimmer","year":"2017","unstructured":"Wimmer, R., Karrenbauer, A., Becker, R., Scholl, C., Becker, B.: From DQBF to QBF by dependency elimination. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 326\u2013343. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_21"},{"key":"36_CR35","doi-asserted-by":"publisher","first-page":"3","DOI":"10.3233\/SAT190115","volume":"11","author":"R Wimmer","year":"2019","unstructured":"Wimmer, R., Scholl, C., Becker, B.: The (D)QBF preprocessor HQSpre - underlying theory and its implementation. J. Satisfiability Boolean Model. Comput. 11, 3\u201352 (2019)","journal-title":"J. Satisfiability Boolean Model. Comput."}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2021"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-80223-3_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T23:37:39Z","timestamp":1625182659000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"2 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Barcelona","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.iiia.csic.es\/sat2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}