A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds

We study the problem of certifying unsatisfiability of formulas in propositional logic. For proof systems such as resolution and polynomial calculus it is known that if the clause-variable incidence graph of a CNF formula is an expander (i.e., is very well-connected), then proving that this formula is unsatisfiable is hard. We further develop techniques in [Alekhnovich and Razborov '03] to show that if one can "cluster" clauses and variables in a way that "respects the structure" of the formula in a certain sense, then it is sufficient that the incidence graph of this clustered version is an expander. We also give a unified view of resolution and polynomial calculus lower bounds in terms of a 2-player game played on this graph, where the difference between resolution and polynomial calculus is just in which player has to go first. As a corollary, we prove that the functional pigeonhole principle (FPHP) formulas are hard for polynomial calculus, answering an open question in [Razborov '02].