{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T00:27:47Z","timestamp":1725668867501},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T00:00:00Z","timestamp":1721779200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T00:00:00Z","timestamp":1721779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Institute of Mathematical Sciences"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,9]]},"abstract":"Abstract<\/jats:title>In Quantified Boolean Formulas QBFs, dependency schemes help to detect spurious or superfluous dependencies that are implied by the variable ordering in the quantifier prefix but are not essential for constructing countermodels. This detection can provably shorten refutations in specific proof systems, and is expected to speed up runs of QBF solvers. The proof system $$\\texttt{QCDCL}$$<\/jats:tex-math>\n QCDCL<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u00a0recently defined by Beyersdorff and Boehm (LMCS 2023) abstracts the reasoning employed by QBF solvers based on conflict-driven clause-learning (CDCL) techniques. We show how to incorporate the use of dependency schemes into this proof system, either in a preprocessing phase, or in the propagations and clause learning, or both. We then show that when the reflexive resolution path dependency scheme $$\\texttt{D}^{\\texttt{rrs}}$$<\/jats:tex-math>\n \n D<\/mml:mi>\n rrs<\/mml:mi>\n <\/mml:msup>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> is used, a mixed picture emerges: the proof systems that add $$\\texttt{D}^{\\texttt{rrs}}$$<\/jats:tex-math>\n \n D<\/mml:mi>\n rrs<\/mml:mi>\n <\/mml:msup>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> to $$\\texttt{QCDCL}$$<\/jats:tex-math>\n QCDCL<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u00a0in these three ways are not only incomparable with each other, but are also incomparable with the basic $$\\texttt{QCDCL}$$<\/jats:tex-math>\n QCDCL<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u00a0proof system that does not use $$\\texttt{D}^{\\texttt{rrs}}$$<\/jats:tex-math>\n \n D<\/mml:mi>\n rrs<\/mml:mi>\n <\/mml:msup>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> at all, as well as with several other resolution-based QBF proof systems. A notable fact is that all our separations are achieved through QBFs with bounded quantifier alternation.<\/jats:p>","DOI":"10.1007\/s10817-024-09707-4","type":"journal-article","created":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T17:01:45Z","timestamp":1721840505000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Dependency Schemes in CDCL-Based QBF Solving: A Proof-Theoretic Study"],"prefix":"10.1007","volume":"68","author":[{"given":"Abhimanyu","family":"Choudhury","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meena","family":"Mahajan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,24]]},"reference":[{"key":"9707_CR1","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1613\/jair.3152","volume":"40","author":"A Atserias","year":"2011","unstructured":"Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res. 40, 353\u2013373 (2011). https:\/\/doi.org\/10.1613\/jair.3152","journal-title":"J. Artif. Intell. Res."},{"key":"9707_CR2","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."},{"issue":"2","key":"9707_CR3","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/3355995","volume":"21","author":"O Beyersdorff","year":"2020","unstructured":"Beyersdorff, O., Blinkhorn, J.: Dynamic QBF dependencies in reduction and expansion. ACM Trans. Comput. Log. 21(2), 8:1-8:27 (2020). https:\/\/doi.org\/10.1145\/3355995","journal-title":"ACM Trans. Comput. Log."},{"key":"9707_CR4","doi-asserted-by":"publisher","unstructured":"Beyersdorff, O., B\u00f6hm, B.: Understanding the relative strength of QBF CDCL solvers and QBF resolution. Log. Methods Comput. Sci. (2023). https:\/\/doi.org\/10.46298\/lmcs-19(2:2)2023. (Preliminary version in ITCS\u201921)","DOI":"10.46298\/lmcs-19(2:2)2023"},{"key":"9707_CR5","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-15(1:13)2019","author":"O Beyersdorff","year":"2019","unstructured":"Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost, and capacity: a semantic technique for hard random QBFs. Log. Methods Comput. Sci. (2019). https:\/\/doi.org\/10.23638\/LMCS-15(1:13)2019","journal-title":"Log. Methods Comput. Sci."},{"issue":"4","key":"9707_CR6","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-26:42 (2019). https:\/\/doi.org\/10.1145\/3352155","journal-title":"ACM Trans. Comput. Theory"},{"key":"9707_CR7","doi-asserted-by":"publisher","unstructured":"Beyersdorff, O., Blinkhorn, J., Peitl, T.: Strong (D)QBF dependency schemes via tautology-free resolution paths. In: Pulina, L., Seidl, M. (eds.) Theory and Applications of Satisfiability Testing\u2014SAT 2020\u201423rd International Conference, Alghero, Italy, July 3\u201310, 2020, Proceedings, Lecture Notes in Computer Science, vol. 12178, pp. 394\u2013411. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_28","DOI":"10.1007\/978-3-030-51825-7_28"},{"key":"9707_CR8","unstructured":"Beyersdorff, O., Blinkhorn, J., Peitl, T.: Strong (D)QBF dependency schemes via implication-free resolution paths. Electron. Colloquium Comput. Complex TR21-135 (2021). https:\/\/eccc.weizmann.ac.il\/report\/2021\/135, arXiv:TR21-135"},{"key":"9707_CR9","doi-asserted-by":"publisher","unstructured":"Beyersdorff, O., Janota, M., Lonsing, F., et\u00a0al.: Quantified Boolean formulas. In: Biere, A., Heule, M., van Maaren, H., et\u00a0al. (eds.) Handbook of Satisfiability\u2014Second Edition, Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 1177\u20131221. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA201015","DOI":"10.3233\/FAIA201015"},{"key":"9707_CR10","doi-asserted-by":"publisher","unstructured":"Blinkhorn, J., Beyersdorff, O.: Shortening QBF proofs with dependency schemes. In: Gaspers, S., Walsh, T. (eds.) Theory and Applications of Satisfiability Testing\u2014SAT 2017\u201420th International Conference, Melbourne, VIC, Australia, August 28\u2013September 1, 2017, Proceedings, Lecture Notes in Computer Science, vol. 10491, pp. 263\u2013280. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_17","DOI":"10.1007\/978-3-319-66263-3_17"},{"key":"9707_CR11","doi-asserted-by":"publisher","unstructured":"B\u00f6hm, B., Beyersdorff, O.: QCDCL vs QBF resolution: further insights. In: Mahajan, M., Slivovsky, F. (eds.) 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4\u20138, 2023, Alghero, Italy, LIPIcs, vol. 271, pp. 4:1\u20134:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2023.4","DOI":"10.4230\/LIPICS.SAT.2023.4"},{"key":"9707_CR12","doi-asserted-by":"publisher","unstructured":"B\u00f6hm, B., Peitl, T., Beyersdorff, O.: Should decisions in QCDCL follow prefix order? In: Meel, K.S., Strichman, O. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2\u20135, 2022, Haifa, Israel, LIPIcs, vol. 236, pp. 11:1\u201311:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2022.11","DOI":"10.4230\/LIPICS.SAT.2022.11"},{"key":"9707_CR13","doi-asserted-by":"publisher","unstructured":"B\u00f6hm, B., Peitl, T., Beyersdorff, O.: QCDCL with cube learning or pure literal elimination\u2014what is best? In: Raedt, L.D. (ed.) Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22. International Joint Conferences on Artificial Intelligence Organization, pp. 1781\u20131787 (2022). https:\/\/doi.org\/10.24963\/ijcai.2022\/248","DOI":"10.24963\/ijcai.2022\/248"},{"key":"9707_CR14","doi-asserted-by":"publisher","unstructured":"Choudhury, A., Mahajan, M.: Dependency schemes in CDCL-based QBF solving: a proof-theoretic study. In: Bouyer, P., Srinivasan, S. (eds.) 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2023, December 18\u201320, 2023, IIIT Hyderabad, Telangana, India, LIPIcs, vol. 284, pp. 38:1\u201338:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.FSTTCS.2023.38","DOI":"10.4230\/LIPICS.FSTTCS.2023.38"},{"key":"9707_CR15","unstructured":"Lonsing, F.: Dependency schemes and search-based QBF solving: theory and practice. PhD thesis, Johannes Kepler University, Linz, Austria (2012)"},{"issue":"2\u20133","key":"9707_CR16","doi-asserted-by":"publisher","first-page":"71","DOI":"10.3233\/sat190077","volume":"7","author":"F Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: A dependency-aware QBF solver. J. Satisf. Boolean Model. Comput. 7(2\u20133), 71\u201376 (2010). https:\/\/doi.org\/10.3233\/sat190077","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"9707_CR17","doi-asserted-by":"publisher","unstructured":"Lonsing, F., Biere, A.: Integrating dependency schemes in search-based QBF solvers. In: Strichman, O., Szeider, S. (eds.) Theory and Applications of Satisfiability Testing\u2014SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11\u201314, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6175, pp. 158\u2013171. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_14","DOI":"10.1007\/978-3-642-14186-7_14"},{"key":"9707_CR18","doi-asserted-by":"publisher","unstructured":"Lonsing, F., Egly, U.: DepQBF 6.0: A search-based QBF solver beyond traditional QCDCL. In: de Moura, L. (ed.) Automated Deduction\u2014CADE 26\u201426th International Conference on Automated Deduction, Gothenburg, Sweden, August 6\u201311, 2017, Proceedings, Lecture Notes in Computer Science, vol. 10395, pp. 371\u2013384. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_23","DOI":"10.1007\/978-3-319-63046-5_23"},{"key":"9707_CR19","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1613\/jair.1.11529","volume":"65","author":"T Peitl","year":"2019","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Dependency learning for QBF. J. Artif. Intell. Res. 65, 180\u2013208 (2019). https:\/\/doi.org\/10.1613\/jair.1.11529","journal-title":"J. Artif. Intell. Res."},{"issue":"1","key":"9707_CR20","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/s10817-018-9467-3","volume":"63","author":"T Peitl","year":"2019","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Long-distance Q-resolution with dependency schemes. J. Autom. Reason. 63(1), 127\u2013155 (2019). https:\/\/doi.org\/10.1007\/s10817-018-9467-3","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9707_CR21","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"K Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2), 512\u2013525 (2011). https:\/\/doi.org\/10.1016\/j.artint.2010.10.002","journal-title":"Artif. Intell."},{"issue":"1","key":"9707_CR22","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10817-008-9114-5","volume":"42","author":"M Samer","year":"2009","unstructured":"Samer, M., Szeider, S.: Backdoor sets of quantified Boolean formulas. J. Autom. Reason. 42(1), 77\u201397 (2009). https:\/\/doi.org\/10.1007\/s10817-008-9114-5","journal-title":"J. Autom. Reason."},{"key":"9707_CR23","first-page":"3","volume-title":"International Conference on Theory and Practice of Satisfiability Testing SAT, LNCS","author":"C Scholl","year":"2018","unstructured":"Scholl, C., Wimmer, R.: Dependency quantified Boolean formulas: an overview of solution methods and applications\u2014extended abstract. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) International Conference on Theory and Practice of Satisfiability Testing SAT, LNCS, vol. 10929, pp. 3\u201316. Springer, Berlin (2018)"},{"key":"9707_CR24","doi-asserted-by":"publisher","unstructured":"Shukla, A., Biere, A., Pulina, L., et\u00a0al.: A survey on applications of quantified Boolean formulas. In: 31st IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2019, Portland, OR, USA, November 4\u20136, 2019, pp. 78\u201384. IEEE (2019). https:\/\/doi.org\/10.1109\/ICTAI.2019.00020","DOI":"10.1109\/ICTAI.2019.00020"},{"key":"9707_CR25","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/j.tcs.2015.10.020","volume":"612","author":"F Slivovsky","year":"2016","unstructured":"Slivovsky, F., Szeider, S.: Soundness of Q-resolution with dependency schemes. Theor. Comput. Sci. 612, 83\u2013101 (2016). https:\/\/doi.org\/10.1016\/j.tcs.2015.10.020","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"9707_CR26","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\u2014underlying theory and its implementation. J. Satisf. Boolean Model. Comput. 11(1), 3\u201352 (2019). https:\/\/doi.org\/10.3233\/SAT190115","journal-title":"J. Satisf. Boolean Model. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09707-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09707-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09707-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T09:08:22Z","timestamp":1725613702000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09707-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,24]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,9]]}},"alternative-id":["9707"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09707-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2024,7,24]]},"assertion":[{"value":"22 January 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 July 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 July 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"16"}}