How difficult is it to certify that a random 3SAT formula is unsatisfiable?

The Satisfiability problem is perhaps the most famous problem in theoretical computer science, and significant effort has been devoted to understanding randomly generated SAT instances. The random k-SAT model (where a random k-CNF formula is chosen by uniformly selecting m clauses from the set of all possible clauses on k distinct variables) is important for several reasons. First, it is an intrinsically natural model analogous to random graph models, and closely related to phase transitions and structural phenomena occurring in statistical physics. Thus like random graph models, understanding the complexity of random SAT sheds light on fundamental structural properties of the satisfiability problem. Secondly, the random k-SAT distribution gives us a testbench of empirically hard examples which are useful for comparing and analyzing SAT algorithms. Third, the difficulty of certifying the unsatisfiability of a random k-SAT formula is connected to several other central questions in complexity theory, including the complexity of approximately solving NP-hard problems, and the complexity of learning DNF formulas.

We will first review the fascinating world of random structured distributions (k-SAT, k-CSP and random graph models), their threshold properties, empirical and theoretical results and conjectures about their complexity and structural properties. We then focus on the following question: how difficult is it to certify that a given random k-SAT formula is unsatisfiable (for a given proof system)? The current state of affairs is perplexing. On the one hand, Chvatal and Szemeredi famously proved exponential lower bounds for Resolution refutations of random k-SAT, and more recently similar exponential lower bounds have been shown for SOS (Sum-of-Squares) and Cutting Planes refutations. Taken together these lower bounds prove that most state-of-the-art algorithms will require exponential-time on random k-SAT instances. On the other hand, current algorithms are unreasonably effective at solving random k-SAT instances! We will sketch the lower bound proofs for Resolution and the recent lower bound for Cutting Planes refutations for random formulas, and discuss the interesting web of connections between the sunflower lemma in extremal combinatorics, threshold properties of random structures, proof complexity lower bounds, and circuit lower bounds.