@inproceedings{3fbb654bfa154aa8940f9ce1af87d91e,
title = "A generalized method for proving polynomial calculus degree lower bounds",
abstract = "We study the problem of obtaining lower bounds for polynomial calculus (PC) and polynomial calculus resolution (PCR) on proof degree, and hence by [Impagliazzo et al. '99] also on proof size. [Alekhnovich and Razborov'03] established that if the clause-variable incidence graph of a CNF formula F is a good enough expander, then proving that F is unsatisfiable requires high PC/PCR degree. We further develop the techniques in [AR03] 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. As a corollary of this, we prove that the functional pigeonhole principle (FPHP) formulas require high PC/PCR degree when restricted to constant-degree expander graphs. This answers an open question in [Razborov'02], and also implies that the standard CNF encoding of the FPHP formulas require exponential proof size in polynomial calculus resolution. Thus, while Onto-FPHP formulas are easy for polynomial calculus, as shown in [Riis'93], both FPHP and Onto-PHP formulas are hard even when restricted to bounded-degree expanders.",
keywords = "Degree, Functional pigeonhole principle, Lower bound, PCR, Polynomial calculus, Polynomial calculus resolution, Proof complexity, Size",
author = "Mladen Mik{\v s}a and Jakob Nordstr{\"o}m",
year = "2015",
month = jun,
day = "1",
doi = "10.4230/LIPIcs.CCC.2015.467",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",
pages = "467--487",
editor = "David Zuckerman",
booktitle = "30th Conference on Computational Complexity, CCC 2015",
note = "30th Conference on Computational Complexity, CCC 2015 ; Conference date: 17-06-2015 Through 19-06-2015",
}