First, let me restate the problem in more “proof‐system” language. A classic fact is that

1. If you have an LLL‐easy CNF—i.e. every clause has size exactly (t), and each clause shares variables with at most (\tfrac{2^t}{e}) other clauses—then the Lovász Local Lemma shows a satisfying assignment exists.

2. Moser–Tardos then give a randomized local‐resampling procedure (“pick any violated clause, resample all its (t) variables at random, repeat until every clause is satisfied”) which runs in expected polynomial time.

On the other hand, a vanilla DPLL solver with
• unit-propagation and
• pure-literal elimination,
and otherwise branching on a random unassigned variable, corresponds exactly to a randomized tree‐resolution proof search. The question is:

Does this natural randomized DPLL‐style search also solve _every_ LLL‐easy formula in expected polynomial time?

Answer: Nobody knows. It’s wide open.

Here are the key points why it remains unresolved.

1. Moser–Tardos vs. tree‐resolution.
   The Moser–Tardos algorithm is not a resolution procedure at all, but a form of local search/resampling. In particular it never produces a resolution proof—let alone a tree-resolution proof—of size polynomial in (n). What it shows is that with high probability you only do (O(n)) “resampling steps,” but those steps do not translate into “DPLL nodes” directly.

2. DPLL ≡ tree‐resolution.
   It is well known that a run of DPLL with just unit‐propagation and pure‐literal elimination corresponds exactly to producing a tree‐resolution refutation (or, in the satisfiable case, a small tree‐resolution proof of satisfiability). Thus to show that DPLL finds a solution in polynomial expected time is equivalent to showing every LLL‐easy CNF has a polynomial-sized tree-resolution proof of satisfiability.

3. We do not have such a tree‐resolution bound.
   All the known proofs of the Lovász Local Lemma (even the constructive Moser–Tardos proof) do not give polynomial-size tree‐resolution proofs. In fact, tree resolution is strictly weaker than the kind of resampling argument Moser–Tardos uses. No one has found a way to convert the resampling process into a small‐size tree‐resolution derivation, nor to bound the size of the minimal DPLL tree on LLL‐easy formulas.

4. No counterexample is known either.
   Conversely, no one has yet exhibited an LLL‐easy family of formulas for which every DPLL‐style search—branching on any random ordering of variables—provably takes super-polynomial time.

So the state of affairs is:

• Positive side: Moser–Tardos gives a polynomial‐time randomized algorithm, but it’s not DPLL.
• Negative side: There is no known lower bound (no explicit LLL‐easy formula that forces DPLL into exponential time).
• Conclusion: Whether DPLL with random splitting (and the two standard prunings) solves all LLL‐easy CNFs in expected polynomial time is an open problem.

If you could show that any DPLL tree on an LLL‐easy formula must, in expectation, be only polynomially large, you would in effect be proving that every LLL-easy CNF has a small tree–resolution proof. Conversely, any explicit family of LLL-easy formulas that forces all DPLL runs into super-polynomial size would separate the power of the Local Lemma from vanilla tree resolution. Neither direction is known at present.