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].
