A sharp threshold in proof complexity

ABSTRACT

We give the first example of a sharp threshold in proof complexity. More precisely, we show that for any sufficiently small &egr;>0 and &Dgr;>2.28, random formulas consisting of (1-&egr;)n 2-clauses and &Dgr n 3-clauses, which are known to be unsatisfiable almost certainly, almost certainly require resolution and Davis-Putnam proofs of unsatisfiability of exponential size, whereas it is easily seen that random formulas with (1+&egr;)n 2-clauses (and &Dgr; n 3 clauses) have linear size proofs of unsatisfiability almost certainly.A consequence of our result also yields the first proof that typical random 3-CNF formulas at ratios below the generally accepted range of the satisfiability threshold (and thus expected to be satisfiable almost certainly) cause natural Davis-Putnam algorithms to take exponential time to find satisfying assignments.

REFERENCES

• 1: Dimitris Achlioptas, Lower bounds for random 3-SAT via differential equations, Theoretical Computer Science, v.265 n.1_2, p.159-185, 08/28/2001 [doi>10.1016/S0304-3975(01)00159-1]
• 2: Demetrios Achlioptas , Allan Borodin , Michael Molloy, Threshold phenomena in random graph colouring and satisfiability, 1999
• 3: Dimitris Achlioptas , Arthur Chtcherba , Gabriel Istrate , Cristopher Moore, The phase transition in 1-in-k SAT and NAE 3-SAT, Proceedings of the twelfth annual ACM-SIAM symposium on Discrete algorithms, p.721-722, January 07-09, 2001, Washington, D.C., United States
• 4: Dimitris Achlioptas , Lefteris M. Kirousis , Evangelos Kranakis , Danny Krizanc, Rigorous results for random (2 + p)-SAT, Theoretical Computer Science, v.265 n.1_2, p.109-129, 08/28/2001 [doi>10.1016/S0304-3975(01)00154-2]
• 5: D. Achioptas , G. B. Sorkin, Optimal myopic algorithms for random 3-SAT, Proceedings of the 41st Annual Symposium on Foundations of Computer Science, p.590, November 12-14, 2000
• 6: Paul Beame , Richard Karp , Toniann Pitassi , Michael Saks, On the complexity of unsatisfiability proofs for random k-CNF formulas, Proceedings of the thirtieth annual ACM symposium on Theory of computing, p.561-571, May 24-26, 1998, Dallas, Texas, United States [doi>10.1145/276698.276870]
• 7: Eli Ben-Sasson , Russell Impagliazzo, Random CNF's are Hard for the Polynomial Calculus, Proceedings of the 40th Annual Symposium on Foundations of Computer Science, p.415, October 17-18, 1999
• 8: Eli Ben-Sasson , Avi Wigderson, Short proofs are narrow—resolution made simple, Proceedings of the thirty-first annual ACM symposium on Theory of computing, p.517-526, May 01-04, 1999, Atlanta, Georgia, United States [doi>10.1145/301250.301392]
• 9: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 10: B. Bollobas. Random graphs. Academic Press, London-New York, 1985.
• 11: 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]
• 12: V. Chvatal and B. Reed. Mick gets some (the odds are on his side). In Proceedings 33rd Annual Symposium on Foundations of Computer Science, pages 620-627, Pittsburgh, PA, October 1992. IEEE.
• 13: 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]
• 14: Cristian Coarfa , Demetrios D. Demopoulos , Alfonso San Miguel Aguirre , Devika Subramanian , Moshe Y. Vardi, Random 3-SAT: The Plot Thickens, Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming, p.143-159, September 18-21, 2000
• 15: 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]
• 16: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 17: E. Friedgut. Sharp thresholds of graph properties, and the k-sat problem. Journal of the American Mathematical Society, 12:1017-1054, 1999.
• 18: 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]
• 19: 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]
• 20: Carla P. Gomes , Bart Selman , Henry Kautz, Boosting combinatorial search through randomization, Proceedings of the fifteenth national/tenth conference on Artificial intelligence/Innovative applications of artificial intelligence, p.431-437, July 1998, Madison, Wisconsin, United States
• 21: Carla P. Gomes , Bart Selman , Nuno Crato , Henry Kautz, Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction Problems, Journal of Automated Reasoning, v.24 n.1-2, p.67-100, February 2000 [doi>10.1023/A:1006314320276]
• 22: Svante Janson , Yannis C. Stamatiou , Malvina Vamvakari, Bounding the unsatisfiability threshold of random 3-SAT, Random Structures & Algorithms, v.17 n.2, p.103-116, Sept. 2000 [doi>10.1002/1098-2418(200009)17:2<103::AID-RSA2>3.0.CO;2-P]
• 23: H. Kautz, D. McAllester, and B. Selman. Encoding plans in propositional logic. In Principles of Knowledge Representation and Reasoning: Proceedings of the Fifth International Conference (KR'96), pages 374-384, 1996.
• 24: H. Kautz and B. Selman. Pushing the envelope: planning, propositional logic, and stochastic search. In Proceedings of the 13th AAAI, pages 1194-2001, 1996.
• 25: S. Kirkpatrick and B. Selman. Critical behavior in the satisfiability of random formulas. Science, 264:1297-1301, May 1994.
• 26: C. J.H. McDiarmid. On the method of bounded differences. In Surveys in Combinatorics, Proceedings of the 12th British Combinatorial Conference, pages 148-188. 1989.
• 27: R. Monasson, R. Zecchina, S. Kirkpatrick, B. Selman, and L. Troyansky. Phase transition and search cost in the (2 + p)-SAT problem. In 4th Workshop on Physics and Computation, (Boston, MA, 1996).
• 28: Rémi Monasson , Riccardo Zecchina , Scott Kirkpatrick , Bart Selman , Lidror Troyansky, 2+p-SAT: relation of typical-case complexity to the nature of the phase transition, Random Structures & Algorithms, v.15 n.3-4, p.414-435, Oct.-Dec. 1999 [doi>10.1002/(SICI)1098-2418(199910/12)15:3/4<414::AID-RSA10>3.0.CO;2-G]
• 29: R. Monasson, R. Zecchina, S. Kirkpatrick, B. Selman, and L. Troyansky. Determining computational complexity from characteristic phase transitions. Nature, 400:133-137, 1999.
• 30: B. Selman and H. Kautz. Domain-independent extensions to GSAT: Solving large structured satisfiability problems. In Proceedings of the 13th IJCAI, pages 290-295, 1993.
• 31: B. Selman, H. Levesque, and D. Mitchell. A new method for solving hard satisfiability problems. In Proceedings Tenth National Conference on Artificial Intelligence (AAAI-92), pages 440-446, 1992.
• 32: 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]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Performance, Theory, Verification