{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:36:05Z","timestamp":1740123365417,"version":"3.37.3"},"reference-count":59,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2020,5,22]],"date-time":"2020-05-22T00:00:00Z","timestamp":1590105600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,5,22]],"date-time":"2020-05-22T00:00:00Z","timestamp":1590105600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100000925","name":"John Templeton Foundation","doi-asserted-by":"publisher","award":["60842"],"award-info":[{"award-number":["60842"]}],"id":[{"id":"10.13039\/100000925","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007569","name":"Carl-Zeiss-Stiftung","doi-asserted-by":"crossref","award":["Grant for returning scientists"],"award-info":[{"award-number":["Grant for returning scientists"]}],"id":[{"id":"10.13039\/100007569","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Strategy extraction is of great importance for quantified Boolean formulas (QBF), both in solving and proof complexity. So far in the QBF literature, strategy extraction has been algorithmically performed<jats:italic>from<\/jats:italic>proofs. Here we devise the first QBF system where (partial) strategies are built<jats:italic>into<\/jats:italic>the proof and are piecewise constructed by simple operations along with the derivation. This has several advantages: (1) lines of our calculus have a clear semantic meaning as they are accompanied by semantic objects; (2) partial strategies are represented succinctly (in contrast to some previous approaches); (3) our calculus has strategy extraction by design; and (4) the partial strategies allow new sound inference steps which are disallowed in previous central QBF calculi such as Q-Resolution and long-distance Q-Resolution. The last item (4) allows us to show an exponential separation between our new system and the previously studied reductionless long-distance resolution calculus. Our approach also naturally lifts to dependency QBFs (DQBF), where it yields the first sound and complete CDCL-style calculus for DQBF, thus opening future avenues into CDCL-based DQBF solving.<\/jats:p>","DOI":"10.1007\/s10817-020-09560-1","type":"journal-article","created":{"date-parts":[[2020,5,22]],"date-time":"2020-05-22T17:02:40Z","timestamp":1590166960000},"page":"125-154","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Building Strategies into QBF Proofs"],"prefix":"10.1007","volume":"65","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2870-1648","authenticated-orcid":false,"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[]},{"given":"Joshua","family":"Blinkhorn","sequence":"additional","affiliation":[]},{"given":"Meena","family":"Mahajan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,5,22]]},"reference":[{"key":"9560_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":"9560_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.-J.K., Jiang, J.-H.R.: Henkin quantifiers and Boolean formulae: a certification perspective of DQBF. Theoret. Comput. Sci. 523, 86\u2013100 (2014)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"9560_CR3","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","volume":"41","author":"V Balabanov","year":"2012","unstructured":"Balabanov, V., Jiang, J.-H.R.: Unified QBF certification and its applications. Form. Methods Syst. Des. 41(1), 45\u201365 (2012)","journal-title":"Form. Methods Syst. Des."},{"key":"9560_CR4","doi-asserted-by":"crossref","unstructured":"Balabanov, V., Jiang, J.-H.R., Janota, M., Widl, M.: Efficient extraction of QBF (counter)models from long-distance resolution proofs. In: Bonet, B., Koenig, S. (eds.) National Conference on Artificial Intelligence (AAAI), pp. 3694\u20133701. AAAI Press (2015)","DOI":"10.1609\/aaai.v29i1.9750"},{"key":"9560_CR5","doi-asserted-by":"crossref","unstructured":"Benedetti, M.: sKizzo: a suite to evaluate and certify QBFs. In: Nieuwenhuis, R. (ed.) International Conference on Automated Deduction (CADE), Volume 3632 of Lecture Notes in Computer Science, pp. 369\u2013376. Springer (2005)","DOI":"10.1007\/11532231_27"},{"issue":"1\u20134","key":"9560_CR6","first-page":"133","volume":"5","author":"M Benedetti","year":"2008","unstructured":"Benedetti, M., Mangassarian, H.: QBF-based formal verification: experience and perspectives. J. Satisf. Boolean Model. Comput. 5(1\u20134), 133\u2013191 (2008)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"9560_CR7","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Blinkhorn, J. (2016) Dependency schemes in QBF calculi: semantics and soundness. In: Rueher, M. (ed.) International Conference on Principles and Practice of Constraint Programming (CP), Volume 9892 of Lecture Notes in Computer Science, pp. 96\u2013112. Springer","DOI":"10.1007\/978-3-319-44953-1_7"},{"issue":"3","key":"9560_CR8","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1007\/s10817-018-9482-4","volume":"63","author":"O Beyersdorff","year":"2019","unstructured":"Beyersdorff, O., Blinkhorn, J., Chew, L., Schmidt, R.A., Suda, M.: Reinterpreting dependency schemes: soundness meets incompleteness in DQBF. J. Autom. Reason. 63(3), 597\u2013623 (2019)","journal-title":"J. Autom. Reason."},{"key":"9560_CR9","unstructured":"Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost, and capacity: a semantic technique for hard random QBFs. Log. Methods Comput. Sci. 15(1), 13:1\u201313:39 (2019)"},{"key":"9560_CR10","unstructured":"Beyersdorff, O., Blinkhorn, J., Mahajan, M.: Building strategies into QBF proofs. In: Niedermeier, R., Paul, C. (ed.) International Symposium on Theoretical Aspects of Computer Science (STACS), Volume 126 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 14:1\u201314:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"9560_CR11","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Bonacina, I., Chew, L.: Lower bounds: from circuits to QBF proof systems. In: Sudan, M. (ed.) ACM Conference on Innovations in Theoretical Computer Science (ITCS), pp. 249\u2013260. ACM (2016)","DOI":"10.1145\/2840728.2840740"},{"issue":"4","key":"9560_CR12","doi-asserted-by":"publisher","first-page":"26:1","DOI":"10.1145\/3352155","volume":"11","author":"O Beyersdorff","year":"2019","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: New resolution-based QBF calculi and their proof complexity. ACM Trans. Comput. Theory 11(4), 26:1\u201326:42 (2019)","journal-title":"ACM Trans. Comput. Theory"},{"key":"9560_CR13","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Chew, L., Schmidt, R.A., Suda, M.: Lifting QBF resolution calculi to DQBF. In: Creignou and Berre [21], pp. 490\u2013499","DOI":"10.1007\/978-3-319-40970-2_30"},{"volume-title":"International Conference on Theory and Practice of Satisfiability Testing (SAT), Volume 10929 of Lecture Notes in Computer Science","year":"2018","key":"9560_CR14","unstructured":"Beyersdorff, O., Wintersteiger, C.M. (eds.): International Conference on Theory and Practice of Satisfiability Testing (SAT), Volume 10929 of Lecture Notes in Computer Science. Springer, Berlin (2018)"},{"key":"9560_CR15","unstructured":"Bj\u00f8rner, N., Janota, M., Klieber, W.: On conflicts and strategies in QBF. In: Fehnker, A., McIver, A., Sutcliffe, G., Voronkov, A. (eds.) International Conference on Logic for Programming, Artificial Intelligence and Reasoning\u2014Short Presentations (LPAR), Volume 35 of EPiC Series in Computing, pp. 28\u201341. EasyChair (2015)"},{"key":"9560_CR16","doi-asserted-by":"crossref","unstructured":"Bubeck, U., B\u00fcning, H.K.: Dependency quantified Horn formulas: models and complexity. In: Biere, A., Gomes, C.P. (eds.) International Conference on Theory and Practice of Satisfiability Testing (SAT), Volume 4121 of Lecture Notes in Computer Science, pp. 198\u2013211. Springer (2006)","DOI":"10.1007\/11814948_21"},{"issue":"7","key":"9560_CR17","doi-asserted-by":"publisher","first-page":"906","DOI":"10.1016\/j.apal.2011.09.009","volume":"163","author":"SR Buss","year":"2012","unstructured":"Buss, S.R.: Towards NP-P via proof complexity and search. Ann. Pure Appl. Log. 163(7), 906\u2013917 (2012)","journal-title":"Ann. Pure Appl. Log."},{"key":"9560_CR18","doi-asserted-by":"crossref","unstructured":"Cashmore, M., Fox, M., Giunchiglia, E.: Partially grounded planning as quantified Boolean formula. In: Borrajo, D., Kambhampati, S., Oddi, A., Fratini, S. (eds.) International Conference on Automated Planning and Scheduling (ICAPS). AAAI (2013)","DOI":"10.1609\/icaps.v23i1.13549"},{"key":"9560_CR19","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511676277","volume-title":"Logical Foundations of Proof Complexity","author":"SA Cook","year":"2010","unstructured":"Cook, S.A., Nguyen, P.: Logical Foundations of Proof Complexity. Cambridge University Press, Cambridge (2010)"},{"issue":"1","key":"9560_CR20","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36\u201350 (1979)","journal-title":"J. Symb. Log."},{"volume-title":"International Conference on Theory and Practice of Satisfiability Testing (SAT). Lecture Notes in Computer Science","year":"2016","key":"9560_CR21","unstructured":"Creignou, N., Le Berre, D. (eds.): International Conference on Theory and Practice of Satisfiability Testing (SAT). Lecture Notes in Computer Science, vol. 9710. Springer, Berlin (2016)"},{"issue":"1","key":"9560_CR22","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10472-016-9501-2","volume":"80","author":"U Egly","year":"2017","unstructured":"Egly, U., Kronegger, M., Lonsing, F., Pfandler, A.: Conformant planning as a case study of incremental QBF solving. Ann. Math. Artif. Intell. 80(1), 21\u201345 (2017)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9560_CR23","doi-asserted-by":"crossref","unstructured":"Egly, U., Lonsing, F., Widl, M.: Long-distance resolution: proof generation and strategy extraction in search-based QBF solving. In: McMillan, K.L., Middeldorp, K.L., Voronkov, A. (eds.) International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Volume 8312 of Lecture Notes in Computer Science, pp. 291\u2013308. Springer (2013)","DOI":"10.1007\/978-3-642-45221-5_21"},{"key":"9560_CR24","doi-asserted-by":"crossref","unstructured":"Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: Legay and Margaria [39], pp. 354\u2013370","DOI":"10.1007\/978-3-662-54577-5_20"},{"key":"9560_CR25","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Tentrup, L.: Fast DQBF refutation. In: Sinz, C., Egly, U. (eds.) International Conference on Theory and Practice of Satisfiability Testing (SAT), Volume 8561 of Lecture Notes in Computer Science, pp. 243\u2013251. Springer (2014)","DOI":"10.1007\/978-3-319-09284-3_19"},{"key":"9560_CR26","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A.: A DPLL algorithm for solving DQBF. https:\/\/arise.or.at\/pubpdf\/Algorithm_for_Solving__DQBF_.pdf, presented at Workshop on Pragmatics of SAT (POS) (2012)"},{"key":"9560_CR27","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A., Veith, H.: iDQ: instantiation-based DQBF solving. In: Le Berre, D. (ed.) Workshop on Pragmatics of SAT (POS), Volume 27 of EPiC Series in Computing, pp. 103\u2013116. EasyChair (2014)"},{"volume-title":"International Conference on Theory and Practice of Satisfiability Testing (SAT). Lecture Notes in Computer Science","year":"2017","key":"9560_CR28","unstructured":"Gaspers, S., Walsh, T. (eds.): International Conference on Theory and Practice of Satisfiability Testing (SAT). Lecture Notes in Computer Science, vol. 10491. Springer, Berlin (2017)"},{"key":"9560_CR29","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"},{"key":"9560_CR30","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1613\/jair.1959","volume":"26","author":"E Giunchiglia","year":"2006","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause\/term resolution and learning in the evaluation of quantified Boolean formulas. J. Artif. Intell. Res. 26, 371\u2013416 (2006)","journal-title":"J. Artif. Intell. Res."},{"key":"9560_CR31","doi-asserted-by":"crossref","unstructured":"Heule, M., Seidl, M., Biere, A.: Efficient extraction of Skolem functions from QRAT proofs. In: Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 107\u2013114. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987602"},{"issue":"8","key":"9560_CR32","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/3107239","volume":"60","author":"MJH Heule","year":"2017","unstructured":"Heule, M.J.H., Kullmann, O.: The science of brute force. Commun. ACM 60(8), 70\u201379 (2017)","journal-title":"Commun. ACM"},{"volume-title":"International Conference on Theory and Practice of Satisfiability Testing (SAT). Lecture Notes in Computer Science","year":"2019","key":"9560_CR33","unstructured":"Janota, M., Lynce, I. (eds.): International Conference on Theory and Practice of Satisfiability Testing (SAT). Lecture Notes in Computer Science, vol. 11628. Springer, Berlin (2019)"},{"key":"9560_CR34","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.tcs.2015.01.048","volume":"577","author":"M Janota","year":"2015","unstructured":"Janota, M., Marques-Silva, J.: Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci. 577, 25\u201342 (2015)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"9560_CR35","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"HK B\u00fcning","year":"1995","unstructured":"B\u00fcning, H.K., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"9560_CR36","doi-asserted-by":"crossref","unstructured":"Klieber, W., Sapra, S., Gao, S., Clarke, E.M.: A non-prenex, non-clausal QBF solver with game-state learning. In: Strichman, O., Szeider, S. (eds.) International Conference on Theory and Practice of Satisfiability Testing (SAT), Volume 6175 of Lecture Notes in Computer Science, pp. 128\u2013142. Springer (2010)","DOI":"10.1007\/978-3-642-14186-7_12"},{"key":"9560_CR37","unstructured":"Kontchakov, R., Pulina, L., Sattler, U., Schneider, T., Selmer, P., Wolter, F., Zakharyaschev, M.: Minimal module extraction from DL-lite ontologies using QBF solvers. In: Boutilier, C. (ed.) International Joint Conference on Artificial Intelligence (IJCAI), pp. 836\u2013841. AAAI Press (2009)"},{"key":"9560_CR38","volume-title":"Bounded Arithmetic, Propositional Logic, and Complexity Theory. Encyclopedia of Mathematics and Its Applications","author":"J Kraj\u00ed\u010dek","year":"1995","unstructured":"Kraj\u00ed\u010dek, J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory. Encyclopedia of Mathematics and Its Applications, vol. 60. Cambridge University Press, Cambridge (1995)"},{"key":"9560_CR39","doi-asserted-by":"crossref","unstructured":"Legay, Axel, Margaria, Tiziana (eds.): International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 10205. Springer, (2017)","DOI":"10.1007\/978-3-662-54577-5"},{"key":"9560_CR40","doi-asserted-by":"crossref","unstructured":"Ling, A.C., Singh, D.P., Brown, S.D.: FPGA logic synthesis using quantified Boolean satisfiability. In: Bacchus, F., Walsh, T. (eds.), International Conference on Theory and Practice of Satisfiability Testing (SAT), Volume 3569 of Lecture Notes in Computer Science, pp. 444\u2013450. Springer (2005)","DOI":"10.1007\/11499107_37"},{"issue":"7","key":"9560_CR41","doi-asserted-by":"publisher","first-page":"981","DOI":"10.1109\/TC.2010.74","volume":"59","author":"H Mangassarian","year":"2010","unstructured":"Mangassarian, H., Veneris, A.G., Benedetti, M.: Robust QBF encodings for sequential circuits with applications to verification, debug, and test. IEEE Trans. Comput. 59(7), 981\u2013994 (2010)","journal-title":"IEEE Trans. Comput."},{"key":"9560_CR42","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Malik, S.: Propositional SAT solving. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 247\u2013275. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_9"},{"issue":"3","key":"9560_CR43","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/2815493.2815497","volume":"2","author":"J Nordstr\u00f6m","year":"2015","unstructured":"Nordstr\u00f6m, J.: On the interplay between proof complexity and SAT solving. SIGLOG News 2(3), 19\u201344 (2015)","journal-title":"SIGLOG News"},{"key":"9560_CR44","doi-asserted-by":"crossref","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Long distance Q-resolution with dependency schemes. In: Creignou and Berre [21], pp. 500\u2013518","DOI":"10.1007\/978-3-319-40970-2_31"},{"key":"9560_CR45","doi-asserted-by":"crossref","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Dependency learning for QBF. In: Gaspers and Walsh [28], pp. 298\u2013313","DOI":"10.1007\/978-3-319-66263-3_19"},{"key":"9560_CR46","doi-asserted-by":"crossref","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Polynomial-time validation of QCDCL certificates. In: Beyersdorff and Wintersteiger [14], pp. 253\u2013269","DOI":"10.1007\/978-3-319-94144-8_16"},{"key":"9560_CR47","doi-asserted-by":"crossref","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Proof complexity of fragments of long-distance Q-resolution. In: Janota and Lynce [33], pp. 319\u2013335","DOI":"10.1007\/978-3-030-24258-9_23"},{"key":"9560_CR48","unstructured":"QBFEVAL homepage: http:\/\/www.qbflib.org\/index_eval.php. Accessed 26 Oct 2018"},{"key":"9560_CR49","doi-asserted-by":"crossref","unstructured":"Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: Kaivola, R., Wahl, T. (eds.) Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 136\u2013143. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"9560_CR50","doi-asserted-by":"crossref","unstructured":"Rabe, M.N.: A resolution-style proof system for DQBF. In: Gaspers and Walsh [28], pp. 314\u2013325","DOI":"10.1007\/978-3-319-66263-3_20"},{"key":"9560_CR51","doi-asserted-by":"crossref","unstructured":"Samulowitz, H., Davies, J., Bacchus, F.: Preprocessing QBF. In: Benhamou, F. (ed.) International Conference on Principles and Practice of Constraint Programming (CP), Volume 4204 of Lecture Notes in Computer Science, pp. 514\u2013529. Springer (2006)","DOI":"10.1007\/11889205_37"},{"key":"9560_CR52","doi-asserted-by":"crossref","unstructured":"Scholl, C., Wimmer, R.: Dependency quantified Boolean formulas: an overview of solution methods and applications\u2014extended abstract. In: Beyersdorff and Wintersteiger [14], pp. 3\u201316","DOI":"10.1007\/978-3-319-94144-8_1"},{"key":"9560_CR53","unstructured":"Silva, J.P.M., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Volume 185 of Frontiers in Artificial Intelligence and Applications, pp. 131\u2013153. IOS Press (2009)"},{"key":"9560_CR54","doi-asserted-by":"crossref","unstructured":"Suda, M., Gleiss, B.: Local soundness for QBF calculi. In: Beyersdorff and Wintersteiger [14], pp. 217\u2013234","DOI":"10.1007\/978-3-319-94144-8_14"},{"key":"9560_CR55","doi-asserted-by":"crossref","unstructured":"Tentrup, L., Rabe, M.N.: Clausal abstraction for DQBF. In: Janota and Lynce [33], pp. 388\u2013405","DOI":"10.1007\/978-3-030-24258-9_27"},{"issue":"3","key":"9560_CR56","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/2578043","volume":"57","author":"MY Vardi","year":"2014","unstructured":"Vardi, M.Y.: Boolean satisfiability: theory and engineering. Commun. ACM 57(3), 5 (2014)","journal-title":"Commun. ACM"},{"key":"9560_CR57","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Gitina, K., Nist, J., Scholl, C., Becker, B.: Preprocessing for DQBF. In: Heule, M., Weaver, S. (eds.) International Conference on Theory and Practice of Satisfiability Testing (SAT), Volume 9340 of Lecture Notes in Computer Science, pp. 173\u2013190. Springer (2015)","DOI":"10.1007\/978-3-319-24318-4_13"},{"key":"9560_CR58","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Reimer, S., Marin, P., Becker, B.: HQSpre\u2014an effective preprocessor for QBF and DQBF. In: Legay and Margaria [39], pp. 373\u2013390","DOI":"10.1007\/978-3-662-54577-5_21"},{"key":"9560_CR59","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: International Conference on Computer-Aided Design (ICCAD), pp. 442\u2013449 (2002)","DOI":"10.1145\/774572.774637"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09560-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09560-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09560-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,24]],"date-time":"2022-10-24T17:04:40Z","timestamp":1666631080000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09560-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5,22]]},"references-count":59,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,1]]}},"alternative-id":["9560"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09560-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2020,5,22]]},"assertion":[{"value":"18 September 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 April 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 May 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}