{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:33:57Z","timestamp":1740123237724,"version":"3.37.3"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T00:00:00Z","timestamp":1707436800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T00:00:00Z","timestamp":1707436800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100012957","name":"Friedrich-Schiller-Universit\u00e4t Jena","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100012957","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":[[2024,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Quantified conflict-driven clause learning (QCDCL) is one of the main solving approaches for quantified Boolean formulas (QBF). One of the differences between QCDCL and propositional CDCL is that QCDCL typically follows the prefix order of the QBF for making decisions. We investigate an alternative model for QCDCL solving where decisions can be made in arbitrary order. The resulting system<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{QCDCL}^\\textsf {{A\\tiny {\\MakeUppercase {ny}}}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mi>QCDCL<\/mml:mi><mml:mrow><mml:mi>A<\/mml:mi><mml:mi>NY<\/mml:mi><\/mml:mrow><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>is still sound and terminating, but does not necessarily allow to always learn asserting clauses or cubes. To address this potential drawback, we additionally introduce two subsystems that guarantee to always learn asserting clauses (<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{QCDCL}^\\textsf {{U\\tiny {\\MakeUppercase {ni}}-A\\tiny {\\MakeUppercase {ny}}}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mi>QCDCL<\/mml:mi><mml:mrow><mml:mi>U<\/mml:mi><mml:mi>NI<\/mml:mi><mml:mo>-<\/mml:mo><mml:mi>A<\/mml:mi><mml:mi>NY<\/mml:mi><\/mml:mrow><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>) and asserting cubes (<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{QCDCL}^\\textsf {{E\\tiny {\\MakeUppercase {xi}}-A\\tiny {\\MakeUppercase {ny}}}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mi>QCDCL<\/mml:mi><mml:mrow><mml:mi>E<\/mml:mi><mml:mi>XI<\/mml:mi><mml:mo>-<\/mml:mo><mml:mi>A<\/mml:mi><mml:mi>NY<\/mml:mi><\/mml:mrow><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>), respectively. We model all four approaches by formal proof systems and show that<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{QCDCL}^\\textsf {{U\\tiny {\\MakeUppercase {ni}}-A\\tiny {\\MakeUppercase {ny}}}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mi>QCDCL<\/mml:mi><mml:mrow><mml:mi>U<\/mml:mi><mml:mi>NI<\/mml:mi><mml:mo>-<\/mml:mo><mml:mi>A<\/mml:mi><mml:mi>NY<\/mml:mi><\/mml:mrow><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>is exponentially better than<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf{{QCDCL}} $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>QCDCL<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>on false formulas, whereas<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{QCDCL}^\\textsf {{E\\tiny {\\MakeUppercase {xi}}-A\\tiny {\\MakeUppercase {ny}}}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mi>QCDCL<\/mml:mi><mml:mrow><mml:mi>E<\/mml:mi><mml:mi>XI<\/mml:mi><mml:mo>-<\/mml:mo><mml:mi>A<\/mml:mi><mml:mi>NY<\/mml:mi><\/mml:mrow><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>is exponentially better than<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf{{QCDCL}} $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>QCDCL<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>on true QBFs. Technically, this involves constructing specific QBF families and showing lower and upper bounds in the respective proof systems. We complement our theoretical study with some initial experiments that confirm our theoretical findings.<\/jats:p>","DOI":"10.1007\/s10817-024-09694-6","type":"journal-article","created":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T13:02:20Z","timestamp":1707483740000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Should Decisions in QCDCL Follow Prefix Order?"],"prefix":"10.1007","volume":"68","author":[{"given":"Benjamin","family":"B\u00f6hm","sequence":"first","affiliation":[]},{"given":"Tom\u00e1\u0161","family":"Peitl","sequence":"additional","affiliation":[]},{"given":"Olaf","family":"Beyersdorff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,2,9]]},"reference":[{"key":"9694_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)","journal-title":"J. Artif. Intell. Res."},{"issue":"1","key":"9694_CR2","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":"9694_CR3","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P Beame","year":"2004","unstructured":"Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. 22, 319\u2013351 (2004)","journal-title":"J. Artif. Intell. Res."},{"key":"9694_CR4","unstructured":"Beyersdorff, O., B\u00f6hm, B.: QCDCL with cube learning or pure literal elimination\u2014what is best? Electron. Colloquium Comput. Complex. 131 (2021)"},{"key":"9694_CR5","unstructured":"Beyersdorff, O., B\u00f6hm, B.: Understanding the relative strength of QBF CDCL solvers and QBF resolution. In: Proceedings of Innovations in Theoretical Computer Science (ITCS), pp. 12\u201311220 (2021)"},{"issue":"1","key":"9694_CR6","first-page":"13","volume":"15","author":"O Beyersdorff","year":"2019","unstructured":"Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost, and capacity: a semantic technique for hard random QBFs. Logical Methods Comput. Sci. 15(1), 13 (2019)","journal-title":"Logical Methods Comput. Sci."},{"key":"9694_CR7","first-page":"1177","volume-title":"Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications","author":"O Beyersdorff","year":"2021","unstructured":"Beyersdorff, O., Janota, M., Lonsing, F., Seidl, M.: Quantified Boolean formulas. In: Biere, A., Heule, M., Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, pp. 1177\u20131221. IOS Press, Amsterdam (2021)"},{"key":"9694_CR8","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). LIPIcs, Vol. 236, pp. 11\u201311119. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"9694_CR9","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-030-80223-3_5","volume-title":"Theory and Applications of Satisfiability Testing\u2014SAT 2021","author":"B B\u00f6hm","year":"2021","unstructured":"B\u00f6hm, B., Beyersdorff, O.: Lower bounds for QCDCL via formula gauge. In: Li, C.-M., Many\u00e0, F. (eds.) Theory and Applications of Satisfiability Testing\u2014SAT 2021, pp. 47\u201363. Springer, Cham (2021)"},{"key":"9694_CR10","first-page":"233","volume-title":"Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications","author":"S Buss","year":"2021","unstructured":"Buss, S., Nordstr\u00f6m, J.: Proof complexity and SAT solving. In: Biere, A., Heule, M., Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, pp. 233\u2013350. IOS Press, Amsterdam (2021)"},{"key":"9694_CR11","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified Boolean formulae. In: Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference (AAAI), pp. 262\u2013267 (1998)"},{"issue":"1","key":"9694_CR12","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. Logic 44(1), 36\u201350 (1979)","journal-title":"J. Symb. Logic"},{"key":"9694_CR13","first-page":"761","volume-title":"Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications","author":"E Giunchiglia","year":"2009","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with quantified Boolean formulas. In: Biere, A., Heule, M., Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 761\u2013780. IOS Press, Amsterdam (2009)"},{"key":"9694_CR14","first-page":"635","volume-title":"Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications","author":"M Heule","year":"2021","unstructured":"Heule, M.: Proofs of unsatisfiability. In: Biere, A., Heule, M., Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, 2nd edn., pp. 635\u2013668. IOS Press, Amsterdam (2021)","edition":"2"},{"issue":"1","key":"9694_CR15","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10817-016-9390-4","volume":"58","author":"MJH Heule","year":"2017","unstructured":"Heule, M.J.H., Seidl, M., Biere, A.: Solution validation and extraction for QBF preprocessing. J. Autom. Reason. 58(1), 97\u2013125 (2017)","journal-title":"J. Autom. Reason."},{"key":"9694_CR16","doi-asserted-by":"publisher","unstructured":"Hoos, H.H., Peitl, T., Slivovsky, F., Szeider, S.: Portfolio-based algorithm selection for circuit qbfs. In: Hooker, J.N. (ed.) Principles and Practice of Constraint Programming - 24th International Conference, CP 2018, Lille, France, August 27-31, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11008, pp. 195\u2013209. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-98334-9_13","DOI":"10.1007\/978-3-319-98334-9_13"},{"key":"9694_CR17","doi-asserted-by":"crossref","unstructured":"Janota, M.: On Q-Resolution and CDCL QBF solving. In: Proceedings of International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 402\u2013418 (2016)","DOI":"10.1007\/978-3-319-40970-2_25"},{"key":"9694_CR18","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."},{"key":"9694_CR19","doi-asserted-by":"publisher","first-page":"670","DOI":"10.1007\/978-3-319-65340-2_55","volume-title":"Progress in Artificial Intelligence","author":"M Janota","year":"2017","unstructured":"Janota, M., Marques-Silva, J.: An Achilles\u2019 heel of term-resolution. In: Oliveira, E., Gama, J., Vale, Z., Lopes Cardoso, H. (eds.) Progress in Artificial Intelligence, pp. 670\u2013680. Springer, Cham (2017)"},{"issue":"1","key":"9694_CR20","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":"9694_CR21","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Egly, U.: DepQBF 6.0: A search-based QBF solver beyond traditional QCDCL. In: Proceedings of International Conference on Automated Deduction (CADE), pp. 371\u2013384 (2017)","DOI":"10.1007\/978-3-319-63046-5_23"},{"key":"9694_CR22","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Egly, U.: Evaluating QBF solvers: Quantifier alternations matter. In: Proceedings of Principles and Practice of Constraint Programming (CP), pp. 276\u2013294. Springer (2018)","DOI":"10.1007\/978-3-319-98334-9_19"},{"key":"9694_CR23","unstructured":"Lonsing, F.: Dependency schemes and search-based QBF solving: Theory and practice. PhD thesis, Johannes Kepler University Linz (2012)"},{"key":"9694_CR24","doi-asserted-by":"crossref","unstructured":"Marques Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications. IOS Press (2021)","DOI":"10.3233\/FAIA200987"},{"key":"9694_CR25","doi-asserted-by":"crossref","unstructured":"Marques Silva, J.P., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: Proceedings of IEEE\/ACM International Conference on Computer-aided Design (ICCAD), pp. 220\u2013227 (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"9694_CR26","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient sat solver. In: Proceedings of the 38th Design Automation Conference (IEEE Cat. No.01CH37232), pp. 530\u2013535 (2001). 11.1145\/378239.379017","DOI":"10.1145\/378239.379017"},{"key":"9694_CR27","doi-asserted-by":"publisher","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Combining resolution-path dependencies with dependency learning. In: Janota, M., Lynce, I. (eds.) Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11628, pp. 306\u2013318. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_22","DOI":"10.1007\/978-3-030-24258-9_22"},{"issue":"1","key":"9694_CR28","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)","journal-title":"J. Autom. Reason."},{"key":"9694_CR29","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)","journal-title":"J. Artif. Intell. Res."},{"issue":"2","key":"9694_CR30","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)","journal-title":"Artif. Intell."},{"issue":"1","key":"9694_CR31","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":"9694_CR32","doi-asserted-by":"crossref","unstructured":"Shukla, A., Biere, A., Pulina, L., Seidl, M.: A survey on applications of quantified Boolean formulas. In: Proceedings of IEEE International Conference on Tools with Artificial Intelligence (ICTAI), pp. 78\u201384 (2019)","DOI":"10.1109\/ICTAI.2019.00020"},{"key":"9694_CR33","doi-asserted-by":"publisher","unstructured":"Slivovsky, F., Peitl, T., Perebor, Heisinger, M.: Fslivovsky\/qute: Out-of-order Decisions. https:\/\/doi.org\/10.5281\/zenodo.10149885","DOI":"10.5281\/zenodo.10149885"},{"key":"9694_CR34","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)","journal-title":"Theor. Comput. Sci."},{"key":"9694_CR35","unstructured":"Tange, O.: GNU Parallel - The command-line power tool. login: The USENIX Magazine February, 42\u201347 (2011)"},{"key":"9694_CR36","doi-asserted-by":"crossref","unstructured":"Vinyals, M.: Hard examples for common variable decision heuristics. In: Proceedings of the AAAI Conference on Artificial Intelligence (AAAI) (2020)","DOI":"10.1609\/aaai.v34i02.5527"},{"key":"9694_CR37","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in Boolean satisfiability solver. In: Proceedings of IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), pp. 279\u2013285 (2001)","DOI":"10.1145\/774572.774637"},{"key":"9694_CR38","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: Proceedings of IEEE\/ACM 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-024-09694-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09694-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09694-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,10]],"date-time":"2024-11-10T23:07:41Z","timestamp":1731280061000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09694-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,2,9]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,3]]}},"alternative-id":["9694"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09694-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2024,2,9]]},"assertion":[{"value":"8 July 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 January 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 February 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"5"}}