A generalized method for proving polynomial calculus degree lower bounds
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
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.
Original language | English |
---|---|
Title of host publication | 30th Conference on Computational Complexity, CCC 2015 |
Editors | David Zuckerman |
Number of pages | 21 |
Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
Publication date | 1 Jun 2015 |
Pages | 467-487 |
ISBN (Electronic) | 9783939897811 |
DOIs | |
Publication status | Published - 1 Jun 2015 |
Externally published | Yes |
Event | 30th Conference on Computational Complexity, CCC 2015 - Portland, United States Duration: 17 Jun 2015 → 19 Jun 2015 |
Conference
Conference | 30th Conference on Computational Complexity, CCC 2015 |
---|---|
Land | United States |
By | Portland |
Periode | 17/06/2015 → 19/06/2015 |
Sponsor | Microsoft Research |
Series | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
Volume | 33 |
ISSN | 1868-8969 |
- Degree, Functional pigeonhole principle, Lower bound, PCR, Polynomial calculus, Polynomial calculus resolution, Proof complexity, Size
Research areas
ID: 251869007