Let @math be a uniformly distributed random @math -SAT formula with @math variables and @math clauses. We present a polynomial time algorithm that finds a satisfying assignment of @math with high probability for constraint densities @math , where @math . Previously no efficient algorithm was known to find satisfying assignments with a nonvanishing probability beyond @math [A. Frieze and S. Suen, J. Algorithms, 20 (1996), pp. 312-355].
Quite a few papers deal with efficient algorithms for random @math -SAT, contributing either rigorous results, non-rigorous evidence based on physics arguments, or experimental evidence. Table summarizes the part of this work that is most relevant to us. The best rigorous result (prior to this work) is due to Frieze and Suen @cite_14 , who proved that SCB'' succeeds for densities @math , where @math is increasing to @math as @math . SCB can be considered a (restricted) DPLL-algorithm. More precisely, SCB combines the shortest clause rule, which is a generalization of Unit Clause, with (very limited) backtracking. Conversely, it is known that DPLL-type algorithms require an exponential running time for densities beyond @math @cite_8 .
@cite_14 @cite_8
2051580875 2001495051
We consider the performance of two algorithms, GUC and SC studied by M. T. Chao and J. Franco SIAM J. Comput.15(1986), 1106?1118;Inform. Sci.51(1990), 289?314 and V. Chvatal and B. Reed in“Proceedings of the 33rd IEEE Symposium on Foundations of Computer Science, 1992,” pp. 620?627, when applied to a random instance ? of a boolean formula in conjunctive normal form withnvariables and ?cn? clauses of sizekeach. For the case wherek=3, we obtain the exact limiting probability that GUC succeeds. We also consider the situation when GUC is allowed to have limited backtracking, and we improve an existing threshold forcbelow which almost all ? is satisfiable. Fork?4, we obtain a similar result regarding SC with limited backtracking. For each k ≤ 4, we give τ k > 0 such that a random k-CNF formula F with n variables and ⌊r k n⌋ 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.