Lower bounds for k-DNF resolution on random 3-CNFs

ABSTRACT

We prove exponential lower bounds for the refutation of a random 3-CNF with linear number of clauses by k-DNF Resolution for k ≤ √ log n ⁄ log log n. For this we design a specially tailored random restrictions that preserve the structure of the input random 3-CNF while mapping every k-DNF with large covering number to 1 with high probability. Next we make use of the switching lemma for small restrictions by Segerlind, Buss and Impagliazzo to prove the lower bound.This work improves the previously known lower bound for Res(2) system on random 3-CNFs by Atserias, Bonet and Esteban and the result of Segerlind, Buss, Impagliazzo stating that random O(k²)-CNF do not possess short Res(k) refutations.

REFERENCES

• 1: Michael Alekhnovich , Allan Borodin , Joshua Buresh-Oppenheim , Russell Impagliazzo , Avner Magen , Toniann Pitassi, Toward a Model for Backtracking and Dynamic Programming, Proceedings of the 20th Annual IEEE Conference on Computational Complexity, p.308-322, June 11-15, 2005 [doi>10.1109/CCC.2005.32]
• 2: Albert Atserias , Maria Luisa Bonet , Juan Luis Esteban, Lower bounds for the weak Pigeonhole principle and random formulas beyond resolution, Information and Computation, v.176 n.2, p.136-152, 01 August 2002 [doi>10.1006/inco.2002.3114]
• 3: Michael Alekhnovich , Eli Ben-Sasson , Alexander A. Razborov , Avi Wigderson, Pseudorandom Generators in Propositional Proof Complexity, SIAM Journal on Computing, v.34 n.1, p.67-88, 2005 [doi>10.1137/S0097539701389944]
• 4: M. Alekhnovich, E. Hirsch and D. Itsykson. Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas. To appear in 2005 SAT special issue of the Journal of Automated Reasoning. See also Proc. 31st ICALP: 84-96, 2004.
• 5: M. Alekhnovich , A. Razborov, Lower Bounds for Polynomial Calculus: Non-Binomial Case, Proceedings of the 42nd IEEE symposium on Foundations of Computer Science, p.190, October 14-17, 2001
• 6: 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
• 7: Paul Beame , Richard Karp , Toniann Pitassi , Michael Saks, The Efficiency of Resolution and Davis--Putnam Procedures, SIAM Journal on Computing, v.31 n.4, p.1048-1075, 2002 [doi>10.1137/S0097539700369156]
• 8: Eli Ben-Sasson , Avi Wigderson, Short proofs are narrow—resolution made simple, Journal of the ACM (JACM), v.48 n.2, p.149-169, March 2001 [doi>10.1145/375827.375835]
• 9: 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]
• 10: 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 [doi>10.1145/509907.509985]
• 11: E. Friedgut. Sharp Thresholds of Graph Properties, and the k-sat Problem. In J. Amer. Math. Soc. 12 (1999), no. 4, 1017--1054.
• 12: J. Kraj%čcek On the weak pigeonhole principle. Fundamenta Mathematicae, 170:123--140, 2001.
• 13: Nathan Segerlind , Samuel R. Buss , Russell Impagliazzo, A Switching Lemma for Small Restrictions and Lower Bounds for k - DNF Resolution, Proceedings of the 43rd Symposium on Foundations of Computer Science, p.604, November 16-19, 2002

INDEX TERMS

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

General Terms:
Algorithms, Theory

Keywords:
random 3CNF, res(k), resolution