{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:02:32Z","timestamp":1750309352915,"version":"3.41.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2024,11,11]],"date-time":"2024-11-11T00:00:00Z","timestamp":1731283200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Austrian Science Fund","award":["J-4361N"],"award-info":[{"award-number":["J-4361N"]}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["BE 4209\/3-1"],"award-info":[{"award-number":["BE 4209\/3-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100007569","name":"Carl-Zeiss-Stiftung","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100007569","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Theory"],"published-print":{"date-parts":[[2024,12,31]]},"abstract":"<jats:p>\n            We suggest a general framework to study dependency schemes for dependency quantified Boolean formulas (DQBF). As our main contribution, we exhibit a new\n            <jats:italic>infinite collection<\/jats:italic>\n            of\n            <jats:italic>implication-free<\/jats:italic>\n            DQBF dependency schemes that generalise the reflexive resolution path dependency scheme. We establish soundness of all these schemes, implying that they can be used in any DQBF proof system. We further explore the power of QBF and DQBF resolution systems parameterised by implication-free dependency schemes and show that the hierarchical structure naturally present among the dependency schemes translates isomorphically to a hierarchical structure of parameterised proof systems with respect to p-simulation.\n          <\/jats:p>\n          <jats:p>As a special case, we demonstrate that our new schemes are exponentially stronger than the reflexive resolution path dependency scheme when used in Q-resolution, thus resulting in the strongest QBF dependency schemes known to date.<\/jats:p>","DOI":"10.1145\/3689345","type":"journal-article","created":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T16:10:12Z","timestamp":1725552612000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Strong (D)QBF Dependency Schemes via Implication-free Resolution Paths"],"prefix":"10.1145","volume":"16","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2870-1648","authenticated-orcid":false,"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[{"name":"Friedrich-Schiller-Universit\u00e4t, Jena, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7452-6521","authenticated-orcid":false,"given":"Joshua Lewis","family":"Blinkhorn","sequence":"additional","affiliation":[{"name":"Friedrich-Schiller-Universit\u00e4t, Jena Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7799-1568","authenticated-orcid":false,"given":"Tom\u00e1\u0161","family":"Peitl","sequence":"additional","affiliation":[{"name":"Institute of Logic and Computation, Technische Universitat Wien, Vienna Austria"}]}],"member":"320","published-online":{"date-parts":[[2024,11,11]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Salman Azhar Gary Peterson and John Reif. 2001. Lower bounds for multiplayer non-cooperative games of incomplete information. Journal of Computers and Mathematics with Applications 41 (2001) 957\u2013992.","key":"e_1_3_2_2_2","DOI":"10.1016\/S0898-1221(00)00333-3"},{"doi-asserted-by":"crossref","unstructured":"Valeriy Balabanov and Jie-Hong R. Jiang. 2012. Unified QBF certification and its applications. Formal Methods in System Design 41 1 (2012) 45\u201365.","key":"e_1_3_2_3_2","DOI":"10.1007\/s10703-012-0152-6"},{"doi-asserted-by":"publisher","key":"e_1_3_2_4_2","DOI":"10.1007\/978-3-319-09284-3_12"},{"key":"e_1_3_2_5_2","first-page":"353","volume-title":"Mathematics for Computation (M4C)","author":"Beyersdorff Olaf","year":"2022","unstructured":"Olaf Beyersdorff. 2022. Proof complexity of quantified Boolean logic \u2013 A survey. In Mathematics for Computation (M4C), Marco Benini, Olaf Beyersdorff, Michael Rathjen, and Peter Schuster (Eds.). World Scientific, 353\u2013391."},{"doi-asserted-by":"publisher","key":"e_1_3_2_6_2","DOI":"10.1007\/978-3-319-44953-1_7"},{"key":"e_1_3_2_7_2","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"12:1\u201312:15","volume-title":"International Symposium on Theoretical Aspects of Computer Science (STACS)","volume":"96","author":"Beyersdorff Olaf","year":"2018","unstructured":"Olaf Beyersdorff and Joshua Blinkhorn. 2018. Genuine lower bounds for QBF expansion. In International Symposium on Theoretical Aspects of Computer Science (STACS)(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 96), Rolf Niedermeier and Brigitte Vall\u00e9e (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Caen, 12:1\u201312:15."},{"doi-asserted-by":"crossref","unstructured":"Olaf Beyersdorff and Joshua Blinkhorn. 2019. Dynamic QBF dependencies in reduction and expansion. ACM Transactions on Computational Logic 21 2 (2019) 1\u201327.","key":"e_1_3_2_8_2","DOI":"10.1145\/3355995"},{"doi-asserted-by":"crossref","unstructured":"Olaf Beyersdorff Joshua Blinkhorn Leroy Chew Renate A. Schmidt and Martin Suda. 2019. Reinterpreting dependency schemes: Soundness meets incompleteness in DQBF. Journal of Automated Reasoning 63 3 (2019) 597\u2013623.","key":"e_1_3_2_9_2","DOI":"10.1007\/s10817-018-9482-4"},{"unstructured":"Olaf Beyersdorff Joshua Blinkhorn and Luke Hinde. 2019. Size cost and capacity: A semantic technique for hard random QBFs. Logical Methods in Computer Science 15 1 (2019).","key":"e_1_3_2_10_2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_11_2","DOI":"10.1007\/978-3-030-51825-7_28"},{"doi-asserted-by":"publisher","key":"e_1_3_2_12_2","DOI":"10.1145\/2840728.2840740"},{"doi-asserted-by":"crossref","unstructured":"Olaf Beyersdorff Leroy Chew and Mikol\u00e1s Janota. 2019. New resolution-based QBF calculi and their proof complexity. ACM Transactions on Computation Theory 11 4 (2019) 26:1\u201326:42.","key":"e_1_3_2_13_2","DOI":"10.1145\/3352155"},{"doi-asserted-by":"crossref","unstructured":"Olaf Beyersdorff Leroy Chew Renate A. Schmidt and Martin Suda. 2016. Lifting QBF resolution calculi to DQBF See Creignou and Berre [19] 490\u2013499.","key":"e_1_3_2_14_2","DOI":"10.1007\/978-3-319-40970-2_30"},{"doi-asserted-by":"crossref","unstructured":"Olaf Beyersdorff Luke Hinde and J\u00e1n Pich. 2020. Reasons for hardness in QBF proof systems. ACM Transactions on Computation Theory 12 2 (2020) 10:1\u201310:27.","key":"e_1_3_2_15_2","DOI":"10.1145\/3378665"},{"doi-asserted-by":"publisher","key":"e_1_3_2_16_2","DOI":"10.3233\/FAIA201015"},{"doi-asserted-by":"publisher","key":"e_1_3_2_17_2","DOI":"10.1007\/978-3-319-66263-3_17"},{"doi-asserted-by":"crossref","unstructured":"Hubie Chen. 2017. Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness. ACM Transactions on Computation Theory 9 3 (2017) 15:1\u201315:20.","key":"e_1_3_2_18_2","DOI":"10.1145\/3087534"},{"doi-asserted-by":"crossref","unstructured":"Stephen A. Cook and Robert A. Reckhow. 1979. The relative efficiency of propositional proof systems. Journal of Symbolic Logic 44 1 (1979) 36\u201350.","key":"e_1_3_2_19_2","DOI":"10.2307\/2273702"},{"doi-asserted-by":"publisher","key":"e_1_3_2_20_2","DOI":"10.1007\/978-3-319-40970-2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_21_2","DOI":"10.1007\/978-3-319-21275-3"},{"doi-asserted-by":"crossref","unstructured":"Martin Davis George Logemann and Donald W. Loveland. 1962. A machine program for theorem-proving. Commun. ACM 5 7 (1962) 394\u2013397.","key":"e_1_3_2_22_2","DOI":"10.1145\/368273.368557"},{"doi-asserted-by":"crossref","unstructured":"Martin Davis and Hilary Putnam. 1960. A computing procedure for quantification theory. Journal of the ACM 7 3 (1960) 201\u2013215.","key":"e_1_3_2_23_2","DOI":"10.1145\/321033.321034"},{"doi-asserted-by":"publisher","key":"e_1_3_2_24_2","DOI":"10.1007\/978-1-4471-5559-1"},{"doi-asserted-by":"crossref","unstructured":"Uwe Egly Martin Kronegger Florian Lonsing and Andreas Pfandler. 2017. Conformant planning as a case study of incremental QBF solving. Annals of Mathematics and Artificial Intelligence 80 1 (2017) 21\u201345.","key":"e_1_3_2_25_2","DOI":"10.1007\/s10472-016-9501-2"},{"unstructured":"L. Henkin. 1961. Some remarks on infinitely long formulas. Infinitistic Methods (1961) 167-183.","key":"e_1_3_2_26_2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_27_2","DOI":"10.1007\/978-3-319-98334-9"},{"doi-asserted-by":"crossref","unstructured":"Holger H. Hoos Tom\u00e1\u0161 Peitl Friedrich Slivovsky and Stefan Szeider. 2018. Portfolio-based algorithm selection for circuit QBFs see Hooker [26] 195\u2013209.","key":"e_1_3_2_28_2","DOI":"10.1007\/978-3-319-98334-9_13"},{"doi-asserted-by":"crossref","unstructured":"Mikol\u00e1s\u0306 Janota and Jo\u00e3o Marques-Silva. 2015. Expansion-based QBF solving versus Q-resolution. Theoretical Computer Science 577 (2015) 25\u201342.","key":"e_1_3_2_29_2","DOI":"10.1016\/j.tcs.2015.01.048"},{"doi-asserted-by":"crossref","unstructured":"Hans Kleine B\u00fcning Marek Karpinski and Andreas Fl\u00f6gel. 1995. Resolution for quantified Boolean formulas. Information and Computation 117 1 (1995) 12\u201318.","key":"e_1_3_2_30_2","DOI":"10.1006\/inco.1995.1025"},{"key":"e_1_3_2_31_2","first-page":"836","volume-title":"International Joint Conference on Artificial Intelligence (IJCAI)","author":"Kontchakov Roman","year":"2009","unstructured":"Roman Kontchakov, Luca Pulina, Ulrike Sattler, Thomas Schneider, Petra Selmer, Frank Wolter, and Michael Zakharyaschev. 2009. Minimal module extraction from DL-lite ontologies using QBF solvers. In International Joint Conference on Artificial Intelligence (IJCAI), Craig Boutilier (Ed.). AAAI Press, Pasadena, 836\u2013841."},{"doi-asserted-by":"publisher","key":"e_1_3_2_32_2","DOI":"10.1007\/978-3-319-63046-5_23"},{"doi-asserted-by":"crossref","unstructured":"Florian Lonsing and Uwe Egly. 2018. Evaluating QBF solvers: Quantifier alternations matter See Hooker [26] 276\u2013294.","key":"e_1_3_2_33_2","DOI":"10.1007\/978-3-319-98334-9_19"},{"doi-asserted-by":"crossref","unstructured":"Hratch Mangassarian Andreas G. Veneris and Marco Benedetti. 2010. Robust QBF encodings for sequential circuits with applications to verification debug and test. IEEE Trans. Comput. 59 7 (2010) 981\u2013994.","key":"e_1_3_2_34_2","DOI":"10.1109\/TC.2010.74"},{"doi-asserted-by":"publisher","key":"e_1_3_2_35_2","DOI":"10.1007\/978-3-030-24258-9_22"},{"doi-asserted-by":"crossref","unstructured":"Tom\u00e1\u0161 Peitl Friedrich Slivovsky and Stefan Szeider. 2019. Dependency learning for QBF. Journal of Artificial Intelligence Research 65 (2019) 181\u2013208.","key":"e_1_3_2_36_2","DOI":"10.1613\/jair.1.11529"},{"doi-asserted-by":"crossref","unstructured":"Tom\u00e1\u0161 Peitl Friedrich Slivovsky and Stefan Szeider. 2019. Long-distance Q-resolution with dependency schemes. Journal of Automated Reasoning 63 1 (2019) 127\u2013155.","key":"e_1_3_2_37_2","DOI":"10.1007\/s10817-018-9467-3"},{"doi-asserted-by":"crossref","unstructured":"Luca Pulina and Martina Seidl. 2019. The 2016 and 2017 QBF solvers evaluations (QBFEVAL\u201916 and QBFEVAL\u201917). Artif. Intell. 274 (2019) 224\u2013248.","key":"e_1_3_2_38_2","DOI":"10.1016\/j.artint.2019.04.002"},{"doi-asserted-by":"crossref","unstructured":"John Alan Robinson. 1965. A machine-oriented logic based on the resolution principle. Journal of the ACM 12 1 (1965) 23\u201341.","key":"e_1_3_2_39_2","DOI":"10.1145\/321250.321253"},{"doi-asserted-by":"crossref","unstructured":"Marko Samer and Stefan Szeider. 2009. Backdoor sets of quantified Boolean formulas. Journal of Automated Reasoning 42 1 (2009) 77\u201397.","key":"e_1_3_2_40_2","DOI":"10.1007\/s10817-008-9114-5"},{"doi-asserted-by":"publisher","key":"e_1_3_2_41_2","DOI":"10.1007\/978-3-319-94144-8_1"},{"key":"e_1_3_2_42_2","volume-title":"Structure in  \\(\\#\\) SAT and QBF","author":"Slivovsky Friedrich","year":"2015","unstructured":"Friedrich Slivovsky. 2015. Structure in \\(\\#\\) SAT and QBF. Ph. D. Dissertation. Vienna University of Technology."},{"doi-asserted-by":"crossref","unstructured":"Friedrich Slivovsky and Stefan Szeider. 2016. Soundness of q-resolution with dependency schemes. Theoretical Computer Science 612 (2016) 83\u2013101.","key":"e_1_3_2_43_2","DOI":"10.1016\/j.tcs.2015.10.020"},{"doi-asserted-by":"crossref","unstructured":"Moshe Y. Vardi. 2014. Boolean satisfiability: Theory and engineering. Commun. ACM 57 3 (2014) 5.","key":"e_1_3_2_44_2","DOI":"10.1145\/2578043"},{"doi-asserted-by":"crossref","unstructured":"Ralf Wimmer Christoph Scholl Karina Wimmer and Bernd Becker. 2016. Dependency schemes for DQBF see Creignou and Berre [19] 473\u2013489.","key":"e_1_3_2_45_2","DOI":"10.1007\/978-3-319-40970-2_29"}],"container-title":["ACM Transactions on Computation Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689345","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689345","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:05:45Z","timestamp":1750291545000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689345"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,11]]},"references-count":44,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,12,31]]}},"alternative-id":["10.1145\/3689345"],"URL":"https:\/\/doi.org\/10.1145\/3689345","relation":{},"ISSN":["1942-3454","1942-3462"],"issn-type":[{"type":"print","value":"1942-3454"},{"type":"electronic","value":"1942-3462"}],"subject":[],"published":{"date-parts":[[2024,11,11]]},"assertion":[{"value":"2021-07-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-15","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}