Short answer: No. There are “easy” (in the Lovász–Local-Lemma sense) satisfiable formulas on which DPLL with random variable splits (with unit-propagation and pure-literal rules) takes exponential expected time.

Why the LLL condition does not help DPLL

• The LLL condition (each t-clause conflicts with fewer than 2^t/e other clauses) guarantees existence of a satisfying assignment and, via the Moser–Tardos resampling algorithm, a polynomial-time randomized algorithm to find one. But this algorithm is not a backtracking search; it exploits local independence in a way that DPLL does not.
• DPLL without clause learning is essentially equivalent to tree-like resolution. Exponential lower bounds on tree-like resolution translate to exponential DPLL search trees for unlucky variable orders.

A standard “selector” construction giving a counterexample

1. Start with any family Fn of unsatisfiable CNF formulas with all of the following properties:

   • Constant clause width and bounded variable occurrences (hence each clause shares variables with only O(1) other clauses).
   • Exponential lower bound for tree-like resolution (and thus for DPLL), e.g., pebbling contradictions on bounded-degree graphs give size 2^Ω(n) tree-like resolution lower bounds.

2. Turn Fn into a satisfiable formula Gn by “hiding” Fn behind a sparse selector gadget:

   • For each clause Ci in Fn introduce a fresh selector variable yi and replace Ci by (yi ∨ Ci).
   • Enforce that all yi take the same value by linking them in a sparse chain of equivalences yi ↔ yi+1, implemented as two clauses (¬yi ∨ yi+1) and (yi ∨ ¬yi+1). This keeps every variable occurrence bounded and every clause sharing only O(1) variables with others.
   • Pad every clause with clause-unique “dummy” variables (used in both polarities across a couple of clauses to avoid purity) so that every clause has exactly t literals. Padding variables are arranged so they introduce at most O(1) additional clause overlaps.

   Properties:

   • If any yi is set to 0, unit propagation through the yi ↔ yi+1 chain forces all yj = 0 and the instance reduces to Fn, which is unsatisfiable and hard for DPLL (exponential).
   • If any yi is set to 1, unit propagation forces all yj = 1 and all (yi ∨ Ci) clauses become satisfied; the remaining gadget and padding can be satisfied in polynomial time.
   • Each clause has width exactly t, and each clause shares variables with only a constant number D of other clauses (coming from the bounded-degree Fn plus O(1) from the selector chain and padding). Choosing t large enough constant ensures D < 2^t/e, i.e., Gn is “easy” in the LLL sense.

3. Randomized DPLL on Gn:

   • The solver picks a random unset variable and a random truth value. With probability at least 1/2, the first selector variable it sets is assigned 0; unit propagation then forces all selectors to 0, immediately exposing Fn. At that point the solver must refute Fn, which by construction requires size 2^Ω(n) tree-like resolution (hence an exponential DPLL search).
   • With probability at most 1/2, the first selector is set to 1 and the instance becomes easy. But the constant probability of hitting the “bad” branch implies exponential expected time: E[time] ≥ (1/2)·2^Ω(n).

   Note: One can also ensure that no variable is initially pure (padding variables occur in both polarities), so the pure-literal rule does not trivialize the instance.

Conclusion

• There exist satisfiable t-CNF formulas that satisfy the Lovász–Local-Lemma dependency condition (hence are “easy” in that sense) for which DPLL with random variable splits has exponential expected running time.
• This exhibits a genuine algorithmic gap: the Moser–Tardos resampling algorithm finds a satisfying assignment in expected polynomial time on these instances, whereas randomized DPLL does not.

Pointers to supporting literature

• Exponential lower bounds for tree-like resolution (DPLL): e.g., Beame, Karp, Pitassi, Saks, The Efficiency of Resolution and Davis–Putnam Procedures, SIAM J. Comput. 2004; and pebbling-contradiction lower bounds (see Ben-Sasson and Wigderson, Short proofs are narrow, JACM 2001, and subsequent work).
• Technique of embedding a hard unsatisfiable core behind a selector to create hard satisfiable instances for backtracking/DPLL goes back to work by Hirsch and others on lower bounds for DPLL-like algorithms.

Therefore the answer to the question is No.