{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,5]],"date-time":"2026-05-05T05:06:06Z","timestamp":1777957566071,"version":"3.51.4"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030802226","type":"print"},{"value":"9783030802233","type":"electronic"}],"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_4","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"30-46","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Davis and Putnam Meet Henkin: Solving DQBF with Resolution"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7452-6521","authenticated-orcid":false,"given":"Joshua","family":"Blinkhorn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7799-1568","authenticated-orcid":false,"given":"Tom\u00e1\u0161","family":"Peitl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1784-2346","authenticated-orcid":false,"given":"Friedrich","family":"Slivovsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1016\/S0898-1221(00)00333-3","volume":"41","author":"S Azhar","year":"2001","unstructured":"Azhar, S., Peterson, G., Reif, J.: Lower bounds for multiplayer non-cooperative games of incomplete information. J. Comput. Math. Appl. 41, 957\u2013992 (2001)","journal-title":"J. Comput. Math. Appl."},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1016\/j.tcs.2013.12.020","volume":"523","author":"V Balabanov","year":"2014","unstructured":"Balabanov, V., Chiang, H.K., Jiang, J.R.: Henkin quantifiers and Boolean formulae: a certification perspective of DQBF. Theor. Comput. Sci. 523, 86\u2013100 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Baldoni, R., Coppa, E., D\u2019Elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. 51(3), 50:1\u201350:39 (2018)","DOI":"10.1145\/3182657"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Blinkhorn, J., Mahajan, M.: Building strategies into QBF proofs. J. Autom. Reasoning (2020). (in Press)","DOI":"10.1007\/s10817-020-09560-1"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/b95238","volume-title":"Theory and Applications of Satisfiability Testing","year":"2004","unstructured":"Giunchiglia, E., Tacchella, A. (eds.): SAT 2003. LNCS, vol. 2919. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/b95238"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/11814948_21","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"U Bubeck","year":"2006","unstructured":"Bubeck, U., B\u00fcning, H.K.: Dependency quantified horn formulas: models and complexity. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 198\u2013211. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_21"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Buss, S.R., Hoffmann, J., Johannsen, J.: resolution trees with lemmas: resolution refinements that characterize DLL algorithms with clause learning. Logical Methods Comput. Sci. 4, (4), (2008). https:\/\/doi.org\/10.2168\/LMCS-4(4:13)2008, https:\/\/lmcs.episciences.org\/860","DOI":"10.2168\/LMCS-4(4:13)2008"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Buss, S.R., Kolodziejczyk, L.A.: Small stone in pool. Logical Methods Comput. Sci. 10(2), (2014). https:\/\/doi.org\/10.2168\/LMCS-10(2:16)2014, https:\/\/lmcs.episciences.org\/852","DOI":"10.2168\/LMCS-10(2:16)2014"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Cashmore, M., Fox, M., Long, D., Magazzeni, D.: A compilation of the full PDDL+ language into SMT. In: Coles, A.J., Coles, A., Edelkamp, S., Magazzeni, D., Sanner, S. (eds.) Proceedings of the Twenty-Sixth International Conference on Automated Planning and Scheduling, ICAPS 2016, pp. 79\u201387. AAAI Press (2016)","DOI":"10.1609\/icaps.v26i1.13755"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. 17, 229\u2013264 (2002) (electronic)","DOI":"10.1613\/jair.989"},{"issue":"3","key":"4_CR12","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-662-54577-5_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 354\u2013370. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_20"},{"key":"4_CR14","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A.: A DPLL algorithm for solving DQBF, presented at Workshop on Pragmatics of SAT (POS) (2012). https:\/\/arise.or.at\/pubpdf\/Algorithm_for_Solving__DQBF_.pdf"},{"key":"4_CR15","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A., Veith, H.: iDQ: instantiation-based DQBF solving. In: Berre, D.L. (ed.) Workshop on Pragmatics of SAT (POS). EPiC Series in Computing, vol. 27, pp. 103\u2013116. EasyChair (2014)"},{"key":"4_CR16","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: IEEE 31st International Conference on Computer Design, ICCD 2013, pp. 396\u2013403. IEEE Computer Society (2013)","DOI":"10.1109\/ICCD.2013.6657071"},{"key":"4_CR17","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.) Design, Automation & Test in Europe Conference (DATE), pp. 1617\u20131622. ACM (2015)","DOI":"10.7873\/DATE.2015.0098"},{"issue":"1","key":"4_CR18","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H Kleine B\u00fcning","year":"1995","unstructured":"Kleine B\u00fcning, H., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"4_CR19","unstructured":"Meel, K.S., et al.: constrained sampling and counting: universal hashing meets SAT solving. In: Darwiche, A. (ed.) Beyond NP. AAAI Workshops, vol. WS-16-05. AAAI Press (2016)"},{"issue":"3","key":"4_CR20","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"DA Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symbolic Comput. 2(3), 293\u2013304 (1986). https:\/\/doi.org\/10.1016\/S0747-7171(86)80028-1","journal-title":"J. Symbolic Comput."},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-319-40970-2_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MN Rabe","year":"2016","unstructured":"Rabe, M.N., Seshia, S.A.: Incremental determinization. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 375\u2013392. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_23"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Randal E. Bryant: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35(8), 677\u2013691 (1986). https:\/\/doi.org\/10.1109\/TC.1986.1676819","DOI":"10.1109\/TC.1986.1676819"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Scholl, C., Jiang, J.R., Wimmer, R., Ge-Ernst, A.: A PSPACE subclass of dependency quantified Boolean formulas and its effective solving. In: The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, pp. 1584\u20131591. AAAI Press (2019)","DOI":"10.1609\/aaai.v33i01.33011584"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: Shen, J.P., Martonosi, M. (eds.) Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2006, pp. 404\u2013415. ACM (2006)","DOI":"10.1145\/1168857.1168907"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: Preliminary report. In: Aho, A.V., et al. (eds.) ACM Symposium on Theory of Computing (STOC), pp. 1\u20139. ACM (1973)","DOI":"10.1145\/800125.804029"},{"key":"4_CR26","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","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":"4_CR27","first-page":"115","volume":"2","author":"GS Tseitin","year":"1968","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. Stud. Constructive Math. Math. Logic Part 2, 115\u2013125 (1968)","journal-title":"Stud. Constructive Math. Math. Logic Part"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Vizel, Y., Weissenbacher, G., Malik, S.: Boolean satisfiability solvers and their applications in model checking. Proc. IEEE 103(11), 2021\u20132035 (2015)","DOI":"10.1109\/JPROC.2015.2455034"}],"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_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,5]],"date-time":"2023-11-05T14:33:02Z","timestamp":1699194782000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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"}}]}}