[1]   Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson: Space complexity in propositional calculus. SIAM J. Comput., 31(4):1184–1211, 2002. Preliminary version in STOC’00. [doi:10.1137/S0097539700366735]

[2]   Michael Alekhnovich and Alexander A. Razborov: Lower bounds for polynomial calculus: Non-binomial case. Proc. Steklov Inst. Math., 242:18–35, 2003. Available at Math-Net.Ru (Russian with English home page) and at author’s home page (English). Preliminary version in FOCS’01.

[3]   Noga Alon and Joel Spencer: The Probabilistic Method. Wiley, 2nd edition, 2000. [doi:10.1002/0471722154]

[4]   Albert Atserias and Víctor Dalmau: A combinatorial characterization of resolution width. J. Comput. System Sci., 74(3):323–334, 2008. Preliminary version in CCC’03. [doi:10.1016/j.jcss.2007.06.025]

[5]   Per Austrin and Kilian Risse: Perfect matching in random graphs is as hard as Tseitin. TheoretiCS, 1(2):1–47, 2022. Preliminary version in SODA’22. [doi:10.46298/theoretics.22.2]

[6]   Roberto J. Bayardo Jr. and Robert Schrag: Using CSP look-back techniques to solve real-world SAT instances. In Proc. 14th Nat’l Conf. on Artificial Intelligence (AAAI’97), pp. 203–208, 1997. Available at ACM DL.

[7]   Paul Beame, Chris Beck, and Russell Impagliazzo: Time-space tradeoffs in resolution: Superpolynomial lower bounds for superlinear space. SIAM J. Comput., 45(4):1612–1645, 2016. Preliminary version in STOC’12. [doi:10.1137/130914085]

[8]   Chris Beck, Jakob Nordström, and Bangsheng Tang: Some trade-off results for polynomial calculus. In Proc. 45th STOC, pp. 813–822. ACM Press, 2013. [doi:10.1145/2488608.2488711]

[9]   Eli Ben-Sasson: Size-space tradeoffs for resolution. SIAM J. Comput., 38(6):2511–2525, 2009. Preliminary version in STOC’02. [doi:10.1137/080723880]

[10]   Eli Ben-Sasson and Nicola Galesi: Space complexity of random formulae in resolution. Random Struct. Algor., 23(1):92–109, 2003. Preliminary version in CCC’01. [doi:10.1002/rsa.10089]

[11]   Eli Ben-Sasson and Jakob Nordström: Short proofs may be spacious: An optimal separation of space and length in resolution. In Proc. 49th FOCS, pp. 709–718. IEEE Comp. Soc., 2008. [doi:10.1109/FOCS.2008.42]

[12]   Eli Ben-Sasson and Jakob Nordström: Understanding space in proof complexity: Separations and trade-offs via substitutions. In Proc. 2nd Innovations in Comp. Sci. Conf. (ICS’11), pp. 401–416. Tsinghua U., 2011. Available at Tsinghua U.

[13]   Eli Ben-Sasson and Avi Wigderson: Short proofs are narrow—resolution made simple. J. ACM, 48(2):149–169, 2001. Preliminary version in STOC’99. [doi:10.1145/375827.375835]

[14]   Patrick Bennett, Ilario Bonacina, Nicola Galesi, Tony Huynh, Mike Molloy, and Paul Wollan: Space proof complexity for random 3-CNFs. Inform. Comput., 255(14):165–176, 2017. [doi:10.1016/j.ic.2017.06.003]

[15]   Archie Blake: Canonical Expressions in Boolean Algebra. Ph. D. thesis, University of Chicago, 1937.

[16]   Béla Bollobás: The isoperimetric number of random regular graphs. Europ. J. Combinat., 9(3):241–244, 1988. [doi:10.1016/S0195-6698(88)80014-3]

[17]   Béla Bollobás and Imre Leader: Edge-isoperimetric inequalities in the grid. Combinatorica, 11:299–314, 1991. [doi:10.1007/BF01275667]

[18]   Ilario Bonacina and Nicola Galesi: A framework for space complexity in algebraic proof systems. J. ACM, 62(3):23:1–20, 2015. Preliminary version in ITCS’13. [doi:10.1145/2699438]

[19]   Michael Brickenstein and Alexander Dreyer: PolyBoRi: A framework for Gröbner-basis computations with Boolean polynomials. J. Symbolic Comput., 44(9):1326–1345, 2009. [doi:10.1016/j.jsc.2008.02.017]

[20]   Samuel R. Buss and Jakob Nordström: Proof complexity and SAT solving. In Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, chapter 7, pp. 233–350. IOS Press, 2nd edition, 2021. [doi:10.3233/FAIA200990]

[21]   Vašek Chvátal and Endre Szemerédi: Many hard examples for resolution. J. ACM, 35(4):759–768, 1988. [doi:10.1145/48014.48016]

[22]   Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo: Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proc. 28th STOC, pp. 174–183. ACM Press, 1996. [doi:10.1145/237814.237860]

[23]   Stephen A. Cook and Robert A. Reckhow: The relative efficiency of propositional proof systems. J. Symbolic Logic, 44(1):36–50, 1979. Preliminary version in STOC’74. [doi:10.2307/2273702]

[24]   Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Dmitry Sokolov: The power of negative reasoning. In Proc. 36th Comput. Complexity Conf. (CCC’21), pp. 40:1–24. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2021. [doi:10.4230/LIPIcs.CCC.2021.40]

[25]   Juan Luis Esteban and Jacobo Torán: Space bounds for resolution. Inform. Comput., 171(1):84–97, 2001. Preliminary version in STACS’99 and CSL’99. [doi:10.1006/inco.2001.2921]

[26]   Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals: Towards an understanding of polynomial calculus: New separations and lower bounds (Extended abstract). In Proc. 40th Internat. Colloq. on Automata, Languages, and Programming (ICALP’13), pp. 437–448. Springer, 2013. [doi:10.1007/978-3-642-39206-1_37]

[27]   Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, and Neil Thapen: Space complexity in polynomial calculus. SIAM J. Comput., 44(4):1119–1153, 2015. Preliminary version in CCC’12. [doi:10.1137/120895950]

[28]   Nicola Galesi, Leszek Kołodziejczyk, and Neil Thapen: Polynomial calculus space and resolution width. In Proc. 60th FOCS, pp. 1325–1337. IEEE Comp. Soc., 2019. [doi:10.1109/FOCS.2019.00081]

[29]   Armin Haken: The intractability of resolution. Theoret. Comput. Sci., 39(2–3):297–308, 1985. [doi:10.1016/0304-3975(85)90144-6]

[30]   Trinh Huynh and Jakob Nordström: On the virtue of succinct proofs: Amplifying communication complexity hardness to time-space trade-offs in proof complexity (Extended abstract). In Proc. 44th STOC, pp. 233–248. ACM Press, 2012. [doi:10.1145/2213977.2214000]

[31]   Russell Impagliazzo and Valentine Kabanets: Constructive proofs of concentration bounds. In Proc. 14th Internat. Workshop on Randomization and Computation (RANDOM’10), pp. 617–631. Springer, 2010. [doi:10.1007/978-3-642-15369-3_46]

[32]   Russell Impagliazzo, Pavel Pudlák, and Jiří Sgall: Lower bounds for the polynomial calculus and the Gröbner basis algorithm. Comput. Complexity, 8(2):127–144, 1999. [doi:10.1007/s000370050024]

[33]   Svante Janson, Tomasz Łuczak, and Andrzej Ruciński: Random Graphs. Wiley-Interscience, 2000. [doi:10.1002/9781118032718]

[34]   Jeong Han Kim and Nicholas C. Wormald: Random matchings which induce Hamilton cycles, and Hamiltonian decompositions of random regular graphs. J. Combin. Theory–B, 81(1):20–44, 2001. [doi:10.1006/jctb.2000.1991]

[35]   Jan Krajíček: Proof Complexity. Volume 170 of Encyclopedia Math. and Its Appl. Cambridge Univ. Press, 2019. [doi:10.1017/9781108242066]

[36]   João P. Marques-Silva and Karem A. Sakallah: GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, 48(5):506–521, 1999. Preliminary version in ICCAD’96. [doi:10.1109/12.769433]

[37]   Mladen Mikša and Jakob Nordström: A generalized method for proving polynomial calculus degree lower bounds. J. ACM, 71(6):1–43, 2024. Preliminary version in CCC’15. [doi:10.1145/3675668]

[38]   Moshe Morgenstern: Existence and explicit constructions of q + 1 regular Ramanujan graphs for every prime power q. J. Combin. Theory–B, 62(1):44–62, 1994. [doi:10.1006/jctb.1994.1054]

[39]   Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik: Chaff: Engineering an efficient SAT solver. In Proc. 38th Design Automation Conf. (DAC’01), pp. 530–535, 2001. [doi:10.1145/378239.379017]

[40]   Jakob Nordström: Narrow proofs may be spacious: Separating space and width in resolution. SIAM J. Comput., 39(1):59–121, 2009. Preliminary version in STOC’06. [doi:10.1137/060668250]

[41]   Jakob Nordström and Johan Håstad: Towards an optimal separation of space and length in resolution. Theory of Computing, 9(14):471–557, 2013. Preliminary version in STOC’08. [doi:10.4086/toc.2013.v009a014]

[42]   Alessandro Panconesi and Aravind Srinivasan: Randomized distributed edge coloring via an extension of the Chernoff–Hoeffding bounds. SIAM J. Comput., 26(2):350–368, 1997. [doi:10.1137/S0097539793250767]

[43]   Alexander A. Razborov: Lower bounds for the polynomial calculus. Comput. Complexity, 7(4):291–324, 1998. [doi:10.1007/s000370050013]

[44]   Alasdair Urquhart: Hard examples for resolution. J. ACM, 34(1):209–219, 1987. [doi:10.1145/7531.8928]

[45]   Nicholas C. Wormald: Models of random regular graphs. In John D. Lamb and Donald A. Preece, editors, Surveys in Combinatorics, pp. 239–298. Cambridge Univ. Press, 1999. [doi:10.1017/CBO9780511721335.010]