Abstract
How hard is it to give short, efficiently verifiable certificates that formulas in conjunctive normal form (CNF) are unsatisfiable, i.e., that
any truth value assignment to the variables must falsify at least one clause? This question is the focus of proof complexity, and a rich body of work has developed ingenious, highly intricate methods for proving strong lower bounds for a variety of different proof systems.
In this talk, we present a simple way to prove optimal, exponential lower bounds on proof size --- without even knowing any proof complexity! --- for two well-studied proof systems, namely resolution and polynomial calculus. Given a CNF formula, it is enough to construct a bipartite graph on the clauses and variables such that (a) this graph is an expander (i.e., is very well-connected) and (b) there is a winning strategy in a simple 2-player game played on any edge. This also gives a unified view of resolution and polynomial calculus lower bounds in that the only difference between the two proof systems is which player moves first in the game.
Using this method (which relies heavily on techniques developed in [Ben-Sasson and Wigderson '01] and [Alekhnovich and Razborov '03]), we prove that the functional pigeonhole principle (FPHP) formulas are hard for polynomial calculus, answering an open question in [Razborov '02]. Building on this, we construct k-colouring instances which require polynomial calculus proofs of linear degree, and hence exponential size. This implies a linear degree lower bound for Gröbner basis algorithms, as well as for the algorithm studied in a sequence of papers [De Loera et al. 08, '09, '11, '15] based on Hilbert's Nullstellensatz proofs, thus resolving an open problem mentioned, e.g., in [De Loera et al. '09] and [Li et al. '16].
Based on joint work with Massimo Lauria and Mladen Miksa.