Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Some trade-off results for polynomial calculus
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-2700-4285
2013 (English)In: STOC '13 Proceedings of the 45th annual ACM symposium on Symposium on theory of computing, Association for Computing Machinery (ACM), 2013, 813-822 p.Conference paper, Published paper (Refereed)
Abstract [en]

We present size-space trade-offs for the polynomial calculus (PC) and polynomial calculus resolution (PCR) proof systems. These are the first true size-space trade-offs in any algebraic proof system, showing that size and space cannot be simultaneously optimized in these models. We achieve this by extending essentially all known size-space trade-offs for resolution to PC and PCR. As such, our results cover space complexity from constant all the way up to exponential and yield mostly superpolynomial or even exponential size blow-ups. Since the upper bounds in our trade-offs hold for resolution, our work shows that there are formulas for which adding algebraic reasoning on top of resolution does not improve the trade-off properties in any significant way. As byproducts of our analysis, we also obtain trade-offs between space and degree in PC and PCR exactly matching analogous results for space versus width in resolution, and strengthen the resolution trade-offs in [Beame, Beck, and Impagliazzo '12] to apply also to k-CNF formulas.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2013. 813-822 p.
Series
Proceedings of the Annual ACM Symposium on Theory of Computing, ISSN 0737-8017
Keyword [en]
Degree, PCR, Pebble games, Pebbling formulas, Polynomial calculus, Proof complexity, Resolution, Size, Space, Trade-offs, Tseitin formulas
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:kth:diva-134132DOI: 10.1145/2488608.2488711Scopus ID: 2-s2.0-84879820217ISBN: 978-145032029-0 (print)OAI: oai:DiVA.org:kth-134132DiVA: diva2:665184
Conference
45th Annual ACM Symposium on Theory of Computing, STOC 2013; Palo Alto, CA; United States; 1 June 2013 through 4 June 2013
Note

QC 20131119

Available from: 2013-11-19 Created: 2013-11-18 Last updated: 2013-11-19Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Nordström, Jakob

Search in DiVA

By author/editor
Nordström, Jakob
By organisation
Theoretical Computer Science, TCS
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 36 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf