
Recognizing more unsatisfiable random 3SAT
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.
