# DPLL and Lovász Local Lemma

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?

• I think the answer to your question is (apparently) "No". Hirsch (2000) exhibited a simple CNF with exactly one satisfying assignment such that no "randomized DPLL" (randomized local search algorithm) can find it in expected polynomial time. See my writeup thi.informatik.uni-frankfurt.de/~jukna/BFC-book/sat-chapter.pdf User: friend, password: catchthecat. Commented Aug 14, 2011 at 19:08
• @Stasys Actually, Dmitriy Itsykson (who you probably know) convinced me that the answer is negative. I'll elaborate on it soon. Argument is more or less the following: we pick a hard unsatisfiable formula and pad it in order to make it easy. Commented Aug 15, 2011 at 0:02
• @ilyaraz Still hoping you'll post an official answer to this question. Commented Jun 8, 2018 at 22:23