Abstract: Determining unsatisfiability of a k-SAT instance with n variables and m clauses is NP-hard in the worst case, but can be done efficiently for average case, random instances provided that the density of clauses m/n is above the "spectral threshold" of n^(k/2 - 1). More generally, for random Boolean CSPs there is a known time-density trade-off for which certifying unsatisfiability is possible, and this trade-off is moreover tight for SDP-based algorithms.

We present an algorithm for certifying the unsatisfiability of smoothed instances of all Boolean CSPs. The smoothed model is a hybrid between worst and average case inputs, where the input is an arbitrary instance of the CSP with only the negation patterns of the literals re-randomized with some small, constant probability. Our algorithm achieves, for smoothed instances, the same optimal time-density trade-off as for random instances, thus showing that smoothed instances are no harder than fully random ones.

We also make a surprising new connection between our algorithm and even covers in hypergraphs, which we use to positively resolve Feige's 2008 conjecture, an extremal combinatorics conjecture on the existence of even covers in sufficiently dense hypergraphs that generalizes the well-known Moore bound for the girth of graphs. As a corollary, we show that polynomial-size refutation witnesses exist for arbitrary semi-random CSP instances at clause densities a polynomial factor below the "spectral threshold" of n^(k/2 - 1), simplifying and extending the celebrated result for random 3-SAT of Feige, Kim and Ofek.

Joint work with Venkatesan Guruswami and Pravesh K. Kothari.