It is known that random k-SAT instances with at least cn clauses where c = c{sub}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. shows that k-SAT instances with at least n{sup}(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 for k even with at least 2{sup}k·(k/2){sup}7·(ln n){sup}7·n{sup}(k/2) = n{sup}((k/2)+o(1)) clauses as unsatisfiable (with high probability).
展开▼
