[1]   Ron Aharoni and Nathan Linial: Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas. J. Combin. Theory Ser. A, 43(2):196–204, 1986. [doi:10.1016/0097-3165(86)90060-9]

[2]   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]

[3]   Michael Alekhnovich, Jan Johannsen, Toniann Pitassi, and Alasdair Urquhart: An exponential separation between regular and general resolution. Theory of Computing, 3(5):81–102, 2007. Preliminary version in STOC’02. [doi:10.4086/toc.2007.v003a005]

[4]   Carlos Ansótegui, María Luisa Bonet, Jordi Levy, and Felip Manyà: Measuring the hardness of SAT instances. In Proc. 23rd AAAI Conference on Artificial Intelligence (AAAI’08), pp. 222–228. AAAI Press, 2008. AAAI. [ACM:1620032]

[5]   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]

[6]   Sven Baumer, Juan Luis Esteban, and Jacobo Torán: Minimally unsatisfiable CNF formulas. Bulletin of the European Association for Theoretical Computer Science, 74:190–192, 2001.

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

[8]   Paul Beame: Proof complexity. In Steven Rudich and Avi Wigderson, editors, Computational Complexity Theory, volume 10 of IAS/Park City Mathematics Series, pp. 199–246. American Mathematical Society, 2004. Available at author’s home page.

[9]   Paul Beame, Christopher Beck, and Russell Impagliazzo: Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space. In Proc. 44th STOC, pp. 213–232. ACM Press, 2012. [doi:10.1145/2213977.2213999]

[10]   Paul Beame, Richard M. Karp, Toniann Pitassi, and Michael E. Saks: The efficiency of resolution and Davis–Putnam procedures. SIAM J. Comput., 31(4):1048–1075, 2002. Preliminary versions in FOCS’96 and STOC’98. [doi:10.1137/S0097539700369156]

[11]   Paul Beame and Toniann Pitassi: Propositional proof complexity: Past, present and future. Bulletin of the European Association for Theoretical Computer Science, 65:66–89, 1998. Available at author’s home page. See also updated version at ECCC.

[12]   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]

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

[14]   Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson: Near optimal separation of tree-like and general resolution. Combinatorica, 24(4):585–603, 2004. [doi:10.1007/s00493-004-0036-5]

[15]   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. Press, 2008. [doi:10.1109/FOCS.2008.42]

[16]   Eli Ben-Sasson and Jakob Nordström: Understanding space in proof complexity: Separations and trade-offs via substitutions. In Proc. 2nd Symp. Innovations in Computer Science (ICS’11), pp. 401–416, 2011. ICS’11.

[17]   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]

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

[19]   María Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen: On the relative complexity of resolution refinements and cutting planes proof systems. SIAM J. Comput., 30(5):1462–1484, 2000. Preliminary version in FOCS’98. [doi:10.1137/S0097539799352474]

[20]   María Luisa Bonet and Nicola Galesi: Optimality of size-width tradeoffs for resolution. Comput. Complexity, 10(4):261–276, 2001. Preliminary version in FOCS’99. [doi:10.1007/s000370100000]

[21]   Joshua Buresh-Oppenheim and Toniann Pitassi: The complexity of resolution refinements. J. Symbolic Logic, 72(4):1336–1352, 2007. Preliminary version in LICS’03. [doi:10.2178/jsl/1203350790]

[22]   Samuel R. Buss and György Turán: Resolution proofs of generalized pigeonhole principles. Theoret. Comput. Sci., 62(3):311–317, 1988. [doi:10.1016/0304-3975(88)90072-2]

[23]   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]

[24]   Stephen A. Cook: The complexity of theorem-proving procedures. In Proc. 3rd STOC, pp. 151–158. ACM Press, 1971. [doi:10.1145/800157.805047]

[25]   Stephen A. Cook: An observation on time-storage trade off. J. Comput. System Sci., 9(3):308–316, 1974. Preliminary version in STOC’73. [doi:10.1016/S0022-0000(74)80046-2]

[26]   Stephen A. Cook and Robert A. Reckhow: The relative efficiency of propositional proof systems. J. Symbolic Logic, 44(1):36–50, 1979. JSTOR.

[27]   Stephen A. Cook and Ravi Sethi: Storage requirements for deterministic polynomial time recognizable languages. J. Comput. System Sci., 13(1):25–37, 1976. Preliminary version in STOC’74. [doi:10.1016/S0022-0000(76)80048-7]

[28]   Martin Davis, George Logemann, and Donald W. Loveland: A machine program for theorem-proving. Commun. ACM, 5(7):394–397, 1962. [doi:10.1145/368273.368557]

[29]   Martin Davis and Hilary Putnam: A computing procedure for quantification theory. J. ACM, 7(3):201–215, 1960. [doi:10.1145/321033.321034]

[30]   Juan Luis Esteban, Nicola Galesi, and Jochen Messner: On the complexity of resolution with bounded conjunctions. Theoret. Comput. Sci., 321(2-3):347–370, 2004. Preliminary version in ICALP’02. [doi:10.1016/j.tcs.2004.04.004]

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

[32]   Juan Luis Esteban and Jacobo Torán: A combinatorial characterization of treelike resolution space. Inform. Process. Lett., 87(6):295–300, 2003. [doi:10.1016/S0020-0190(03)00345-4]

[33]   Zvi Galil: On resolution with clauses of bounded size. SIAM J. Comput., 6(3):444–459, 1977. Preliminary version found in STOC’75. [doi:10.1137/0206031]

[34]   John R. Gilbert, Thomas Lengauer, and Robert Endre Tarjan: The pebbling problem is complete in polynomial space. SIAM J. Comput., 9(3):513–524, 1980. Preliminary version in STOC’79. [doi:10.1137/0209038]

[35]   John R. Gilbert and Robert Endre Tarjan: Variations of a pebble game on graphs. Technical Report STAN-CS-78-661, Stanford University, 1978. InfoLab. [ACM:892174]

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

[37]   Alexander Hertel: Applications of Games to Propositional Proof Complexity. Ph. D. thesis, University of Toronto, 2008. Available at author’s home page. [ACM:1925663]

[38]   Philipp Hertel and Toniann Pitassi: The PSPACE-completeness of black-white pebbling. SIAM J. Comput., 39(6):2622–2682, 2010. Preliminary version in FOCS’07. [doi:10.1137/080713513]

[39]   John E. Hopcroft, Wolfgang J. Paul, and Leslie G. Valiant: On time versus space. J. ACM, 24(2):332–337, 1977. Preliminary version in FOCS’75. [doi:10.1145/322003.322015]

[40]   Matti Järvisalo, Arie Matsliah, Jakob Nordström, and Stanislav Živný: Relating proof complexity measures and practical hardness of SAT. In Proc. 18th Internat. Conf. on Principles and Practice of Constraint Programming (CP’12), pp. 316–331. Springer, 2012. [doi:10.1007/978-3-642-33558-7_25]

[41]   Henry A. Kautz and Bart Selman: The state of SAT. Discr. Appl. Math., 155(12):1514–1524, 2007. [doi:10.1016/j.dam.2006.10.004]

[42]   Maria M. Klawe: A tight bound for black and white pebbles on the pyramid. J. ACM, 32(1):218–228, 1985. Preliminary version in FOCS’83. [doi:10.1145/2455.214115]

[43]   Oliver Kullmann: An application of matroid theory to the SAT problem. In Proc. 15th IEEE Conf. on Computational Complexity (CCC’00), pp. 116–124. IEEE Comp. Soc. Press, 2000. [doi:10.1109/CCC.2000.856741]

[44]   Thomas Lengauer and Robert Endre Tarjan: The space complexity of pebble games on trees. Inform. Process. Lett., 10(4-5):184–188, 1980. [doi:10.1016/0020-0190(80)90136-2]

[45]   João P. Marques-Silva: Practical applications of Boolean satisfiability. In 9th Internat. Workshop on Discrete Event Systems (WODES’08), pp. 74–80, 2008. [doi:10.1109/WODES.2008.4605925]

[46]   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]

[47]   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]

[48]   Jakob Nordström: New wine into old wineskins: A survey of some pebbling classics with supplemental results. Manuscript in preparation. To appear in Foundations and Trends in Theoretical Computer Science. Current draft version available at author’s home page, 2013.

[49]   Jakob Nordström: Pebble games, proof complexity and time-space trade-offs. Logical Methods in Computer Science, 2013. To appear. Available at author’s home page.

[50]   Jakob Nordström and Johan Håstad: Towards an optimal separation of space and length in resolution. In Proc. 40th STOC, pp. 701–710. ACM Press, 2008. [doi:10.1145/1374376.1374478]

[51]   Nicholas Pippenger: Pebbling. Technical Report RC8258, IBM Watson Research Center, 1980. Appeared in Proceedings of the 5th IBM Symposium on Mathematical Foundations of Computer Science, Japan.

[52]   Ran Raz: Resolution lower bounds for the weak pigeonhole principle. J. ACM, 51(2):115–138, 2004. Preliminary version in STOC’02. [doi:10.1145/972639.972640]

[53]   Ran Raz and Pierre McKenzie: Separation of the monotone NC hierarchy. Combinatorica, 19(3):403–435, 1999. Preliminary version in FOCS’97. [doi:10.1007/s004930050062]

[54]   Alexander A. Razborov: Resolution lower bounds for the weak functional pigeonhole principle. Theoret. Comput. Sci., 303(1):233–243, 2003. [doi:10.1016/S0304-3975(02)00453-X]

[55]   Alexander A. Razborov: Resolution lower bounds for perfect matching principles. J. Comput. System Sci., 69(1):3–27, 2004. Preliminary version in CCC’02. [doi:10.1016/j.jcss.2004.01.004]

[56]   John Alan Robinson: A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23–41, 1965. [doi:10.1145/321250.321253]

[57]   Ashish Sabharwal, Paul Beame, and Henry A. Kautz: Using problem structure for efficient clause learning. In 6th Internat. Conf. on Theory and Applications of Satisfiability Testing (SAT’03), pp. 242–256, 2004. [doi:10.1007/978-3-540-24605-3_19]

[58]   The international SAT Competitions web page. http://www.satcompetition.org.

[59]   Nathan Segerlind: The complexity of propositional proofs. Bulletin of Symbolic Logic, 13(4):417–481, 2007. Bulletin of Symbolic Logic.

[60]   Jacobo Torán: Space and width in propositional resolution. Bulletin of the EATCS, 83:86–104, 2004. Universität Ulm.

[61]   Grigori Tseitin: On the complexity of derivation in propositional calculus. In A. O. Silenko, editor, Structures in Constructive Mathematics and mathematical Logic, Part II, pp. 115–125. Consultants Bureau, New York-London, 1968.

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