{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:27:10Z","timestamp":1750220830120,"version":"3.41.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2019,11,17]],"date-time":"2019-11-17T00:00:00Z","timestamp":1573948800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"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","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. Logic"],"published-print":{"date-parts":[[2020,4,30]]},"abstract":"<jats:p>We provide the first proof complexity results for QBF dependency calculi. By showing that the reflexive resolution path dependency scheme admits exponentially shorter Q-resolution proofs on a known family of instances, we answer a question first posed by Slivovsky and Szeider in 2014 [37]. Further, we conceive a method of QBF solving in which dependency recomputation is utilised as a form of inprocessing. Formalising this notion, we introduce a new version of Q-resolution in which a dependency scheme is applied dynamically. We demonstrate the further potential of this approach beyond that of the existing static system with an exponential separation. Last, we show that the same picture emerges in an analogous approach to the universal expansion paradigm.<\/jats:p>","DOI":"10.1145\/3355995","type":"journal-article","created":{"date-parts":[[2019,11,18]],"date-time":"2019-11-18T13:01:53Z","timestamp":1574082113000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Dynamic QBF Dependencies in Reduction and Expansion"],"prefix":"10.1145","volume":"21","author":[{"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","family":"Blinkhorn","sequence":"additional","affiliation":[{"name":"Friedrich-Schiller-Universit\u00e4t Jena, Germany"}]}],"member":"320","published-online":{"date-parts":[[2019,11,17]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_2_1_2_1","first-page":"1","article-title":"QBF-based formal verification: Experience and perspectives","volume":"5","author":"Benedetti Marco","year":"2008","journal-title":"J. Satisf., Boolean Model. Comput."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9482-4"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200710069"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-44953-1_7"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the International Symposium on Theoretical Aspects of Computer Science (STACS\u201918)","volume":"96","author":"Beyersdorff Olaf","year":"2018"},{"volume-title":"cost, and capacity: A semantic technique for hard random QBFs. Log. Meth. Comput. Sci. 15, 1","year":"2019","author":"Beyersdorff Olaf","key":"e_1_2_1_7_1"},{"volume-title":"Feasible interpolation for QBF resolution calculi. Log. Meth. Comput. Sci. 13, 2","year":"2017","author":"Beyersdorff Olaf","key":"e_1_2_1_8_1"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3157053"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2016.11.011"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66263-3_17"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.009"},{"volume-title":"Cook and Phuong Nguyen","year":"2010","author":"Stephen","key":"e_1_2_1_13_1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-016-9501-2"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_20"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23786-7_59"},{"volume-title":"Handbook of Satisfiability, Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications","author":"Giunchiglia Enrico","key":"e_1_2_1_18_1"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622559.1622569"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2016.01.004"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.01.048"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1025"},{"volume-title":"Propositional Logic, and Complexity Theory. Encyclopedia of Mathematics and Its Applications","author":"Kraj\u00ed\u010dek Jan","key":"e_1_2_1_23_1"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26287-1_14"},{"key":"e_1_2_1_26_1","first-page":"2","article-title":"DepQBF: A dependency-aware QBF solver","volume":"7","author":"Lonsing Florian","year":"2010","journal-title":"J. Sat., Boolean Model. Comput."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_27"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_31"},{"volume-title":"Proceedings of the National Conference on Artificial Intelligence (AAAI\u201907)","year":"2007","author":"Rintanen Jussi","key":"e_1_2_1_30_1"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9114-5"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/11564751_43"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/MTV.2003.1250266"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48159-1_5"},{"volume-title":"Proceedings of the International Conference on Computer-Aided Design (ICCAD\u201996)","author":"Jo\u00e3o","key":"e_1_2_1_35_1"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_21"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.10.020"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/774572.774637"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3355995","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3355995","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:13:30Z","timestamp":1750202010000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3355995"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,17]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,4,30]]}},"alternative-id":["10.1145\/3355995"],"URL":"https:\/\/doi.org\/10.1145\/3355995","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2019,11,17]]},"assertion":[{"value":"2019-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-11-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}