Paper Info
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.
Year
DOI
Venue
2015
10.4230/LIPIcs.CCC.2015.467
Electronic Colloquium on Computational Complexity (ECCC)
Keywords
Field
DocType
Proof complexity,polynomial calculus,polynomial calculus resolution,PCR,degree,size,functional pigeonhole principle,lower bound
Discrete mathematics,Combinatorics,Expander graph,Exponential function,Upper and lower bounds,Degree of a polynomial,Matrix polynomial,Proof complexity,Corollary,Mathematics,Pigeonhole principle
Journal
Volume
ISSN
Citations 
22
1868-8969
5
PageRank 
References 
Authors
0.38
23
2
Name
Order
Citations
PageRank
Mladen Miksa1191.98
Jakob Nordström217721.76