Short proofs are narrow—resolution made simple

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Short proofs are narrow—resolution made simple

Full text

Pdf (895 KB)

Source

Annual ACM Symposium on Theory of Computing archive
Proceedings of the thirty-first annual ACM symposium on Theory of computing table of contents

Atlanta, Georgia, United States

Pages: 517 - 526

Year of Publication: 1999

ISBN:1-58113-067-8

Authors

Eli Ben-Sasson	Institute of Computer Science, Hebrew University, Jerusalem, Israel
Avi Wigderson	Institute of Computer Science, Hebrew University, Jerusalem, Israel

Sponsor

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 14, Citation Count: 19

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/301250.301392 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	BEGJ98	M. L. Boner, J. L. Esteban, N. Galesi, J. Johannsen. Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems. submitted.
	BKPS98	P. Beame, R. Karp, T. Pitassi, M. Saks. On the Complexity of Unsatisfiability Proofs for Random k-CNF Formulas. Submitted.
	BP96	P. Beame , T. Pitassi, Simplified and improved resolution lower bounds, Proceedings of the 37th Annual Symposium on Foundations of Computer Science, p.274, October 14-16, 1996
	BP97	Samuel R. Buss , Toniann Pitassi, Resolution and the Weak Pigeonhole Principle, Selected Papers from the11th International Workshop on Computer Science Logic, p.149-156, August 23-29, 1997
	BT88	S. R. Buss , G. Turán, Resolution proofs of generalized pigeonhole principles. (Note), Theoretical Computer Science, v.62 n.3, p.311-317, Dec. 1988 [doi>10.1016/0304-3975(88)90072-2]
	CEI96	Matthew Clegg , Jeffery Edmonds , Russell Impagliazzo, Using the Groebner basis algorithm to find proofs of unsatisfiability, Proceedings of the twenty-eighth annual ACM symposium on Theory of computing, p.174-183, May 22-24, 1996, Philadelphia, Pennsylvania, United States [doi>10.1145/237814.237860]
	CPT77	R. Celoni, W.J. Paul, R.E. Tarjan Space Bounds for a Game on Graphs. In Math. Systems Theory, 10 (1977), pp 239-251.
	CR79	S.A. Cook, R. Reckhow. The relative efficiency of propositional proof systems. In J. of Symbolic Logic, Voi. 44 (1979), pp. 36-50.
	CS88	Vašek Chvátal , Endre Szemerédi, Many hard examples for resolution, Journal of the ACM (JACM), v.35 n.4, p.759-768, Oct. 1988 [doi>10.1145/48014.48016]
	DLL62	Martin Davis , George Logemann , Donald Loveland, A machine program for theorem-proving, Communications of the ACM, v.5 n.7, p.394-397, July 1962 [doi>10.1145/368273.368557]
	H85	A. Haken. The Intractibility of Resolution. In Theoretical Computer Science, 39 (1985), pp. 297-308.
	IPS97	R.Impagliazzo, P Pudl~k, J. Sgall. Lower Bounds for the Polynomial-Calculus and the Groebner Basis Algorithm. Found at Electronic Colloqium on Computational Comple~city, Reports Series 1997, Available at http://www.eccc.unitrier.de/eccc/. Technical Report TR97-042.
	MR98	R. Raz, P. McKenzie. Separation of the Monotone NC Hierarchy. submitted.
	P	N. Pippenger Pebbling. Technical Report, IBM Watson Research Center.
	R95	A.A. Razborov Unprovability of Lower Bounds on Circuit Size in Certain Fragments of Bounded Arithmetic. Izvestia of the RAN, 59 (1), pages 201-222, 1995.
	RR94	Alexander A. Razborov , Steven Rudich, Natural proofs, Proceedings of the twenty-sixth annual ACM symposium on Theory of computing, p.204-213, May 23-25, 1994, Montreal, Quebec, Canada [doi>10.1145/195058.195134]
	RWY97	Alexander Razborov , Avi Wigderson , Andrew Yao, Read-once branching programs, rectangular proofs of the pigeonhole principle and the transversal calculus, Proceedings of the twenty-ninth annual ACM symposium on Theory of computing, p.739-748, May 04-06, 1997, El Paso, Texas, United States [doi>10.1145/258533.258673]
	T68	G.S. Tseitin On the Complexity of Derivation in Propositional Calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part 2. Consultants Bureau, New-York-London, 1968, pp. ! t5-125.
	U87	Alasdair Urquhart, Hard examples for resolution, Journal of the ACM (JACM), v.34 n.1, p.209-219, Jan. 1987 [doi>10.1145/7531.8928]
	U95	A. Urquhart. The Complexity of Propositional Proofs In The Bulletin of Symbolic Logic, Vol 1 No. 4 (1995), pp. 425-467.

CITED BY 19

	Toniann Pitassi , Ran Raz, Regular resolution lower bounds for the weak pigeonhole principle, Proceedings of the thirty-third annual ACM symposium on Theory of computing, p.347-355, July 2001, Hersonissos, Greece
	Ran Raz, Resolution lower bounds for the weak pigeonhole principle, Proceedings of the thiry-fourth annual ACM symposium on Theory of computing, May 19-21, 2002, Montreal, Quebec, Canada
	Michael Alekhnovich , Eli Ben-Sasson , Alexander A. , Avi Wigderson, Space complexity in propositional calculus, Proceedings of the thirty-second annual ACM symposium on Theory of computing, p.358-367, May 21-23, 2000, Portland, Oregon, United States
	Abraham Flaxman, A spectral technique for random satisfiable 3CNF formulas, Proceedings of the fourteenth annual ACM-SIAM symposium on Discrete algorithms, January 12-14, 2003, Baltimore, Maryland
	Uriel Feige, Relations between average case complexity and approximation complexity, Proceedings of the thiry-fourth annual ACM symposium on Theory of computing, May 19-21, 2002, Montreal, Quebec, Canada
	Dimitris Achlioptas , Paul Beame , Michael Molloy, A sharp threshold in proof complexity, Proceedings of the thirty-third annual ACM symposium on Theory of computing, p.337-346, July 2001, Hersonissos, Greece
	Eli Ben-Sasson , Nicola Galesi, Space complexity of random formulae in resolution, Random Structures & Algorithms, v.23 n.1, p.92-109, August 2003
	J. F. Groote , H. Zantema, Resolution and binary decision diagrams cannot simulate each other polynomially, Discrete Applied Mathematics, v.130 n.2, p.157-171, 15 August 2003
	Michael Alekhnovich, Mutilated chessboard problem is exponentially hard for resolution, Theoretical Computer Science, v.310 n.1-3, p.513-525, 01 January 2004
	Pavel Pudlák , Russell Impagliazzo, A lower bound for DLL algorithms for k-SAT (preliminary version), Proceedings of the eleventh annual ACM-SIAM symposium on Discrete algorithms, p.128-136, January 09-11, 2000, San Francisco, California, United States
	Juan Luis Esteban , Jacobo Torán, Space bounds for resolution, Information and Computation, v.171 n.1, p.84-97, November 25, 2001
	Joshua Buresh-Oppenheim , Matthew Clegg , Russell Impagliazzo , Toniann Pitassi, Homogenization and the polynomial calculus, Computational Complexity, v.11 n.3/4, p.91-108, March 2003
	Eli Ben-Sasson, Hard examples for the bounded depth Frege proof system, Computational Complexity, v.11 n.3/4, p.109-136, March 2003
	Eli Ben-Sasson, Hard examples for bounded depth frege, Proceedings of the thiry-fourth annual ACM symposium on Theory of computing, May 19-21, 2002, Montreal, Quebec, Canada
	Eli Ben-Sasson, Size space tradeoffs for resolution, Proceedings of the thiry-fourth annual ACM symposium on Theory of computing, May 19-21, 2002, Montreal, Quebec, Canada
	Alan Frieze , Michael Molloy, The satisfiability threshold for randomly generated binary constraint satisfaction problems, Random Structures & Algorithms, v.28 n.3, p.323-339, May 2006
	Michael L. Littman , Stephen M. Majercik , Toniann Pitassi, Stochastic Boolean Satisfiability, Journal of Automated Reasoning, v.27 n.3, p.251-296, October 2001
	Misha Alekhnovich , Mark Braverman , Vitaly Feldman , Adam R. Klivans , Toniann Pitassi, The complexity of properly learning simple concept classes, Journal of Computer and System Sciences, v.74 n.1, p.16-34, February, 2008
	Paul Beanie , Henry Kautz , Ashish Sabharwal, Understanding the power of clause learning, Proceedings of the 18th international joint conference on Artificial intelligence, p.1194-1201, August 09-15, 2003, Acapulco, Mexico