License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CCC.2015.467
URN: urn:nbn:de:0030-drops-50775
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5077/
Go to the corresponding LIPIcs Volume Portal

Miksa, Mladen ; Nordström, Jakob

A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds

pdf-format:
29.pdf (0.5 MB)

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 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.

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 =	{467--487},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-81-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{33},
  editor =	{David Zuckerman},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5077},
  URN =		{urn:nbn:de:0030-drops-50775},
  doi =		{10.4230/LIPIcs.CCC.2015.467},
  annote =	{Keywords: proof complexity, polynomial calculus, polynomial calculus resolution, PCR, degree, size, functional pigeonhole principle, lower bound}
}

Keywords: proof complexity, polynomial calculus, polynomial calculus resolution, PCR, degree, size, functional pigeonhole principle, lower bound
Collection: 30th Conference on Computational Complexity (CCC 2015)
Issue Date: 2015
Date of publication: 06.06.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI