Random instances of 3SAT are known to be unsatisfiable with high probability when there at least $5N$ clauses. However, given a random 3SAT instance on $N$ variables, the task of refuting the instance, or of certifying that the instance has no satisfying assignments, is hypothesized to be computationally hard if there are $O(N)$ clauses—in fact, the best known efficient algorithms for refutation require instances with at least $N^{3/2}$ clauses, a factor of $N^{1/2}$ beyond the unsatisfiability threshold.

In this talk, I will describe a new spectral algorithm that refutes 3SAT instances with fewer clauses, given more time. Our algorithm extends the best polynomial time algorithms at $N^{3/2}$ clauses, interpolating between them and the exponential brute-force search at the unsatisfiability threshold at $\Theta(N)$ clauses. Further, our algorithm strongly refutes the instances, certifying that no assignment satisfies more than a $(7/8)$-fraction of constraints.