A generalized method for proving polynomial calculus degree lower bounds
2015 (English)In: Leibniz International Proceedings in Informatics, LIPIcs, Dagstuhl Publishing , 2015, Vol. 33, 467-487 p.Conference paper (Refereed)Text
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.
Place, publisher, year, edition, pages
Dagstuhl Publishing , 2015. Vol. 33, 467-487 p.
Degree, Functional pigeonhole principle, Lower bound, PCR, Polynomial calculus, Polynomial calculus resolution, Proof complexity, Size
IdentifiersURN: urn:nbn:se:kth:diva-187389DOI: 10.4230/LIPIcs.CCC.2015.467ScopusID: 2-s2.0-84958256296ISBN: 978-393989781-1OAI: oai:DiVA.org:kth-187389DiVA: diva2:931257
30th Conference on Computational Complexity, CCC 2015; Portland; United States
QC 201605272016-05-272016-05-232016-05-27Bibliographically approved