Some trade-off results for polynomial calculus
(2013) 45th Annual ACM Symposium on Theory of Computing, STOC 2013 In Proceedings of the Annual ACM Symposium on Theory of Computing p.813-822- Abstract
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... (More)
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.
(Less)
- author
- Beck, Chris ; Nordström, Jakob LU and Tang, Bangsheng
- publishing date
- 2013
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- keywords
- Degree, PCR, Pebble games, Pebbling formulas, Polynomial calculus, Proof complexity, Resolution, Size, Space, Trade-offs, Tseitin formulas
- host publication
- STOC 2013 - Proceedings of the 2013 ACM Symposium on Theory of Computing
- series title
- Proceedings of the Annual ACM Symposium on Theory of Computing
- pages
- 10 pages
- publisher
- Association for Computing Machinery (ACM)
- conference name
- 45th Annual ACM Symposium on Theory of Computing, STOC 2013
- conference location
- Palo Alto, CA, United States
- conference dates
- 2013-06-01 - 2013-06-04
- external identifiers
-
- scopus:84879820217
- ISSN
- 0737-8017
- ISBN
- 9781450320290
- DOI
- 10.1145/2488608.2488711
- language
- English
- LU publication?
- no
- id
- 41bc78ce-8327-40a3-9b9c-9e46124d150d
- date added to LUP
- 2020-12-18 22:25:52
- date last changed
- 2022-04-11 06:31:47
@inproceedings{41bc78ce-8327-40a3-9b9c-9e46124d150d,
abstract = {{<p>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.</p>}},
author = {{Beck, Chris and Nordström, Jakob and Tang, Bangsheng}},
booktitle = {{STOC 2013 - Proceedings of the 2013 ACM Symposium on Theory of Computing}},
isbn = {{9781450320290}},
issn = {{0737-8017}},
keywords = {{Degree; PCR; Pebble games; Pebbling formulas; Polynomial calculus; Proof complexity; Resolution; Size; Space; Trade-offs; Tseitin formulas}},
language = {{eng}},
pages = {{813--822}},
publisher = {{Association for Computing Machinery (ACM)}},
series = {{Proceedings of the Annual ACM Symposium on Theory of Computing}},
title = {{Some trade-off results for polynomial calculus}},
url = {{http://dx.doi.org/10.1145/2488608.2488711}},
doi = {{10.1145/2488608.2488711}},
year = {{2013}},
}