Miksa, Mladen ;
Nordström, Jakob
A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds
Abstract
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 clausevariable 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 constantdegree 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.
BibTeX  Entry
@InProceedings{miksa_et_al:LIPIcs:2015:5077,
author = {Mladen Miksa and Jakob Nordstr{\"o}m},
title = {{A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds}},
booktitle = {30th Conference on Computational Complexity (CCC 2015)},
pages = {467487},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897811},
ISSN = {18688969},
year = {2015},
volume = {33},
editor = {David Zuckerman},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5077},
URN = {urn:nbn:de:0030drops50775},
doi = {10.4230/LIPIcs.CCC.2015.467},
annote = {Keywords: proof complexity, polynomial calculus, polynomial calculus resolution, PCR, degree, size, functional pigeonhole principle, lower bound}
}
2015
Keywords: 

proof complexity, polynomial calculus, polynomial calculus resolution, PCR, degree, size, functional pigeonhole principle, lower bound 
Seminar: 

30th Conference on Computational Complexity (CCC 2015)

Issue date: 

2015 
Date of publication: 

2015 