Change search
ReferencesLink to record
Permanent link

Direct link
A generalized method for proving polynomial calculus degree lower bounds
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-2700-4285
2015 (English)In: Leibniz International Proceedings in Informatics, LIPIcs, Dagstuhl Publishing , 2015, Vol. 33, 467-487 p.Conference paper (Refereed)Text
Abstract [en]

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.
Keyword [en]
Degree, Functional pigeonhole principle, Lower bound, PCR, Polynomial calculus, Polynomial calculus resolution, Proof complexity, Size
National Category
Mathematical Analysis
Identifiers
URN: 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
Conference
30th Conference on Computational Complexity, CCC 2015; Portland; United States
Note

QC 20160527

Available from: 2016-05-27 Created: 2016-05-23 Last updated: 2016-05-27Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Mikša, MladenNordström, Jakob
By organisation
Theoretical Computer Science, TCS
Mathematical Analysis

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 1 hits
ReferencesLink to record
Permanent link

Direct link