Exponential bounds for DPLL below the satisfiability threshold

ABSTRACT

For each k ≤ 4, we give τk > 0 such that a random k-CNF formula F with n variables and ⌊rkn⌋ clauses is satisfiable with high probability, but ORDERED-DLL takes exponential time on F with uniformly positive probability. Using results of [2], this can be strengthened to a high probability result for certain natural backtracking schemes and extended to many other DPLL algorithms.

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: 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 [doi>10.1145/380752.380820]
• 3: D. Achlioptas and Y. Peres. The random k-SAT threshold is 2k ln 2 - O(k). STOC'03, pp. 223--231.
• 4: 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]
• 5: 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]