Recognizing more unsatisfiable random 3-SAT instances efficiently
  • Postscript version.
  • Dvi version.
  • PDF version.

  • Abstract:

    It is known that random $k$-SAT instances with at least $dn$ clauses where $d=d_k$ is a suitable constant are unsatisfiable (with high probability). This paper deals with the question to certify the unsatisfiability of a random $3$-SAT instance in polynomial time. A backtracking based algorithm of Beame et al. works for random $3$-SAT instances with at least $n^2 /\log n$ clauses. This is the best result known by now. We improve the $n^2/\log n$ bound attained by Beame et al. to $n^{3/2+\varepsilon}$ for any $\varepsilon>0$. Our approach extends the spectral approach introduced to the study of random $k$-SAT instances for $k\ge 4$ in previous work of the second author.