Strong refutation heuristics for random k-SAT

Abstract

A simple first moment argument shows that in a randomly chosen k-SAT formula with m clauses over n boolean variables, the fraction of satisfiable clauses is at most 1-2-k + o(1) as m/n → ∞ almost surely.In this paper, we deal with the corresponding algorithmic strong refutation problem: given a random k-SAT formula, can we find a certificate that the fraction of satisfiable clauses is at most 1-2-k + o(1) in polynomial time? We present heuristics based on spectral techniques that in the case k = 3, m ≥ In(n)6n3/2 and in the case k = 4, m ≥ Cn2 find such certificates almost surely, where C denotes a constant. Our methods also apply to some hypergraph problems. © Springer-Verlag 2004.