Richard M. Karp Distinguished Lecture — How Difficult Is It to Certify That a Random SAT 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 instances 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, and empirical and theoretical results and conjectures about their structure and complexity. 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!

Lastly, we reflect on the lower bound proofs (in particular the recent lower bound for Cutting Planes refutations) which reveal an interesting web of connections between sunflower lemmas in extremal combinatorics, threshold properties of random structures, proof complexity lower bounds, and circuit lower bounds.

If you require accommodation for communication, please contact our Access Coordinator at simonsevents@berkeley.edu with as much advance notice as possible.