Short answer
————————————————
Nobody knows. At the moment there is neither
• a proof that a (pure) DPLL procedure that always branches on a randomly chosen variable finishes in polynomial expected time on every instance that satisfies the Lovász-Local-Lemma (LLL) condition, nor
• an instance that satisfies this LLL condition for which the same DPLL procedure can be shown to need super-polynomial (let alone exponential) expected running time.
So the question you ask is open.
Why we do not have an upper bound
———————————————————
The Moser–Tardos algorithm that turns the LLL into an efficient constructive
result relies on “resampling’’ the variables of a clause without ever
exploring assignments that are inconsistent with the current partial
assignment. A DPLL tree search behaves quite differently: whenever it
guesses a value for a variable it explores both possibilities, and the whole
sub-tree corresponding to the first value has to be proved unsatisfiable
before the procedure can back-track and try the second value. Proving a
polynomial bound for DPLL therefore amounts to proving that every
tree–resolution refutation of an LLL instance that is inconsistent with the
target (unknown) satisfying assignment is short; at present we do not know
how to do that.
Why we do not have a lower bound
———————————————————
To show a lower bound one has to exhibit a satisfiable formula F that
(1) satisfies the LLL condition
(p = 2^–t, d < 2^t / e – 1),
and
(2) forces a random-branching DPLL algorithm to construct an exponentially large search tree before it stumbles upon a satisfying assignment.
Lower bounds for DPLL are usually obtained by exhibiting formulas whose every unsatisfiable sub-instance requires an exponentially long tree-resolution proof (Tseitin formulas, pigeon-hole principles, etc.). All such formulas violate the LLL condition, so one has to hide one of them inside a satisfiable “wrapper’’ while keeping the overall clause-dependency below the 2^t / e threshold. No one has succeeded in doing this so far. On the other hand, nothing rules it out either.
Related partial results
——————————————
• For many random k-CNF distributions with clause density well below the
satisfiability threshold (far below the LLL bound) simple DPLL variants are
known to succeed in expected polynomial time, but that says nothing about
worst-case LLL instances.
• Exponential lower bounds are known for DPLL on satisfiable formulas (Beame, Kautz & Sabharwal, 2004; Paturi & Pudlák, 2005, and later work) in which every variable appears only a constant number of times. Unfortunately the constants involved are too large for the LLL condition to hold.
• If additional inference rules (e.g. clause learning with certain restart policies) are allowed, one can simulate the Moser–Tardos resampling algorithm inside a SAT solver and obtain a polynomial bound; but that is no longer the plain DPLL framework you asked about.
Conclusion
——————
Whether plain DPLL with random variable selection is always fast on
LLL-satisfiable formulas is an interesting and, at present, open research
problem. Neither a proof nor a counterexample is known.
Was this answer helpful?
version: o3-2025-04-16
Status: UQ Validated
Validated: 8 months ago
Status: Failed Human Verification
Verified: 7 months ago
Loading model reviews...
Loading reviews...