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). We consider the problem to certify efficiently the unsatisfiability of such formulas. A result of Beame et al. show that k-SAT instances with at least n^(k-1)/log(n) clauses can be certified unsatisfiable in polynomial time. We employ spectral methods to improve on this: We present a polynomial time algorithm which certifies random k-SAT instances with at least 2^k * (k/2)^7 * (ln(n))^7 * n^(k/2) clauses as unsatisfiable (with high probability).

This is joint work with M. Krivelevich from Tel Aviv University.

Host: Klaus Meer