[1]   Fahiem Bacchus, Philipp Hertel, and Toniann Pitassi: The complexity of resolution with caching. 2006. Unpublished manuscript.

[2]   Paul Beame, Henry Kautz, and Ashish Sabharwal: Towards understanding and harnessing the potential of clause learning. Journal of Artifical Intelligence Research, 22:319–351, 2004.

[3]   Paul Beame and Toniann Pitassi: Simplified and improved resolution lower bounds. In Proc. 37th FOCS, pp. 274–282. IEEE Comp. Soc. Press, 1996. [FOCS:10.1109/SFCS.1996.548486].

[4]   Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson: Near-optimal separation of tree-like and general resolution. ECCC TR00-005, 2000. [ECCC:TR00-005].

[5]   M. Bonet and N. Galesi: A study of proof search algorithms for resolution and polynomial calculus. In Proc. 40th FOCS, pp. 422–432. IEEE Comp. Soc. Press, 1999. [FOCS:10.1109/SFFCS.1999.814614].

[6]   Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen: On the relative complexity of resolution restrictions and cutting planes proof systems. SIAM Journal of Computing, 30:1462–1484, 2000. [SICOMP:10.1137/S0097539799352474].

[7]   Joshua Buresh-Oppenheim, Matthew Clegg, Russell Impagliazzo, and Toniann Pitassi: Homogenization and the polynomial calculus. In Proc. 27th International Colloquium on Automata, Languages and Programming, pp. 926–937. Springer, 2000. [ICALP:fvxybba423y153b8].

[8]   James Celoni, Wolfgang Paul, and Robert Tarjan: Space bounds for a game on graphs. Mathematical Systems Theory, 10:239–251, 1977. [Springer:u32u2r202jv33611].

[9]   Stephen A. Cook: A short proof of the pigeon hole principle using extended resolution. SIGACT News, 8(4):28–32, 1976. [SIGACT:10.1145/1008335.1008338].

[10]   Stephen A. Cook and Robert A. Reckhow: The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 6:169–184, 1979.

[11]   Martin Davis, George Logemann, and Donald Loveland: A machine program for theorem proving. Communications of the Association for Computing Machinery, 5:394–397, 1962. [ACM:10.1145/368273.368557].

[12]   Niklas Een and Niklas Sörensson: An extensible SAT-solver. In Proc. 6th International Conference on Theory and Applications of Satisfiability Testing, pp. 502–518. Springer, 2003. [Springer:x9uavq4vpvqntt23].

[13]   Andreas Goerdt: Davis-Putnam resolution versus unrestricted resolution. Annals of Mathematics and Artificial Intelligence, 6:169–184, 1992. [Springer:k008110v05867897].

[14]    Andreas Goerdt: Regular resolution versus unrestricted resolution. SIAM Journal of Computing, 22:661–683, 1993. [SICOMP:10.1137/0222044].

[15]   Armin Haken: The intractability of resolution. Theoretical Computer Science, 39:297–308, 1985. [TCS:10.1016/0304-3975(85)90144-6].

[16]   Wenqi Huang and Xiangdong Yu: A DNF without regular shortest consensus path. SIAM Journal on Computing, 16:836–840, 1987. [SICOMP:10.1137/0216054].

[17]   Jan Krajíček: Bounded Arithmetic, Propositional Logic and Complexity Theory. Cambridge University Press, 1995.

[18]   Balakrishnan Krishnamurthy: Short proofs for tricky formulas. Acta Informatica, 22:253–274, 1985. [ActaInf:mp65776636126242].

[19]   Matthew Moskewicz, Conor Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik: Chaff: Engineering an efficient SAT solver. In Proc. 38th Design Automation Conference, pp. 530–535. ACM Press, 2001. [ACM:10.1145/378239.379017].

[20]   Alexander Nadel: Backtrack search algorithms for propositional logic satisfiability: Review and innovations. Master’s thesis, Hebrew University, 2002.

[21]   Ran Raz and Pierre McKenzie: Separation of the monotone NC hierarchy. Combinatorica, 19:403–435, 1999. Preliminary Version in: Proc. 38th FOCS, 1997. [Springer:h4prxbwxpn1c8xqh].

[22]   Gunnar Stålmarck: Short resolution proofs for a sequence of tricky formulas. Acta Informatica, 33:277–280, 1996. [ActaInf:lhrhe2glkmgflbu1].

[23]   G. S. Tseitin: On the complexity of derivation in propositional calculus. In A. O. Slisenko, editor, Studies in Constructive Mathematics and Mathematical Logic, Part 2, pp. 115–125. Consultants Bureau, New York, 1970.

[24]   Alasdair Urquhart: The complexity of propositional proofs. The Bulletin of Symbolic Logic, 1:425–467, 1995.