{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:09:40Z","timestamp":1750219780851,"version":"3.41.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2023,1,27]],"date-time":"2023-01-27T00:00:00Z","timestamp":1674777600000},"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 JTF","doi-asserted-by":"crossref","award":["60842 JTF60842"],"award-info":[{"award-number":["60842 JTF60842"]}],"id":[{"id":"10.13039\/100000925","id-type":"DOI","asserted-by":"crossref"}]},{"name":"DFG","award":["BE 4209\/3-1"],"award-info":[{"award-number":["BE 4209\/3-1"]}]},{"name":"Austrian Science Fund FWF FWF","award":["J-4361"],"award-info":[{"award-number":["J-4361"]}]},{"name":"Carl Zeiss Foundation CZF"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2023,4,30]]},"abstract":"<jats:p>\n            We provide a\n            <jats:italic>tight characterisation of proof size in resolution for quantified Boolean formulas (QBF) via circuit complexity.<\/jats:italic>\n            Such a characterisation was previously obtained for a hierarchy of QBF Frege systems\u00a0[\n            <jats:xref ref-type=\"bibr\">16<\/jats:xref>\n            ], but leaving open the most important case of QBF resolution. Different from the Frege case, our characterisation uses a new version of decision lists as its circuit model, which is stronger than the CNFs the system works with. Our decision list model is well suited to compute countermodels for QBFs. Our characterisation works for both\n            <jats:italic>Q-Resolution and QU-Resolution.<\/jats:italic>\n          <\/jats:p>\n          <jats:p>\n            Using our characterisation, we obtain a\n            <jats:italic>size-width relation for QBF resolution<\/jats:italic>\n            in the spirit of the celebrated result for propositional resolution\u00a0[\n            <jats:xref ref-type=\"bibr\">4<\/jats:xref>\n            ]. However, our result is not just a replication of the propositional relation\u2014intriguingly ruled out for QBF in previous research\u00a0[\n            <jats:xref ref-type=\"bibr\">12<\/jats:xref>\n            ]\u2014but shows a different dependence between size, width, and quantifier complexity. An essential ingredient is an improved relation between the size and width of term decision lists; this may be of independent interest.\n          <\/jats:p>\n          <jats:p>\n            We demonstrate that\n            <jats:italic>our new technique elegantly reproves known QBF hardness results<\/jats:italic>\n            and unifies previous lower-bound techniques in the QBF domain.\n          <\/jats:p>","DOI":"10.1145\/3565286","type":"journal-article","created":{"date-parts":[[2022,9,28]],"date-time":"2022-09-28T11:47:37Z","timestamp":1664365657000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Hardness Characterisations and Size-width Lower Bounds for QBF Resolution"],"prefix":"10.1145","volume":"24","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[{"name":"Friedrich-Schiller-Universit\u00e4t Jena, Germany"}]},{"given":"Joshua","family":"Blinkhorn","sequence":"additional","affiliation":[{"name":"Friedrich-Schiller-Universit\u00e4t Jena, Germany"}]},{"given":"Meena","family":"Mahajan","sequence":"additional","affiliation":[{"name":"The Institute of Mathematical Sciences, HBNI, Chennai, India"}]},{"given":"Tom\u00e1\u0161","family":"Peitl","sequence":"additional","affiliation":[{"name":"TU Wienm, Vienna, Austria"}]}],"member":"320","published-online":{"date-parts":[[2023,1,27]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1016\/j.tcs.2013.12.020","article-title":"Henkin quantifiers and Boolean formulae: A certification perspective of DQBF","volume":"523","author":"Balabanov Valeriy","year":"2014","unstructured":"Valeriy Balabanov, Hui-Ju Katherine Chiang, and Jie-Hong R. Jiang. 2014. Henkin quantifiers and Boolean formulae: A certification perspective of DQBF. Theoret. Comput. Sci. 523 (2014), 86\u2013100.","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"e_1_3_2_3_2","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","article-title":"Unified QBF certification and its applications","volume":"41","author":"Balabanov Valeriy","year":"2012","unstructured":"Valeriy Balabanov and Jie-Hong R. Jiang. 2012. Unified QBF certification and its applications. Form. Meth. Syst. Des. 41, 1 (2012), 45\u201365.","journal-title":"Form. Meth. Syst. Des."},{"key":"e_1_3_2_4_2","first-page":"42","volume-title":"Current Trends in Theoretical Computer Science: Entering the 21st Century","author":"Beame Paul","year":"2001","unstructured":"Paul Beame and Toniann Pitassi. 2001. Propositional proof complexity: Past, present, and future. In Current Trends in Theoretical Computer Science: Entering the 21st Century, G. Paun, G. Rozenberg, and A. Salomaa (Eds.). World Scientific Publishing, UK, 42\u201370."},{"issue":"2","key":"e_1_3_2_5_2","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1145\/375827.375835","article-title":"Short proofs are narrow\u2014Resolution made simple","volume":"48","author":"Ben-Sasson Eli","year":"2001","unstructured":"Eli Ben-Sasson and Avi Wigderson. 2001. Short proofs are narrow\u2014Resolution made simple. J. ACM 48, 2 (2001), 149\u2013169.","journal-title":"J. ACM"},{"issue":"2","key":"e_1_3_2_6_2","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1002\/malq.200710069","article-title":"On the correspondence between arithmetic theories and propositional proof systems\u2014A survey","volume":"55","author":"Beyersdorff Olaf","year":"2009","unstructured":"Olaf Beyersdorff. 2009. On the correspondence between arithmetic theories and propositional proof systems\u2014A survey. Math. Logic Quart. 55, 2 (2009), 116\u2013137.","journal-title":"Math. Logic Quart."},{"issue":"1","key":"e_1_3_2_7_2","article-title":"Size, cost, and capacity: A semantic technique for hard random QBFs","volume":"15","author":"Beyersdorff Olaf","year":"2019","unstructured":"Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. 2019. Size, cost, and capacity: A semantic technique for hard random QBFs. Logic. Meth. Comput. Sci. 15, 1 (2019).","journal-title":"Logic. Meth. Comput. Sci."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394793"},{"key":"e_1_3_2_9_2","first-page":"249","volume-title":"ACM Conference on Innovations in Theoretical Computer Science (ITCS)","author":"Beyersdorff Olaf","year":"2016","unstructured":"Olaf Beyersdorff, Ilario Bonacina, and Leroy Chew. 2016. Lower bounds: From circuits to QBF proof systems. In ACM Conference on Innovations in Theoretical Computer Science (ITCS). ACM, New York, NY, 249\u2013260."},{"key":"e_1_3_2_10_2","first-page":"76","volume-title":"International Symposium on Theoretical Aspects of Computer Science (STACS) (Leibniz International Proceedings in Informatics (LIPIcs))","volume":"30","author":"Beyersdorff Olaf","year":"2015","unstructured":"Olaf Beyersdorff, Leroy Chew, and Mikol\u00e1s\u0306 Janota. 2015. Proof complexity of resolution-based QBF Calculi. In International Symposium on Theoretical Aspects of Computer Science (STACS) (Leibniz International Proceedings in Informatics (LIPIcs)), Vol. 30. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 76\u201389."},{"issue":"4","key":"e_1_3_2_11_2","first-page":"26:1\u201326:42","article-title":"New resolution-based QBF Calculi and their proof complexity","volume":"11","author":"Beyersdorff Olaf","year":"2019","unstructured":"Olaf Beyersdorff, Leroy Chew, and Mikol\u00e1s Janota. 2019. New resolution-based QBF Calculi and their proof complexity. ACM Trans. Computat. Theor. 11, 4 (2019), 26:1\u201326:42.","journal-title":"ACM Trans. Computat. Theor."},{"key":"e_1_3_2_12_2","article-title":"Feasible interpolation for QBF resolution Calculi","volume":"13","author":"Beyersdorff Olaf","year":"2017","unstructured":"Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. 2017. Feasible interpolation for QBF resolution Calculi. Logic. Meth. Comput. Sci. 13, 2 (2017).","journal-title":"Logic. Meth. Comput. Sci."},{"issue":"1","key":"e_1_3_2_13_2","first-page":"1:1\u20131:26","article-title":"Are short proofs narrow? QBF resolution is not so simple.","volume":"19","author":"Beyersdorff Olaf","year":"2018","unstructured":"Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. 2018. Are short proofs narrow? QBF resolution is not so simple. ACM Trans. Computat. Logic 19, 1 (2018), 1:1\u20131:26.","journal-title":"ACM Trans. Computat. Logic"},{"key":"e_1_3_2_14_2","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1016\/j.jcss.2016.11.011","article-title":"A game characterisation of tree-like Q-Resolution size","volume":"104","author":"Beyersdorff Olaf","year":"2019","unstructured":"Olaf Beyersdorff, Leroy Chew, and Karteek Sreenivasaiah. 2019. A game characterisation of tree-like Q-Resolution size. J. Comput. Syst. Sci. 104 (2019), 82\u2013101.","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"e_1_3_2_15_2","first-page":"10:1\u201310:27","article-title":"Reasons for hardness in QBF proof systems","volume":"12","author":"Beyersdorff Olaf","year":"2020","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.","journal-title":"ACM Transactions on Computation Theory"},{"issue":"3","key":"e_1_3_2_16_2","doi-asserted-by":"crossref","first-page":"320","DOI":"10.1016\/j.ic.2010.11.006","article-title":"Proof systems that take advice","volume":"209","author":"Beyersdorff Olaf","year":"2011","unstructured":"Olaf Beyersdorff, Johannes K\u00f6bler, and Sebastian M\u00fcller. 2011. Proof systems that take advice. Inf. Computat. 209, 3 (2011), 320\u2013332.","journal-title":"Inf. Computat."},{"key":"e_1_3_2_17_2","first-page":"146","volume-title":"Symposium on Logic in Computer Science (LICS)","author":"Beyersdorff Olaf","year":"2016","unstructured":"Olaf Beyersdorff and J\u00e1n Pich. 2016. Understanding Gentzen and Frege systems for QBF. In Symposium on Logic in Computer Science (LICS). ACM, New York, NY, 146\u2013155."},{"key":"e_1_3_2_18_2","volume-title":"Canonical Expressions in Boolean Algebra","author":"Blake A.","year":"1937","unstructured":"A. Blake. 1937. Canonical Expressions in Boolean Algebra. Ph.D. Dissertation. University of Chicago."},{"issue":"1","key":"e_1_3_2_19_2","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/0020-0190(96)00077-4","article-title":"A subexponential exact learning algorithm for DNF using equivalence queries","volume":"59","author":"Bshouty Nader H.","year":"1996","unstructured":"Nader H. Bshouty. 1996. A subexponential exact learning algorithm for DNF using equivalence queries. Inform. Process. Lett. 59, 1 (1996), 37\u201339.","journal-title":"Inform. Process. Lett."},{"issue":"7","key":"e_1_3_2_20_2","doi-asserted-by":"crossref","first-page":"906","DOI":"10.1016\/j.apal.2011.09.009","article-title":"Towards NP-P via proof complexity and search","volume":"163","author":"Buss Samuel R.","year":"2012","unstructured":"Samuel R. Buss. 2012. Towards NP-P via proof complexity and search. Ann. Pure Appl. Logic 163, 7 (2012), 906\u2013917.","journal-title":"Ann. Pure Appl. Logic"},{"issue":"3","key":"e_1_3_2_21_2","first-page":"15:1\u201315:20","article-title":"Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness","volume":"9","author":"Chen Hubie","year":"2017","unstructured":"Hubie Chen. 2017. Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness. ACM Trans. Computat. Theor. 9, 3 (2017), 15:1\u201315:20.","journal-title":"ACM Trans. Computat. Theor."},{"key":"e_1_3_2_22_2","volume-title":"Proof Complexity for Quantified Boolean Formulas","author":"Clymo Judith","year":"2021","unstructured":"Judith Clymo. 2021. Proof Complexity for Quantified Boolean Formulas. Ph.D. Dissertation. School of Computing, University of Leeds."},{"key":"e_1_3_2_23_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.ipl.2018.05.005","article-title":"Relating size and width in variants of Q-resolution","volume":"138","author":"Clymo Judith","year":"2018","unstructured":"Judith Clymo and Olaf Beyersdorff. 2018. Relating size and width in variants of Q-resolution. Inf. Process. Lett. 138 (2018), 1\u20136.","journal-title":"Inf. Process. Lett."},{"key":"e_1_3_2_24_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511676277","volume-title":"Logical Foundations of Proof Complexity","author":"Cook Stephen A.","year":"2010","unstructured":"Stephen A. Cook and Phuong Nguyen. 2010. Logical Foundations of Proof Complexity. Cambridge University Press, Cambridge, UK."},{"issue":"1","key":"e_1_3_2_25_2","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","article-title":"The relative efficiency of propositional proof systems","volume":"44","author":"Cook Stephen A.","year":"1979","unstructured":"Stephen A. Cook and Robert A. Reckhow. 1979. The relative efficiency of propositional proof systems. J. Symbol. Logic 44, 1 (1979), 36\u201350.","journal-title":"J. Symbol. Logic"},{"key":"e_1_3_2_26_2","unstructured":"(Lecture Notes in Computer Science International Conference on Theory and Practice of Satisfiability Testing (SAT) 9710) Nadia Creignou Daniel Le Berre 2016"},{"issue":"1","key":"e_1_3_2_27_2","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/s10472-016-9501-2","article-title":"Conformant planning as a case study of incremental QBF solving","volume":"80","author":"Egly Uwe","year":"2017","unstructured":"Uwe Egly, Martin Kronegger, Florian Lonsing, and Andreas Pfandler. 2017. Conformant planning as a case study of incremental QBF solving. Ann. Math. Artif. Intell. 80, 1 (2017), 21\u201345.","journal-title":"Ann. Math. Artif. Intell."},{"key":"e_1_3_2_28_2","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1007\/978-3-642-33558-7_47","volume-title":"International Conference on Principles and Practice of Constraint Programming (CP) (Lecture Notes in Computer Science)","volume":"7514","author":"Gelder Allen Van","year":"2012","unstructured":"Allen Van Gelder. 2012. Contributions to the theory of practical quantified Boolean formula solving. In International Conference on Principles and Practice of Constraint Programming (CP) (Lecture Notes in Computer Science), Vol. 7514. Springer, New York, NY, 647\u2013663."},{"issue":"6","key":"e_1_3_2_29_2","first-page":"37:1\u201337:59","article-title":"Circuit complexity, proof complexity, and polynomial identity testing: The ideal proof system","volume":"65","author":"Grochow Joshua A.","year":"2018","unstructured":"Joshua A. Grochow and Toniann Pitassi. 2018. Circuit complexity, proof complexity, and polynomial identity testing: The ideal proof system. J. ACM 65, 6 (2018), 37:1\u201337:59.","journal-title":"J. ACM"},{"key":"e_1_3_2_30_2","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","article-title":"The intractability of resolution","volume":"39","author":"Haken Armin","year":"1985","unstructured":"Armin Haken. 1985. The intractability of resolution. Theoret. Comput. Sci. 39 (1985), 297\u2013308.","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_3_2_31_2","volume-title":"Computational Limitations of Small Depth Circuits","author":"H\u00e5stad J.","year":"1987","unstructured":"J. H\u00e5stad. 1987. Computational Limitations of Small Depth Circuits. MIT Press, Cambridge, MA."},{"key":"e_1_3_2_32_2","doi-asserted-by":"crossref","unstructured":"Mikol\u00e1s Janota. 2016. On Q-resolution and CDCL QBF solving. In International Conference on Theory and Practice of Satisfiability Testing (SAT). 402\u2013418.","DOI":"10.1007\/978-3-319-40970-2_25"},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/j.tcs.2015.01.048","article-title":"Expansion-based QBF solving versus Q-resolution","volume":"577","author":"Janota Mikol\u00e1s\u0306","year":"2015","unstructured":"Mikol\u00e1s\u0306 Janota and Jo\u00e3o Marques-Silva. 2015. Expansion-based QBF solving versus Q-resolution. Theoret. Comput. Sci. 577 (2015), 25\u201342.","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"e_1_3_2_34_2","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1006\/inco.1995.1025","article-title":"Resolution for quantified Boolean formulas","volume":"117","author":"B\u00fcning Hans Kleine","year":"1995","unstructured":"Hans Kleine B\u00fcning, Marek Karpinski, and Andreas Fl\u00f6gel. 1995. Resolution for quantified Boolean formulas. Inf. Computat. 117, 1 (1995), 12\u201318.","journal-title":"Inf. Computat."},{"key":"e_1_3_2_35_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). AAAI Press, 836\u2013841."},{"key":"e_1_3_2_36_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511529948","volume-title":"Bounded Arithmetic, Propositional Logic, and Complexity Theory","author":"Kraj\u00ed\u010dek Jan","year":"1995","unstructured":"Jan Kraj\u00ed\u010dek. 1995. Bounded Arithmetic, Propositional Logic, and Complexity Theory(Encyclopedia of Mathematics and Its Applications, Vol. 60). Cambridge University Press, Cambridge, UK."},{"issue":"4","key":"e_1_3_2_37_2","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1007\/s00037-005-0203-0","article-title":"On the computational power of Boolean decision lists","volume":"14","author":"Krause Matthias","year":"2006","unstructured":"Matthias Krause. 2006. On the computational power of Boolean decision lists. Computat. Complex. 14, 4 (2006), 362\u2013375.","journal-title":"Computat. Complex."},{"key":"e_1_3_2_38_2","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1007\/978-3-319-98334-9_19","volume-title":"International Conference on Principles and Practice of Constraint Programming (CP) (Lecture Notes in Computer Science)","volume":"11008","author":"Lonsing Florian","year":"2018","unstructured":"Florian Lonsing and Uwe Egly. 2018. Evaluating QBF solvers: Quantifier alternations matter. In International Conference on Principles and Practice of Constraint Programming (CP) (Lecture Notes in Computer Science), Vol. 11008. Springer, New York, NY, 276\u2013294."},{"key":"e_1_3_2_39_2","first-page":"100","volume-title":"International Conference on Theory and Applications of Satisfiability Testing (SAT) (Lecture Notes in Computer Science)","volume":"7962","author":"Lonsing Florian","year":"2013","unstructured":"Florian Lonsing, Uwe Egly, and Allen Van Gelder. 2013. Efficient clause learning for quantified Boolean formulas via QBF pseudo unit propagation. In International Conference on Theory and Applications of Satisfiability Testing (SAT) (Lecture Notes in Computer Science), Vol. 7962. Springer, New York, NY, 100\u2013115."},{"key":"e_1_3_2_40_2","doi-asserted-by":"crossref","unstructured":"Florian Lonsing Uwe Egly and Martina Seidl. 2016. Q-resolution with generalized axioms. In International Conference on Theory and Practice of Satisfiability Testing (SAT). 435\u2013452.","DOI":"10.1007\/978-3-319-40970-2_27"},{"issue":"7","key":"e_1_3_2_41_2","doi-asserted-by":"crossref","first-page":"981","DOI":"10.1109\/TC.2010.74","article-title":"Robust QBF encodings for sequential circuits with applications to verification, debug, and test","volume":"59","author":"Mangassarian Hratch","year":"2010","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.","journal-title":"IEEE Trans. Comput."},{"issue":"3","key":"e_1_3_2_42_2","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1145\/2815493.2815497","article-title":"On the interplay between proof complexity and SAT solving","volume":"2","author":"Nordstr\u00f6m Jakob","year":"2015","unstructured":"Jakob Nordstr\u00f6m. 2015. On the interplay between proof complexity and SAT solving. SIGLOG News 2, 3 (2015), 19\u201344.","journal-title":"SIGLOG News"},{"key":"e_1_3_2_43_2","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1016\/j.artint.2019.04.002","article-title":"The 2016 and 2017 QBF solvers evaluations (QBFEVAL\u201916 and QBFEVAL\u201917)","volume":"274","author":"Pulina Luca","year":"2019","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.","journal-title":"Artif. Intell."},{"issue":"4","key":"e_1_3_2_44_2","first-page":"333","article-title":"Lower bounds for the size of circuits of bounded depth with basis  \\(\\lbrace \\wedge ,\\oplus \\rbrace\\)","volume":"41","author":"Razborov A. A.","year":"1987","unstructured":"A. A. Razborov. 1987. Lower bounds for the size of circuits of bounded depth with basis \\(\\lbrace \\wedge ,\\oplus \\rbrace\\) . Math. Notes Acad. Sci. USSR 41, 4 (1987), 333\u2013338.","journal-title":"Math. Notes Acad. Sci. USSR"},{"issue":"3","key":"e_1_3_2_45_2","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/BF00058680","article-title":"Learning decision lists","volume":"2","author":"Rivest Ronald L.","year":"1987","unstructured":"Ronald L. Rivest. 1987. Learning decision lists. Mach. Learn. 2, 3 (1987), 229\u2013246.","journal-title":"Mach. Learn."},{"issue":"1","key":"e_1_3_2_46_2","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson John Alan","year":"1965","unstructured":"John Alan Robinson. 1965. A machine-oriented logic based on the resolution principle. J. ACM 12, 1 (1965), 23\u201341.","journal-title":"J. ACM"},{"issue":"4","key":"e_1_3_2_47_2","doi-asserted-by":"crossref","first-page":"417","DOI":"10.2178\/bsl\/1203350879","article-title":"The complexity of propositional proofs","volume":"13","author":"Segerlind Nathan","year":"2007","unstructured":"Nathan Segerlind. 2007. The complexity of propositional proofs. Bull. Symbol. Logic 13, 4 (2007), 417\u2013481.","journal-title":"Bull. Symbol. Logic"},{"key":"e_1_3_2_48_2","first-page":"77","volume-title":"19th ACM Symposium on Theory of Computing","author":"Smolensky R.","year":"1987","unstructured":"R. Smolensky. 1987. Algebraic methods in the theory of lower bounds for Boolean circuit complexity. In 19th ACM Symposium on Theory of Computing. ACM Press, New York, NY, 77\u201382."},{"key":"e_1_3_2_49_2","volume-title":"First-order Logic","author":"Smullyan Raymond M.","year":"1995","unstructured":"Raymond M. Smullyan. 1995. First-order Logic. Dover Publications, Dover, DE."},{"issue":"3","key":"e_1_3_2_50_2","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1145\/2578043","article-title":"Boolean satisfiability: Theory and engineering","volume":"57","author":"Vardi Moshe Y.","year":"2014","unstructured":"Moshe Y. Vardi. 2014. Boolean satisfiability: Theory and engineering. Commun. ACM 57, 3 (2014), 5.","journal-title":"Commun. ACM"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3565286","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3565286","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:43Z","timestamp":1750178263000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3565286"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,27]]},"references-count":49,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,4,30]]}},"alternative-id":["10.1145\/3565286"],"URL":"https:\/\/doi.org\/10.1145\/3565286","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2023,1,27]]},"assertion":[{"value":"2020-10-05","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-08-28","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-01-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}