2026-07-20T10:41:58Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5077 2024-03-06T10:35:48Z ddc:004 open_access

A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds Miksa, Mladen Nordström, Jakob proof complexity polynomial calculus polynomial calculus resolution PCR degree size functional pigeonhole principle lower bound We study the problem of establishing 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mladen Miksa and Jakob Nordström 2015 Is Part Of LIPIcs, Volume 33, 30th Conference on Computational Complexity (CCC 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CCC.2015.467 urn:nbn:de:0030-drops-50775 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2015.467 eng https://creativecommons.org/licenses/by/3.0/legalcode