Exponential bounds for DPLL below the satisfiability threshold

For each k ≥ 4, we give rk> 0 such that a random k-CNF formula F with n variables and brknc 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 strength-ened to a high probability result for certain natu-ral backtracking schemes and extended to many other DPLL algorithms. 1 Previous work In the last twenty years a significant amount of work has been devoted to the study of randomly generated satisfiability instances and the performance of different algorithms on them. Historically, a major motivation for studying random instances has been the desire to understand the hardness of “typical ” instances. Indeed, some of the better practical ideas in use today come from insights gained by studying the performance of algorithms on random k-SAT instances (defined below). Let Ck(n) denote the set of all possible disjunctions of k distinct, non-complementary literals (k-clauses) from some canonical set of n Boolean variables. A ran-dom k-CNF formula Fk(n,m) is formed by selecting uni-formly, independently, and with replacement m clauses from Ck(n) and taking their conjunction. We will say that a sequence of random events En occurs with high probability (w.h.p.) if limn→ ∞ Pr[En] = 1 and with uni-formly positive probability if lim infn→ ∞ Pr[En]> 0. It is widely believed that for each k ≥ 3, there exists a constant ck such that Fk(n,m = cn) is w.h.p. satisfiable if c < ck and w.h.p. unsatisfiable if c> ck. Currently, the best general bounds are 2k ln 2−O(k) < ck < 2k ln 2 − O(1) , where by ck < c we mean that Fk(n, cn) is w.h.p. unsatisfiable (analogously for ck> c). Let res(F) denote the size of the minimal resolution refutation of a formula F (we define res(F) to be infinite when F is satisfiable). A celebrated result of Chvátal and Szemerédi [5] asserts that for all k ≥ 3 and ever