{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:58:48Z","timestamp":1781078328164,"version":"3.54.1"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2024,11,8]],"date-time":"2024-11-08T00:00:00Z","timestamp":1731024000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"European Union\u2019s Seventh Framework Programme","award":["FP7\/2007\u20132013"],"award-info":[{"award-number":["FP7\/2007\u20132013"]}]},{"name":"ERC","award":["279611"],"award-info":[{"award-number":["279611"]}]},{"name":"Knut and Alice Wallenberg","award":["KAW 2016.0066"],"award-info":[{"award-number":["KAW 2016.0066"]}]},{"DOI":"10.13039\/501100004359","name":"Swedish Research Council","doi-asserted-by":"crossref","award":["621-2010-4797, 621-2012-5645, and 2016-00782"],"award-info":[{"award-number":["621-2010-4797, 621-2012-5645, and 2016-00782"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Independent Research Fund Denmark","award":["9040-00389B"],"award-info":[{"award-number":["9040-00389B"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2024,12,31]]},"abstract":"<jats:p>\n            We study the problem of obtaining lower bounds for polynomial calculus (PC) and polynomial calculus resolution (PCR) on proof degree, and hence by [Impagliazzo et\u00a0al. \u00a0\u201999] also on proof size. [Alekhnovich and Razborov\u201903] established that if the clause-variable incidence graph of a conjunctive normal form (CNF) formula\u00a0\n            <jats:italic>F<\/jats:italic>\n            is a good enough expander, then proving that\u00a0\n            <jats:italic>F<\/jats:italic>\n            is unsatisfiable requires high PC\/PCR degree. We further develop their techniques to show that if one can \u201ccluster\u201d clauses and variables in a way that \u201crespects the structure\u201d of the formula in a certain sense, then it is sufficient that the incidence graph of this clustered version is an expander. We also show how a weaker structural condition is sufficient to obtain lower bounds on width for the resolution proof system, and give a unified treatment that highlights similarities and differences between resolution and polynomial calculus (PC) lower bounds.\n          <\/jats:p>\n          <jats:p>As a corollary of our main technical theorem, we prove that the functional pigeonhole principle (FPHP) formulas require high PC\/PCR degree when restricted to constant-degree expander graphs. This answers an open question in [Razborov\u201902], and also implies that the standard CNF encoding of the FPHP formulas require exponential proof size in polynomial calculus resolution (PCR). Thus, while onto-FPHP formulas are easy for polynomial calculus, as shown in [Riis\u201993], both FPHP and onto-PHP formulas are hard even when restricted to bounded-degree expanders.<\/jats:p>","DOI":"10.1145\/3675668","type":"journal-article","created":{"date-parts":[[2024,7,4]],"date-time":"2024-07-04T11:10:32Z","timestamp":1720091432000},"page":"1-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds"],"prefix":"10.1145","volume":"71","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5422-4267","authenticated-orcid":false,"given":"Mladen","family":"Mik\u0161a","sequence":"first","affiliation":[{"name":"School of Computer Science and Communication, KTH Royal Institute of Technology, Stockholm, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2700-4285","authenticated-orcid":false,"given":"Jakob","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Copenhagen, Copenhagen Denmark and Department of Computer Science, Lund University, Lund, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,11,8]]},"reference":[{"issue":"4","key":"e_1_3_3_2_2","doi-asserted-by":"crossref","first-page":"1184","DOI":"10.1137\/S0097539700366735","article-title":"Space complexity in propositional calculus","volume":"31","author":"Alekhnovich Michael","year":"2002","unstructured":"Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. 2002. Space complexity in propositional calculus. SIAM Journal on Computing 31, 4 (April2002), 1184\u20131211. Preliminary version in STOC\u201900.","journal-title":"SIAM Journal on Computing"},{"key":"e_1_3_3_3_2","first-page":"18","article-title":"Lower bounds for polynomial calculus: Non-binomial case","volume":"242","author":"Alekhnovich Michael","year":"2003","unstructured":"Michael Alekhnovich and Alexander A. Razborov. 2003. Lower bounds for polynomial calculus: Non-binomial case. Proceedings of the Steklov Institute of Mathematics 242 (2003), 18\u201335. Available at http:\/\/people.cs.uchicago.edu\/razborov\/files\/misha.pdf. Preliminary version in FOCS\u201901.","journal-title":"Proceedings of the Steklov Institute of Mathematics"},{"issue":"3","key":"e_1_3_3_4_2","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/j.jcss.2007.06.025","article-title":"A combinatorial characterization of resolution width","volume":"74","author":"Atserias Albert","year":"2008","unstructured":"Albert Atserias and V\u00edctor Dalmau. 2008. A combinatorial characterization of resolution width. Journal of Computer and System Sciences 74, 3 (May2008), 323\u2013334. Preliminary version in CCC\u201903.","journal-title":"Journal of Computer and System Sciences"},{"key":"e_1_3_3_5_2","first-page":"1:1\u20131:46","article-title":"Proof complexity meets algebra","volume":"20","author":"Atserias Albert","year":"2019","unstructured":"Albert Atserias and Joanna Ochremiak. 2019. Proof complexity meets algebra. ACM Transactions on Computational Logic 20, 1 (Feb.2019), 1:1\u20131:46. Preliminary version in ICALP\u201917.","journal-title":"ACM Transactions on Computational Logic"},{"issue":"1","key":"e_1_3_3_6_2","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/j.dam.2005.05.004","article-title":"The resolution complexity of random graph k-colorability","volume":"153","author":"Beame Paul","year":"2005","unstructured":"Paul Beame, Joseph C. Culberson, David G. Mitchell, and Cristopher Moore. 2005. The resolution complexity of random graph k-colorability. Discrete Applied Mathematics 153, 1-3 (Dec.2005), 25\u201347.","journal-title":"Discrete Applied Mathematics"},{"issue":"3","key":"e_1_3_3_7_2","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/s00037-007-0230-0","article-title":"The resolution complexity of independent sets and vertex covers in random graphs","volume":"16","author":"Beame Paul","year":"2007","unstructured":"Paul Beame, Russell Impagliazzo, and Ashish Sabharwal. 2007. The resolution complexity of independent sets and vertex covers in random graphs. Computational Complexity 16, 3 (Oct.2007), 245\u2013297. Preliminary version in CCC\u201901.","journal-title":"Computational Complexity"},{"key":"e_1_3_3_8_2","series-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1090\/dimacs\/039\/02","volume-title":"Proceedings of the Proof Complexity and Feasible Arithmetics","volume":"39","author":"Beame Paul","year":"1998","unstructured":"Paul Beame and S\u00f8ren Riis. 1998. More on the relative strength of counting principles. In Proceedings of the Proof Complexity and Feasible Arithmetics(DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 39). American Mathematical Society, 13\u201335. Available at https:\/\/homes.cs.washington.edu\/beame\/papers\/riis.pdf"},{"issue":"4","key":"e_1_3_3_9_2","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1007\/s00037-010-0293-1","article-title":"Random CNF\u2019s are hard for the polynomial calculus","volume":"19","author":"Ben-Sasson Eli","year":"2010","unstructured":"Eli Ben-Sasson and Russell Impagliazzo. 2010. Random CNF\u2019s are hard for the polynomial calculus. Computational Complexity 19, 4 (2010), 501\u2013519. Preliminary version in FOCS\u201999.","journal-title":"Computational Complexity"},{"issue":"2","key":"e_1_3_3_10_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. Journal of the ACM 48, 2 (March2001), 149\u2013169. Preliminary version in STOC\u201999.","journal-title":"Journal of the ACM"},{"key":"e_1_3_3_11_2","series-title":"Frontiers in Artificial Intelligence and Applications","doi-asserted-by":"crossref","DOI":"10.3233\/FAIA336","volume-title":"Handbook of Satisfiability (2nd ed.)","author":"Biere Armin","year":"2021","unstructured":"Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh (Eds.). 2021. Handbook of Satisfiability (2nd ed.). Frontiers in Artificial Intelligence and Applications, Vol. 336. IOS Press."},{"key":"e_1_3_3_12_2","volume-title":"Canonical Expressions in Boolean Algebra","author":"Blake Archie","year":"1937","unstructured":"Archie Blake. 1937. Canonical Expressions in Boolean Algebra. Ph. D. Dissertation. University of Chicago."},{"issue":"2","key":"e_1_3_3_13_2","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1006\/jcss.2000.1726","article-title":"Linear gaps between degrees for the polynomial calculus modulo distinct primes","volume":"62","author":"Buss Samuel R.","year":"2001","unstructured":"Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. 2001. Linear gaps between degrees for the polynomial calculus modulo distinct primes. Journal of Computer and System Sciences 62, 2 (March2001), 267\u2013289. Preliminary version in CCC\u201999.","journal-title":"Journal of Computer and System Sciences"},{"key":"e_1_3_3_14_2","unstructured":"Samuel R. Buss and Jakob Nordstr\u00f6m. 2021. Proof complexity and SAT solving. See Biere et\u00a0al. [10] Chapter 7 233\u2013350 IOS Press Ebooks."},{"issue":"4","key":"e_1_3_3_15_2","first-page":"26","article-title":"On the proof complexity of paris-harrington and off-diagonal ramsey tautologies","volume":"17","author":"Carlucci Lorenzo","year":"2016","unstructured":"Lorenzo Carlucci, Nicola Galesi, and Massimo Lauria. 2016. On the proof complexity of paris-harrington and off-diagonal ramsey tautologies. ACM Transactions on Computational Logic 17, 4 (Nov.2016), Article 26, 26:1\u201326:25 pages.","journal-title":"ACM Transactions on Computational Logic"},{"issue":"4","key":"e_1_3_3_16_2","doi-asserted-by":"crossref","first-page":"759","DOI":"10.1145\/48014.48016","article-title":"Many hard examples for resolution","volume":"35","author":"Chv\u00e1tal Va\u0161ek","year":"1988","unstructured":"Va\u0161ek Chv\u00e1tal and Endre Szemer\u00e9di. 1988. Many hard examples for resolution. Journal of the ACM 35, 4 (Oct.1988), 759\u2013768.","journal-title":"Journal of the ACM"},{"key":"e_1_3_3_17_2","first-page":"174","volume-title":"Proceedings of the 28th Annual ACM Symposium on Theory of Computing","author":"Clegg Matthew","year":"1996","unstructured":"Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. 1996. Using the groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the 28th Annual ACM Symposium on Theory of Computing. 174\u2013183."},{"key":"e_1_3_3_18_2","first-page":"1","volume-title":"Proceedings of the 64th Annual IEEE Symposium on Foundations of Computer Science","author":"Conneryd Jonas","year":"2023","unstructured":"Jonas Conneryd, Susanna F. de Rezende, Jakob Nordstr\u00f6m, Shuo Pang, and Kilian Risse. 2023. Graph colouring is hard on average for polynomial calculus and nullstellensatz. In Proceedings of the 64th Annual IEEE Symposium on Foundations of Computer Science. 1\u201311."},{"issue":"1","key":"e_1_3_3_19_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. Journal of Symbolic Logic 44, 1 (March1979), 36\u201350. Preliminary version in STOC\u201974.","journal-title":"Journal of Symbolic Logic"},{"key":"e_1_3_3_20_2","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"28:1\u201328:24","volume-title":"Proceedings of the 35th Annual Computational Complexity Conference (CCC\u201920)","volume":"169","author":"Rezende Susanna F. de","year":"2020","unstructured":"Susanna F. de Rezende, Jakob Nordstr\u00f6m, Kilian Risse, and Dmitry Sokolov. 2020. Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs. In Proceedings of the 35th Annual Computational Complexity Conference (CCC\u201920)(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 169). 28:1\u201328:24."},{"key":"e_1_3_3_21_2","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1016\/j.tcs.2019.09.023","article-title":"Another look at degree lower bounds for polynomial calculus","volume":"796","author":"Filmus Yuval","year":"2019","unstructured":"Yuval Filmus. 2019. Another look at degree lower bounds for polynomial calculus. Theoretical Computer Science 796 (Dec.2019), 286\u2013293.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"e_1_3_3_22_2","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/s00224-009-9195-5","article-title":"On the automatizability of polynomial calculus","volume":"47","author":"Galesi Nicola","year":"2010","unstructured":"Nicola Galesi and Massimo Lauria. 2010. On the automatizability of polynomial calculus. Theory of Computing Systems 47, 2 (Aug.2010), 491\u2013506.","journal-title":"Theory of Computing Systems"},{"issue":"1","key":"e_1_3_3_23_2","first-page":"4","article-title":"Optimality of size-degree trade-offs for polynomial calculus","volume":"12","author":"Galesi Nicola","year":"2010","unstructured":"Nicola Galesi and Massimo Lauria. 2010. Optimality of size-degree trade-offs for polynomial calculus. ACM Transactions on Computational Logic 12, 1 (Nov.2010), Article 4, 4:1\u20134:22 pages.","journal-title":"ACM Transactions on Computational Logic"},{"issue":"1","key":"e_1_3_3_24_2","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/PL00001599","article-title":"A complex-number fourier technique for lower bounds on the mod-m degree","volume":"9","author":"Green Frederic","year":"2000","unstructured":"Frederic Green. 2000. A complex-number fourier technique for lower bounds on the mod-m degree. Computational Complexity 9, 1 (Jan.2000), 16\u201338.","journal-title":"Computational Complexity"},{"key":"e_1_3_3_25_2","first-page":"648","volume-title":"Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science","author":"Grigoriev Dima","year":"1998","unstructured":"Dima Grigoriev. 1998. Tseitin\u2019s tautologies and lower bounds for nullstellensatz proofs. In Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science. 648\u2013652."},{"issue":"2","key":"e_1_3_3_26_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. Theoretical Computer Science 39, 2-3 (Aug.1985), 297\u2013308.","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"e_1_3_3_27_2","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1090\/S0273-0979-06-01126-8","article-title":"Expander graphs and their applications","volume":"43","author":"Hoory Shlomo","year":"2006","unstructured":"Shlomo Hoory, Nathan Linial, and Avi Wigderson. 2006. Expander graphs and their applications. Bulletin of the American Mathematical Society 43, 4 (Oct.2006), 439\u2013561.","journal-title":"Bulletin of the American Mathematical Society"},{"issue":"2","key":"e_1_3_3_28_2","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/s000370050024","article-title":"Lower bounds for the polynomial calculus and the gr\u00f6bner basis algorithm","volume":"8","author":"Impagliazzo Russell","year":"1999","unstructured":"Russell Impagliazzo, Pavel Pudl\u00e1k, and Ji\u0159\u00ed Sgall. 1999. Lower bounds for the polynomial calculus and the gr\u00f6bner basis algorithm. Computational Complexity 8, 2 (1999), 127\u2013144.","journal-title":"Computational Complexity"},{"issue":"3","key":"e_1_3_3_29_2","doi-asserted-by":"crossref","first-page":"229","DOI":"10.3233\/FI-2016-1358","article-title":"Tight lower bounds on the resolution complexity of perfect matching principles","volume":"145","author":"Itsykson Dmitry","year":"2016","unstructured":"Dmitry Itsykson, Vsevolod Oparin, Mikhail Slabodkin, and Dmitry Sokolov. 2016. Tight lower bounds on the resolution complexity of perfect matching principles. Fundamenta Informaticae 145, 3 (Aug.2016), 229\u2013242. Preliminary version in CSR\u201915.","journal-title":"Fundamenta Informaticae"},{"key":"e_1_3_3_30_2","doi-asserted-by":"crossref","unstructured":"Hans Kleine B\u00fcning and Oliver Kullmann. 2021. Minimal unsatisfiability and autarkies. See Biere et\u00a0al. [10] Chapter 14 571\u2013633.","DOI":"10.3233\/FAIA200997"},{"key":"e_1_3_3_31_2","series-title":"Encyclopedia of Mathematics and Its Applications","doi-asserted-by":"crossref","DOI":"10.1017\/9781108242066","volume-title":"Proof Complexity","author":"Kraj\u00ed\u010dek Jan","year":"2019","unstructured":"Jan Kraj\u00ed\u010dek. 2019. Proof Complexity. Encyclopedia of Mathematics and Its Applications, Vol. 170. Cambridge University Press."},{"key":"e_1_3_3_32_2","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"2:1\u20132:20","volume-title":"Proceedings of the 32nd Annual Computational Complexity Conference","volume":"79","author":"Lauria Massimo","year":"2017","unstructured":"Massimo Lauria and Jakob Nordstr\u00f6m. 2017. Graph colouring is hard for algorithms based on hilbert\u2019s nullstellensatz and gr\u00f6bner bases. In Proceedings of the 32nd Annual Computational Complexity Conference(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 79). 2:1\u20132:20."},{"issue":"2","key":"e_1_3_3_33_2","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/s00493-015-3193-9","article-title":"The complexity of proving that a graph is ramsey","volume":"37","author":"Lauria Massimo","year":"2017","unstructured":"Massimo Lauria, Pavel Pudl\u00e1k, Vojt\u011bch R\u00f6dl, and Neil Thapen. 2017. The complexity of proving that a graph is ramsey. Combinatorica 37, 2 (April2017), 253\u2013268. Preliminary version in ICALP\u201913.","journal-title":"Combinatorica"},{"key":"e_1_3_3_34_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/978-3-319-09284-3_10","volume-title":"Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing .","volume":"8561","author":"Mik\u0161a Mladen","year":"2014","unstructured":"Mladen Mik\u0161a and Jakob Nordstr\u00f6m. 2014. Long proofs of (seemingly) simple formulas. In Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing .Lecture Notes in Computer Science, Vol. 8561). Springer, 121\u2013137."},{"key":"e_1_3_3_35_2","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"467","volume-title":"Proceedings of the 30th Annual Computational Complexity Conference","volume":"33","author":"Mik\u0161a Mladen","year":"2015","unstructured":"Mladen Mik\u0161a and Jakob Nordstr\u00f6m. 2015. A generalized method for proving polynomial calculus degree lower bounds. In Proceedings of the 30th Annual Computational Complexity Conference(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 33). 467\u2013487."},{"issue":"14","key":"e_1_3_3_36_2","doi-asserted-by":"crossref","first-page":"610","DOI":"10.1016\/j.ipl.2012.05.004","article-title":"A lower bound on the size of resolution proofs of the ramsey theorem","volume":"112","author":"Pudl\u00e1k Pavel","year":"2012","unstructured":"Pavel Pudl\u00e1k. 2012. A lower bound on the size of resolution proofs of the ramsey theorem. Information Processing Letters 112, 14\u201315 (Aug.2012), 610\u2013611.","journal-title":"Information Processing Letters"},{"issue":"2","key":"e_1_3_3_37_2","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1145\/972639.972640","article-title":"Resolution lower bounds for the weak pigeonhole principle","volume":"51","author":"Raz Ran","year":"2004","unstructured":"Ran Raz. 2004. Resolution lower bounds for the weak pigeonhole principle. Journal of the ACM 51, 2 (March2004), 115\u2013138. Preliminary version in STOC\u201902.","journal-title":"Journal of the ACM"},{"issue":"4","key":"e_1_3_3_38_2","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/s000370050013","article-title":"Lower bounds for the polynomial calculus","volume":"7","author":"Razborov Alexander A.","year":"1998","unstructured":"Alexander A. Razborov. 1998. Lower bounds for the polynomial calculus. Computational Complexity 7, 4 (Dec.1998), 291\u2013324.","journal-title":"Computational Complexity"},{"key":"e_1_3_3_39_2","volume-title":"Improved Resolution Lower Bounds for the Weak Pigeonhole Principle","author":"Razborov Alexander A.","year":"2001","unstructured":"Alexander A. Razborov. 2001. Improved Resolution Lower Bounds for the Weak Pigeonhole Principle. Technical Report TR01-055. Electronic Colloquium on Computational Complexity (ECCC)."},{"key":"e_1_3_3_40_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1007\/3-540-46011-X_8","volume-title":"Proceedings of the 5th International Conference on Developments in Language Theory, Revised Papers","volume":"2295","author":"Razborov Alexander A.","year":"2002","unstructured":"Alexander A. Razborov. 2002. Proof complexity of pigeonhole principles. In Proceedings of the 5th International Conference on Developments in Language Theory, Revised Papers(Lecture Notes in Computer Science, Vol. 2295). Springer, 100\u2013116."},{"issue":"303","key":"e_1_3_3_41_2","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1016\/S0304-3975(02)00453-X","article-title":"Resolution lower bounds for the weak functional pigeonhole principle","volume":"1","author":"Razborov Alexander A.","year":"2003","unstructured":"Alexander A. Razborov. 2003. Resolution lower bounds for the weak functional pigeonhole principle. Theoretical Computer Science 1, 303 (June2003), 233\u2013243.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"e_1_3_3_42_2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.jcss.2004.01.004","article-title":"Resolution lower bounds for perfect matching principles","volume":"69","author":"Razborov Alexander A.","year":"2004","unstructured":"Alexander A. Razborov. 2004. Resolution lower bounds for perfect matching principles. Journal of Computer and System Sciences 69, 1 (Aug.2004), 3\u201327. Preliminary version in CCC\u201902.","journal-title":"Journal of Computer and System Sciences"},{"key":"e_1_3_3_43_2","article-title":"Possible research directions","author":"Razborov Alexander A.","year":"2014","unstructured":"Alexander A. Razborov. 2014. Possible research directions. List of open problems (in proof complexity and other areas) available at http:\/\/people.cs.uchicago.edu\/razborov\/teaching\/","journal-title":"List of open problems (in proof complexity and other areas) available at http:\/\/people.cs.uchicago.edu\/razborov\/teaching\/"},{"key":"e_1_3_3_44_2","volume-title":"Independence in Bounded Arithmetic","author":"Riis S\u00f8ren","year":"1993","unstructured":"S\u00f8ren Riis. 1993. Independence in Bounded Arithmetic. Ph. D. Dissertation. University of Oxford."},{"key":"e_1_3_3_45_2","first-page":"1.2","article-title":"sgen1: A generator of small but difficult satisfiability benchmarks","volume":"15","author":"Spence Ivor","year":"2010","unstructured":"Ivor Spence. 2010. sgen1: A generator of small but difficult satisfiability benchmarks. Journal of Experimental Algorithmics 15 (March2010), Article 1.2, 1.2:1\u20131.2:15 pages.","journal-title":"Journal of Experimental Algorithmics"},{"issue":"3","key":"e_1_3_3_46_2","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/s002360050044","article-title":"Short resolution proofs for a sequence of tricky formulas","volume":"33","author":"St\u00e5lmarck Gunnar","year":"1996","unstructured":"Gunnar St\u00e5lmarck. 1996. Short resolution proofs for a sequence of tricky formulas. Acta Informatica 33, 3 (May1996), 277\u2013280.","journal-title":"Acta Informatica"},{"issue":"1","key":"e_1_3_3_47_2","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/7531.8928","article-title":"Hard examples for resolution","volume":"34","author":"Urquhart Alasdair","year":"1987","unstructured":"Alasdair Urquhart. 1987. Hard examples for resolution. Journal of the ACM 34, 1 (Jan.1987), 209\u2013219.","journal-title":"Journal of the ACM"},{"key":"e_1_3_3_48_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1007\/978-3-642-14186-7_37","volume-title":"Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing.","volume":"6175","author":"Gelder Allen Van","year":"2010","unstructured":"Allen Van Gelder and Ivor Spence. 2010. Zero-one designs produce small hard SAT instances. In Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing.Lecture Notes in Computer Science, Vol. 6175. Springer, 388\u2013397."},{"key":"e_1_3_3_49_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1007\/978-3-319-94144-8_18","volume-title":"Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing.","volume":"10929","author":"Vinyals Marc","year":"2018","unstructured":"Marc Vinyals, Jan Elffers, Jes\u00fas Gir\u00e1ldez-Cru, Stephan Gocht, and Jakob Nordstr\u00f6m. 2018. In between resolution and cutting planes: A study of proof systems for pseudo-boolean SAT solving. In Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing.Lecture Notes in Computer Science, Vol. 10929. Springer, 292\u2013310."},{"key":"e_1_3_3_50_2","volume-title":"An Application of Expanders to the Study of Proofs of the Pigeonhole Principle in Algebraic Propositional Proof Systems","author":"Wo\u0142ochowski \u0141ukasz","year":"2013","unstructured":"\u0141ukasz Wo\u0142ochowski. 2013. An Application of Expanders to the Study of Proofs of the Pigeonhole Principle in Algebraic Propositional Proof Systems. Master\u2019s thesis. University of Warsaw."}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3675668","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3675668","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:04:08Z","timestamp":1750291448000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3675668"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,8]]},"references-count":49,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2024,12,31]]}},"alternative-id":["10.1145\/3675668"],"URL":"https:\/\/doi.org\/10.1145\/3675668","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,8]]},"assertion":[{"value":"2020-01-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-03-23","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}