Recognizing more unsatisfiable random 3-SAT instances Efficiently

Abstract

It is known that random k-SAT instances with at least dn clauses where d = dk 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 n2/log n clauses. This is the best result known by now. We improve the n2/log n bound attained by Beame et al. to n3/2ε for any ε > 0. Our approach extends the spectral approach introduced to the study of random k-SAT instances for k ≥ 4 in previous work of the second author. © 2011 Springer-Verlag Berlin Heidelberg.