14
$\begingroup$

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?

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.