Recognizing More Unsatisfiable Random k -SAT Instances Efficiently
Joel I. Friedman, Andreas Goerdt, Michael Krivelevich · SIAM Journal on Computing · 2005
It is known that random k-SAT instances with at least $cn$ clauses, where $c = obreak c_k$ 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^{k-1}/(\log n)^{k-2}$ clauses can be certified unsatisfiable in polynomial time. We employ spectral methods to improve on this bound. For even $k\ge 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 $n^{3/2+\varepsilon}$ clauses, where $\varepsilon >0$ is an arbitrary constant.