Recognizing More Unsatisfiable Random k -SAT Instances Efficiently

It is known that random k-SAT instances with at least $cn$ clauses, where c = cₖ is a suitable constant, are unsatisfiable (with high probability). We consider the problem to certify efficiently the unsatisfiability of such formulas. A backtracking-based algorithm of Beame et al. [SIAM J. Comput.,} 31 (2002), pp. 1048--1075] shows that k-SAT instances with at least nᵏ⁻¹/(log n)ᵏ⁻² clauses can be certified unsatisfiable in polynomial time. We employ spectral methods to improve on this bound. For even k≥ 4 we present a polynomial time algorithm which certifies random k-SAT instances with at least n(k/2)+o(1) clauses as unsatisfiable (with high probability). For odd k we focus on 3-SAT instances and obtain an efficient algorithm for formulas with at least n3/2+ε clauses, where ε >0 is an arbitrary constant.