{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T14:21:49Z","timestamp":1790691709384,"version":"4.1.0"},"reference-count":91,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2015,8,17]],"date-time":"2015-08-17T00:00:00Z","timestamp":1439769600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM SIGLOG News"],"published-print":{"date-parts":[[2015,8,17]]},"abstract":"<jats:p>This paper is intended as an informal and accessible survey of proof complexity for non-experts, focusing on some comparatively weak proof systems of particular interest in connection with SAT solving. We review resolution, polynomial calculus, and cutting planes (related to conflict-driven clause learning, Gr\u00f6bner basis computations, and pseudo-Boolean solving, respectively) and some complexity measures that have been studied for these proof systems. We also discuss briefly to what extent proof complexity could provide insights into SAT solver performance, and how concerns related to applied SAT solving can give rise to interesting complexity-theoretic questions. Along the way, we highlight a number of current research challenges.<\/jats:p>","DOI":"10.1145\/2815493.2815497","type":"journal-article","created":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T01:17:49Z","timestamp":1585963069000},"page":"19-44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":54,"title":["On the interplay between proof complexity and SAT solving"],"prefix":"10.1145","volume":"2","author":[{"given":"Jakob","family":"Nordstr\u00f6m","sequence":"first","affiliation":[{"name":"KTH Royal Institute of Technology, Stockholm, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2015,8,17]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00395-5"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700366735"},{"key":"e_1_2_1_3_1","first-page":"18","article-title":"Lower Bounds for Polynomial Calculus: Non-Binomial Case","volume":"242","author":"Alekhnovich Michael","year":"2003","journal-title":"Proceedings of the Steklov Institute of Mathematics"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1137\/06066850X"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 23rd National Conference on Artificial Intelligence (AAAI '08)","author":"Ans\u00f3tegui Carlos","year":"2008"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2007.06.025"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/2016945.2016955"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/CCC.2014.36"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 24th AAAI Conference on Artificial Intelligence, (AAAI '10)","author":"Audemard Gilles","year":"2010"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI '09)","author":"Audemard Gilles","year":"2009"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 14th National Conference on Artificial Intelligence (AAAI '97)","author":"Bayardo Roberto J."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2213977.2213999"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2005.05.004"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-007-0230-0"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622487.1622497"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2488608.2488711"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1137\/080723880"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.10089"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/795665.796522"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-010-0293-1"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00493-004-0036-5"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2008.42"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS '11)","author":"Ben-Sasson Eli","year":"2011"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2012.48"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_22"},{"key":"e_1_2_1_29_1","volume-title":"Frontiers in Artificial Intelligence and Applications","volume":"185","author":"Biere Armin","year":"2009"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699438"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2014.74"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539799352474"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370100000"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2008.02.017"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2008.11.043"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1726"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(4:13)2008"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2004.842808"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/48014.48016"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237860"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(87)90039-4"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the 18th National Conference on Artificial Intelligence (AAAI '02)","author":"Heidi"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622467.1622474"},{"key":"e_1_2_1_49_1","volume-title":"An Extensible SAT-solver. In 6th International Conference on Theory and Applications of Satisfiability Testing (SAT '03)","volume":"2919","author":"E\u00e9n Niklas","year":"2004"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190014"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2921"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39206-1_37"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2746339"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/CCC.2012.27"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1838552.1838556"},{"key":"e_1_2_1_56_1","volume-title":"Proceedings of the 30th Annual Computational Complexity Conference (CCC '15) (Leibniz International Proceedings in Informatics (LIPIcs))","volume":"33","author":"Galesi Nicola","year":"2015"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2591796.2591838"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_2_1_60_1","volume-title":"Proceedings of the 23rd National Conference on Artificial Intelligence (AAAI '08)","author":"Hertel Philipp","year":"2008"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/11527695_12"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2213977.2214000"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050024"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.5555\/2969951.2969981"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.5555\/4336.4338"},{"key":"e_1_2_1_67_1","volume-title":"Release 2.2. Journal on Satisfiability, Boolean Modeling and Computation 7","author":"Berre Daniel Le","year":"2010"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/322344.322354"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39611-3_14"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190024"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"e_1_2_1_72_1","volume-title":"Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT '14)","volume":"8561","author":"Mik\u0161a Mladen","year":"2014"},{"key":"e_1_2_1_73_1","volume-title":"Proceedings of the 30th Annual Computational Complexity Conference (CCC '15) (Leibniz International Proceedings in Informatics (LIPIcs))","volume":"33","author":"Mik\u0161a Mladen","year":"2015"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1137\/060668250"},{"key":"e_1_2_1_76_1","volume-title":"Article 15 (Sept.","author":"Nordstr\u00f6m Jakob","year":"2013"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_1"},{"key":"e_1_2_1_78_1","volume-title":"Article 14 (May","author":"Nordstr\u00f6m Jakob","year":"2013"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01683275"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2010.10.002"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275583"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/972639.972640"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1007\/s004930050062"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050013"},{"key":"e_1_2_1_85_1","volume-title":"Proof Complexity of Pigeonhole Principles. In 5th International Conference on Developments in Language Theory, (DLT '01)","volume":"2295","author":"Razborov Alexander A.","year":"2002"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00453-X"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2004.01.004"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1203350879"},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190020"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1007\/11753728_60"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1145\/1671970.1671972"},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050044"},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1145\/7531.8928"},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_37"}],"container-title":["ACM SIGLOG News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2815493.2815497","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2815493.2815497","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:43:13Z","timestamp":1750225393000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2815493.2815497"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,8,17]]},"references-count":91,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,8,17]]}},"alternative-id":["10.1145\/2815493.2815497"],"URL":"https:\/\/doi.org\/10.1145\/2815493.2815497","relation":{},"ISSN":["2372-3491"],"issn-type":[{"value":"2372-3491","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,8,17]]},"assertion":[{"value":"2015-08-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}