School of Technology and Computer Science Seminars
A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds
by Jakob Nordstrom (KTH Royal Institute of Technology, Sweden)
Tuesday, February 21, 2017
from
to
(Asia/Kolkata)
at A-201 (STCS Seminar Room)
at A-201 (STCS Seminar Room)
Description |
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]. |