Exponential bounds for DPLL below the satisfiability threshold
Dimitris Achlioptas, Paul W. Beame, Michael S. O. Molloy · TSpace (University of Toronto) · 2004
Abstract For each k> = 4, we give rk> 0 such that a random k-CNF formula F with n variables and brknc clausesis satisfiable with high probability, but ordered-dlltakes exponential time on F with uniformly positiveprobability. Using results of [2], this can be strengthened 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 workhas been devoted to the study of randomly generated satisfiability instances and the performance of differentalgorithms on them. Historically, a major motivation for studying random instances has been the desire tounderstand the hardness of "typical " instances. Indeed, some of the better practical ideas in use today comefrom insights gained by studying the performance of algorithms on random k-SAT instances (defined below).Let Ck(n) denote the set of all possible disjunctionsof 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 clausesfrom Ck(n) and taking their conjunction. We will saythat a sequence of random events E n occurs with highprobability (w.h.p.) if lim n!1 Pr[En] = 1 and with uni-formly positive probability if lim inf n!1 Pr[En]> 0.It is widely believed that for each k> = 3, thereexists a constant ck such that Fk(n, m = cn) is w.h.p.satisfiable if c ck.Currently, the best general bounds are 2 k ln 2- O(k) c).Let res(F) denote the size of the minimal resolutionrefutation of a formula F (we define res(F) to be infinitewhen F is satisfiable). A celebrated result of Chv'ataland Szemer'edi [5] asserts that for all k> = 3 and every