Let $\varphi$ be a CNF formula. Suppose that each of $\varphi$'s clauses consist of exactly $t$ literals (and, moreover, all literals within one particular clause correspond to different variables). It is well known that if every clause has less than $2^t / e$ clauses that share variables with it, then $\varphi$ is satisfiable (let us call such formulae easy). Satisfiability can be proved easily using Lovász local lemma. Moreover, using a recent result by Moser and Tardos one can show that one of the satisfying assignments can be found in polynomial expected time using the following very simple procedure:
- Pick a random assignment
- While there exists an unsatisfied clause, resample all its variables.
On the other hand, most of modern SAT solvers are DPLL-based. It means that they try to find a satisfying assignment using brute force with two simple prunings:
- If a formula contains clause with one literal, then we can fix it.
- If one variable occurs in a formula only with (or without) negation, then we can fix it.
The question: is it true that a version of DPLL that splits on random variables finds a satisfying assignment of any easy formula in polynomial expected time?
