An exponential separation between regular and general resolution

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

An exponential separation between regular and general resolution

Full text

Pdf (251 KB)

Source

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

Montreal, Quebec, Canada

SESSION: Session 8A table of contents

Pages: 448 - 456

Year of Publication: 2002

ISBN:1-58113-495-9

Authors

Michael Alekhnovich	Massachusetts Institute of Technology, Cambridge, MA
Jan Johannsen	Ludwig-Maximilians-Universität, München, Germany
Toniann Pitassi	University of Toronto, Toronto, ON, Canada
Alasdair Urquhart	University of Toronto, Toronto, ON, Canada

Sponsor

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 29, Citation Count: 7

Additional Information:

abstract 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/509907.509974 What is a DOI?

ABSTRACT

Two distinct proofs of an exponential separation between regular resolution and unrestricted resolution are given. The previous best known separation between these systems was quasi-polynomial.

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.

	1	P. Beame and T. Pitassi. Simplified and improved resolution lower bounds. In Proc. 28th ACM Symposium on Theory of Computing, 1996.
	2	E. Ben-Sasson, R. Impagliazzo, and A. Wigderson. Near-optimal separation of tree-like and general resolution. ECCC TR00-005, 2000.
	3	Maria Luisa Bonet , Nicola Galesi, A Study of Proof Search Algorithms for Resolution and Polynomial Calculus, Proceedings of the 40th Annual Symposium on Foundations of Computer Science, p.422, October 17-18, 1999
	4	Maria Luisa Bonet , Juan Luis Esteban , Nicola Galesi , Jan Johannsen, On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems, SIAM Journal on Computing, v.30 n.5, p.1462-1484, 2000 [doi>10.1137/S0097539799352474]
	5	Josh Buresh-Oppenheim , Matthew Clegg , Russell Impagliazzo , Toniann Pitassi, Homogenization and the Polynominal Calculus, Proceedings of the 27th International Colloquium on Automata, Languages and Programming, p.926-937, July 09-15, 2000
	6	J. Celoni, W. Paul, and R. Tarjan. Space bounds for a game on graphs. (MATH)ematical Systems Theory, 10:239--251, 1977.
	7	S. Cook and R. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 6:169--184, 1979.
	8	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]
	9	A. Goerdt. Davis-Putnam resolution versus unrestricted resolution. Annals of (MATH)ematics and Artificial Intelligence, 6:1--3, 1992.
	10	Andreas Goerdt, Regular resolution versus unrestricted resolution, SIAM Journal on Computing, v.22 n.4, p.661-683, Aug. 1993 [doi>10.1137/0222044]
	11	Wenqi Huang , Xiangdong Yu, A DNF without regular shortest consensus path, SIAM Journal on Computing, v.16 n.5, p.836-840, Oct. 1987 [doi>10.1137/0216054]
	12	Jan Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press, New York, NY, 1996
	13	Balakrishnan Krishnamurthy, Short proofs for tricky formulas, Acta Informatica, v.22 n.3, p.253-275, Aug. 1985
	14	R. Raz , P. McKenzie, Separation of the monotone NC hierarchy, Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS '97), p.234, October 19-22, 1997
	15	G. Tseitin. On the complexity of derivation in propositional calculus. In A. O. Slisenko, editor, Studies in Constructive (MATH)ematics and (MATH)ematical Logic, Part 2, pages 115--125. Consultants Bureau, New York, 1970.
	16	A. Urquhart. The complexity of propositional proofs. The Bulletin of Symbolic Logic, 1:425--467, 1995.

CITED BY 7

	Jakob Nordström, Narrow proofs may be spacious: separating space and width in resolution, Proceedings of the thirty-eighth annual ACM symposium on Theory of computing, May 21-23, 2006, Seattle, WA, USA
	Alexander (Sasha) Razborov, Eulogy: Michael (Misha) Alekhnovich 1978-2006, ACM SIGACT News, v.38 n.1, p.70-71, March 2007
	Samuel R. Buss , Jan Hoffmann, Note: The NP-hardness of finding a directed acyclic graph for regular resolution, Theoretical Computer Science, v.396 n.1-3, p.271-276, May, 2008
	Matti Järvisalo , Tommi Junttila, Limitations of restricted branching in clause learning, Constraints, v.14 n.3, p.325-356, September 2009
	Paul Beame , Henry Kautz , Ashish Sabharwal, Towards understanding and harnessing the potential of clause learning, Journal of Artificial Intelligence Research, v.22 n.1, p.319-351, July 2004
	Philipp Hertel , Fahiem Bacchus , Toniann Pitassi , Allen Van Gelder, Clause learning can effectively P-simulate general propositional resolution, Proceedings of the 23rd national conference on Artificial intelligence, p.283-290, July 13-17, 2008, Chicago, Illinois
	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