During the last decade, an active line of research in proof complexity has been into the space complexity of proofs and how space is related to other measures. By now these aspects of resolution are fairly well understood, but many open problems remain for the related but stronger polynomial calculus (PC/PCR) proof system. For instance, the space complexity of many standard “benchmark formulas” is still open, as well as the relation of space to size and degree in PC/PCR. We prove that if a formula requires large resolution width, then making XOR substitution yields a formula requiring large PCR space, providing some circumstantial evidence that degree might be a lower bound for space. More importantly, this immediately yields formulas that are very hard for space but very easy for size, exhibiting a size-space separation similar to what is known for resolution. Using related ideas, we show that if a graph has good expansion and in addition its edge set can be partitioned into short cycles, then the Tseitin formula over this graph requires large PCR space. In particular, Tseitin formulas over random 4-regular graphs almost surely require space at least Ω√ . Our proofs use techniques recently introduced in [Bonacina-Galesi ’13]. Our final contribution, however, is to show that these techniques provably cannot yield non-constant space lower bounds for the functional pigeonhole principle, delineating the limitations of this framework and suggesting that we are still far from characterizing PC/PCR space.

Towards an understanding of polynomial calculus: New separations and lower bounds (extended abstract) / Filmus, Yuval; Lauria, Massimo; Mikša, Mladen; Nordström, Jakob; Vinyals, Marc. - 7965:(2013), pp. 437-448. (Intervento presentato al convegno 40th International Colloquium on Automata, Languages, and Programming, ICALP 2013 tenutosi a Riga, lva nel 2013) [10.1007/978-3-642-39206-1_37].

Towards an understanding of polynomial calculus: New separations and lower bounds (extended abstract)

LAURIA, MASSIMO;
2013

Abstract

During the last decade, an active line of research in proof complexity has been into the space complexity of proofs and how space is related to other measures. By now these aspects of resolution are fairly well understood, but many open problems remain for the related but stronger polynomial calculus (PC/PCR) proof system. For instance, the space complexity of many standard “benchmark formulas” is still open, as well as the relation of space to size and degree in PC/PCR. We prove that if a formula requires large resolution width, then making XOR substitution yields a formula requiring large PCR space, providing some circumstantial evidence that degree might be a lower bound for space. More importantly, this immediately yields formulas that are very hard for space but very easy for size, exhibiting a size-space separation similar to what is known for resolution. Using related ideas, we show that if a graph has good expansion and in addition its edge set can be partitioned into short cycles, then the Tseitin formula over this graph requires large PCR space. In particular, Tseitin formulas over random 4-regular graphs almost surely require space at least Ω√ . Our proofs use techniques recently introduced in [Bonacina-Galesi ’13]. Our final contribution, however, is to show that these techniques provably cannot yield non-constant space lower bounds for the functional pigeonhole principle, delineating the limitations of this framework and suggesting that we are still far from characterizing PC/PCR space.
2013
40th International Colloquium on Automata, Languages, and Programming, ICALP 2013
theoretical computer science; computer science; polynomial calculus
04 Pubblicazione in atti di convegno::04b Atto di convegno in volume
Towards an understanding of polynomial calculus: New separations and lower bounds (extended abstract) / Filmus, Yuval; Lauria, Massimo; Mikša, Mladen; Nordström, Jakob; Vinyals, Marc. - 7965:(2013), pp. 437-448. (Intervento presentato al convegno 40th International Colloquium on Automata, Languages, and Programming, ICALP 2013 tenutosi a Riga, lva nel 2013) [10.1007/978-3-642-39206-1_37].
File allegati a questo prodotto
File Dimensione Formato  
Filmus_copertina_Towards-an-understanding_2013.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 1.37 MB
Formato Unknown
1.37 MB Unknown   Contatta l'autore
Filmus_indice_Towards-an-understanding_2013.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 72.77 kB
Formato Unknown
72.77 kB Unknown   Contatta l'autore
Filmus_Towards-an-understanding_2013.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 175.86 kB
Formato Adobe PDF
175.86 kB Adobe PDF   Contatta l'autore

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/957567
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 22
  • ???jsp.display-item.citation.isi??? 19
social impact