<p>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 <em>easy</em>). Satisfiability can be proved easily using <a href="http://en.wikipedia.org/wiki/Lov%C3%A1sz_local_lemma">Lovász local lemma</a>. Moreover, using <a href="http://arxiv.org/abs/0903.0544">a recent result</a> 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:</p>

<ul>
<li>Pick a random assignment</li>
<li>While there exists an unsatisfied clause, resample all its variables.</li>
</ul>

<p>On the other hand, most of modern SAT solvers are <a href="http://en.wikipedia.org/wiki/DPLL_algorithm">DPLL</a>-based. It means that they try to find a satisfying assignment using brute force with two simple prunings:</p>

<ul>
<li>If a formula contains clause with one literal, then we can fix it.</li>
<li>If one variable occurs in a formula only with (or without) negation, then we can fix it.</li>
</ul>

<p><strong>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?</strong></p>

CC BY-SA 3.0
2011-08-14T19:08:23.673Z
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 http://www.thi.informatik.uni-frankfurt.de/~jukna/BFC-book/sat-chapter.pdf User: friend, password: catchthecat.
Stasys
CC BY-SA 3.0
2011-08-15T00:02:49.327Z
@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.
ilyaraz
CC BY-SA 4.0
2018-06-08T22:23:36.477Z
@ilyaraz Still hoping you'll post an official answer to this question.
Kyle Jones
<cc.complexity-theory><ds.algorithms><sat>
DPLL and Lovász Local Lemma
ilyaraz
# DPLL and Lovász Local Lemma

(Asked by: username_0 on 2011-08-13)

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](http://en.wikipedia.org/wiki/Lov%C3%A1sz_local_lemma). Moreover, using [a recent result](http://arxiv.org/abs/0903.0544) 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](http://en.wikipedia.org/wiki/DPLL_algorithm)-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?**

**Tags:** cc.complexity-theory, ds.algorithms, sat

> **Comments:**
> **username_1**: 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 http://www.thi.informatik.uni-frankfurt.de/~jukna/BFC-book/sat-chapter.pdf User: friend, password: catchthecat.  
> **username_0**: @username_1 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.  
> **username_2**: @username_0 Still hoping you'll post an official answer to this question.  

---

## 0 answers

