An Exponential Separation between Regular and General Resolution

by Michael Alekhnovich, Jan Johannsen, Toniann Pitassi, and Alasdair Urquhart

Theory of Computing, Volume 3(5), pp. 81-102, 2007

Bibliography with links to cited articles

[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. [ .html ]
[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ícek: 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 Stalmarck: 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.

This file has been generated by bibtex2html 1.85.