A generalized method for proving polynomial calculus degree lower bounds

Forskningsoutput: Kapitel i bok/rapport/Conference proceedingKonferenspaper i proceeding

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.

Detaljer

Författare
Externa organisationer
  • KTH Royal Institute of Technology
Forskningsområden

Ämnesklassifikation (UKÄ) – OBLIGATORISK

  • Datavetenskap (datalogi)

Nyckelord

Originalspråkengelska
Titel på värdpublikation30th Conference on Computational Complexity, CCC 2015
RedaktörerDavid Zuckerman
FörlagSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Sidor467-487
Antal sidor21
ISBN (elektroniskt)9783939897811
StatusPublished - 2015 jun 1
PublikationskategoriForskning
Peer review utfördJa
Externt publiceradJa
Evenemang30th Conference on Computational Complexity, CCC 2015 - Portland, USA
Varaktighet: 2015 jun 172015 jun 19

Publikationsserier

NamnLeibniz International Proceedings in Informatics, LIPIcs
FörlagSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Volym33
ISSN (tryckt)1868-8969

Konferens

Konferens30th Conference on Computational Complexity, CCC 2015
LandUSA
OrtPortland
Period2015/06/172015/06/19