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?

  • 1
    $\begingroup$ 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. $\endgroup$
    – Stasys
    Commented Aug 14, 2011 at 19:08
  • $\begingroup$ @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. $\endgroup$
    – ilyaraz
    Commented Aug 15, 2011 at 0:02
  • $\begingroup$ @ilyaraz Still hoping you'll post an official answer to this question. $\endgroup$
    – Kyle Jones
    Commented Jun 8, 2018 at 22:23


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.