Refuting Smoothed k-SAT Formulas and a Proof of Feige's Conjecture

I'll present a new algorithm to refute, that is, efficiently find certificates of unsatisfiability, for smoothed instances of k-SAT and other CSPs. Smoothed instances are produced by starting with a worst-case instance and flipping each literal in every clause independently with a small constant probability. The "clause" structure in such instances is arbitrary and the only randomness is in the literal patterns. The trade-off between the density, i.e., the number of constraints in the instance and the running time required by the algorithm matches (up to polylogarithmic factors density) the best known (and possibly sharp) trade-off for random k-SAT. As a corollary, we also obtain a simpler analysis for refuting random k-SAT formulas.

Our analysis inspires a new method that we use to prove Feige's 2008 conjecture on the trade-off between the size of the hypergraph and its girth that generalizes the Moore bound on the girth of irregular graphs proved by Alon, Hoory, and Linial (2002). As a corollary, we obtain that smoothed instances of 3-sat with arbitrary clause structure and ~n^{1.4} (<< n^{1.5}, the threshold for known efficient refutation) constraints admit polynomial-size certificates of unsatisfiability with appropriate generalization to all k-CSPs. This extends the celebrated work of Feige, Kim, and Ofek (2006) who proved a similar result for random 3-sat. FKO's proof uses a 2nd-moment-method based argument that strongly exploits the randomness of the clause structure. Our proof gives a simpler argument that extends to ``worst-case" clause structures. 

Taken together, our results show that smoothed instances with arbitrary clause structure and considerably less randomness enjoy the same thresholds for both refutation algorithms and certificates of unsatisfiability as random instances.

Based on joint work with Venkat Guruswami (CMU/Berkeley) and Peter Manohar (CMU).