On the complexity of unsatisfiability proofs for random k-CNF formulas

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

On the complexity of unsatisfiability proofs for random k-CNF formulas

Full text

Pdf (1.55 MB)

Source

Annual ACM Symposium on Theory of Computing archive
Proceedings of the thirtieth annual ACM symposium on Theory of computing table of contents

Dallas, Texas, United States

Pages: 561 - 571

Year of Publication: 1998

ISBN:0-89791-962-9

Authors

Paul Beame	Computer Science, and Engineering, University of Washington, Box 352350, Seattle, WA
Richard Karp	Computer Science and Engineering, University of Washington Box, 352350, Seattle, WA
Toniann Pitassi	Computer Science Department, University of Arizona, Tucson, AZ
Michael Saks	Department of Mathematics, Rutgers University, New Brunswick, NJ

Sponsor

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 29, 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/276698.276870 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.

	ASE92	N. Alon, J. Spencer, and P. Erdos. The Probabilisitic Method. John Wiley and Sons, Inc., 1992.
	AV79	D. Angluin and L. Valiant. Fast probabilistic algorithms for Hamiltonian circuits and matchings. Journal of Computer and System Sciences, 18:155-193, 1979.
	BFU93	A. Broder, A. Frieze, and E. Upfal. On the satisfiability and maximum satisfiability of random 3-CNF formulas. January 1993.
	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
	CA96	James M. Crawford , Larry D. Auton, Experimental results on the crossover point in random 3-SAT, Artificial Intelligence, v.81 n.1-2, p.31-57, March 1996 [doi>10.1016/0004-3702(95)00046-1]
	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]
	CF90	Ming-Te Chao , John Franco, Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for the k satisfiability problem, Information Sciences: an International Journal, v.51 n.3, p.289-314, Aug. 1990 [doi>10.1016/0020-0255(90)90030-E]
	CR92	V. Chvfital and B. Reed. Mick gets some (the odds are on his side). In 33nd Annual S3wtposiurn on Founda. tions of Computer Science, pages 620--627, Pittsburgh, PA, October 1992. IEEE.
	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]
	Fri	E. Friedgut. Necessary and sufficient conditions for sharp thresholds of graph properties, and the k-sat problem. Preprint, May 1997.
	FS96	Alan Frieze , Stephen Suen, Analysis of two simple heuristics on a random instance of k-SAT, Journal of Algorithms, v.20 n.2, p.312-355, March 1996 [doi>10.1006/jagm.1996.0016]
	Fu95	Xudong Fu. On the complexi~ of proof systems. Phi) thesis, University of Toronto, 1995.
	Goe96	Andreas Goerdt, A threshold for unsatisfiability, Journal of Computer and System Sciences, v.53 n.3, p.469-486, Dec. 1996 [doi>10.1006/jcss.1996.0081]
	GPFW97	J. Gu, P. W. Purdom, .l. Franco, and B. J. Wah. Algorithms for the Satisfiability (SAT) Problem: A Survey. In Satisftability (SAT) Problem, DIMACS, pages 19- 151. American Mathematical Society, 1997.
	KKK96	Lefteris M. Kirousis , Evangelos Kranakis , Danny Krizanc, Approximating the Unsatisfiability Threshold of Random Formulas (Extended Abstract), Proceedings of the Fourth Annual European Symposium on Algorithms, p.27-38, September 25-27, 1996
	KS94	S. Kirkpatrick and B. $elman. Critical behavior in the satisfiabiHty of random formulas. Science, 264:1297- 1301, May 1994.
	Mit95	D. Mitchell. Propositional satisfiability testing. 1995.
	SML96	Bart Selman , David G. Mitchell , Hector J. Levesque, Generating hard satisfiability problems, Artificial Intelligence, v.81 n.1-2, p.17-29, March 1996 [doi>10.1016/0004-3702(95)00045-3]

CITED BY 19

	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
	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
	John Franco , Allen Van Gelder, A perspective on certain polynomial-time solvable classes of satisfiability, Discrete Applied Mathematics, v.125 n.2-3, p.177-214, February 2003
	Eli Ben-Sasson , Nicola Galesi, Space complexity of random formulae in resolution, Random Structures & Algorithms, v.23 n.1, p.92-109, August 2003
	Chu-Min Li , Sylvain Gérard, On the limit of branching rules for hard random unsatisfiable 3-SAT, Discrete Applied Mathematics, v.130 n.2, p.277-290, 15 August 2003
	Dimitris Achlioptas , Paul Beame , Michael Molloy, A sharp threshold in proof complexity yields lower bounds for satisfiability search, Journal of Computer and System Sciences, v.68 n.2, p.238-268, March 2004
	Albert Atserias, On sufficient conditions for unsatisfiability of random formulas, Journal of the ACM (JACM), v.51 n.2, p.281-311, March 2004
	Simona Cocco , Rémi Monasson, Heuristic average-case analysis of the backtrack resolution of random 3-satisfiability instances, Theoretical Computer Science, v.320 n.2-3, p.345-372, June 14, 2004
	John Franco, Typical case complexity of satisfiability algorithms and the threshold phenomenon, Discrete Applied Mathematics, v.153 n.1, p.89-123, 1 December 2005
	Ke Xu , Wei Li, Many hard examples in exact phase transitions, Theoretical Computer Science, v.355 n.3, p.291-302, 14 April 2006
	Andrej Bogdanov , Luca Trevisan, Average-case complexity, Foundations and Trends® in Theoretical Computer Science, v.2 n.1, p.1-106, October 2006
	John Franco, Some interesting research directions in satisfiability, Annals of Mathematics and Artificial Intelligence, v.28 n.1-4, p.7-15, 2000
	Cristian Coarfa , Demetrios D. Demopoulos , Alfonso San Miguel Aguirre , Devika Subramanian , Moshe Y. Vardi, Random 3-SAT: The Plot Thickens, Constraints, v.8 n.3, p.243-261, July 2003
	Simona Cocco , Rémi Monasson, Restarts and Exponential Acceleration of the Davis–Putnam–Loveland–Logemann Algorithm: A Large Deviation Analysis of the Generalized Unit Clause Heuristic for Random 3-SAT, Annals of Mathematics and Artificial Intelligence, v.43 n.1-4, p.153-172, January 2005
	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
	Kevin Leyton-Brown , Eugene Nudelman , Yoav Shoham, Empirical hardness models: Methodology and a case study on combinatorial auctions, Journal of the ACM (JACM), v.56 n.4, p.1-52, June 2009
	Yong Gao , Joseph Culberson, Consistency and random constraint satisfaction models, Journal of Artificial Intelligence Research, v.28 n.1, p.517-557, January 2007
	Tudor Hulubei , Barry O’Sullivan, Optimal refutations for constraint satisfaction problems, Proceedings of the 19th international joint conference on Artificial intelligence, p.163-168, July 30-August 05, 2005, Edinburgh, Scotland