Refuting Smoothed 3CNF Formulas

We introduce the following model for generating .semi-random 3CNF formulas. First, an adversary is allowed to pick an arbitrary formula with n varialdes and in clauses. Then, the formula is slightly perturbed at random. Namely, the smoothing operation leaves the variables of the formula unchanged, but flips the polarity of every variable occurrence in the formula independently with probability a. If the density m/n of a 3CNF formula exceeds a certain threshold value (say, 5epsiv^-3) then the smoothing operation almost surely results in a non-satisfiable formula. We present a randomized polynomial time refutation algorithm that for every sufficiently dense 3CNF formula manages to refute most of its smoothed instantiations. The density requirement for our refutation algorithm is roughly epsiv^-2 radic(n log log n), which almost matches the density Omega( radicn) required bv known algorithms for refuting 3CNF formulas that are completely random.