 |
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.
|