Some trade-off results for polynomial calculus

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Standard

Some trade-off results for polynomial calculus. / Beck, Chris; Nordström, Jakob; Tang, Bangsheng.

STOC 2013 - Proceedings of the 2013 ACM Symposium on Theory of Computing. 2013. p. 813-822 (Proceedings of the Annual ACM Symposium on Theory of Computing).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Harvard

Beck, C, Nordström, J & Tang, B 2013, Some trade-off results for polynomial calculus. in STOC 2013 - Proceedings of the 2013 ACM Symposium on Theory of Computing. Proceedings of the Annual ACM Symposium on Theory of Computing, pp. 813-822, 45th Annual ACM Symposium on Theory of Computing, STOC 2013, Palo Alto, CA, United States, 01/06/2013. https://doi.org/10.1145/2488608.2488711

APA

Beck, C., Nordström, J., & Tang, B. (2013). Some trade-off results for polynomial calculus. In STOC 2013 - Proceedings of the 2013 ACM Symposium on Theory of Computing (pp. 813-822). Proceedings of the Annual ACM Symposium on Theory of Computing https://doi.org/10.1145/2488608.2488711

Vancouver

Beck C, Nordström J, Tang B. Some trade-off results for polynomial calculus. In STOC 2013 - Proceedings of the 2013 ACM Symposium on Theory of Computing. 2013. p. 813-822. (Proceedings of the Annual ACM Symposium on Theory of Computing). https://doi.org/10.1145/2488608.2488711

Author

Beck, Chris ; Nordström, Jakob ; Tang, Bangsheng. / Some trade-off results for polynomial calculus. STOC 2013 - Proceedings of the 2013 ACM Symposium on Theory of Computing. 2013. pp. 813-822 (Proceedings of the Annual ACM Symposium on Theory of Computing).

Bibtex

@inproceedings{0069b5c761014a09a2d12d885a6d6d47,
title = "Some trade-off results for polynomial calculus",
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 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.",
keywords = "Degree, PCR, Pebble games, Pebbling formulas, Polynomial calculus, Proof complexity, Resolution, Size, Space, Trade-offs, Tseitin formulas",
author = "Chris Beck and Jakob Nordstr{\"o}m and Bangsheng Tang",
year = "2013",
doi = "10.1145/2488608.2488711",
language = "English",
isbn = "9781450320290",
series = "Proceedings of the Annual ACM Symposium on Theory of Computing",
publisher = "Association for Computing Machinery (ACM)",
pages = "813--822",
booktitle = "STOC 2013 - Proceedings of the 2013 ACM Symposium on Theory of Computing",
note = "45th Annual ACM Symposium on Theory of Computing, STOC 2013 ; Conference date: 01-06-2013 Through 04-06-2013",

}

RIS

TY - GEN

T1 - Some trade-off results for polynomial calculus

AU - Beck, Chris

AU - Nordström, Jakob

AU - Tang, Bangsheng

PY - 2013

Y1 - 2013

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

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

KW - Degree

KW - PCR

KW - Pebble games

KW - Pebbling formulas

KW - Polynomial calculus

KW - Proof complexity

KW - Resolution

KW - Size

KW - Space

KW - Trade-offs

KW - Tseitin formulas

UR - http://www.scopus.com/inward/record.url?scp=84879820217&partnerID=8YFLogxK

U2 - 10.1145/2488608.2488711

DO - 10.1145/2488608.2488711

M3 - Article in proceedings

AN - SCOPUS:84879820217

SN - 9781450320290

T3 - Proceedings of the Annual ACM Symposium on Theory of Computing

SP - 813

EP - 822

BT - STOC 2013 - Proceedings of the 2013 ACM Symposium on Theory of Computing

T2 - 45th Annual ACM Symposium on Theory of Computing, STOC 2013

Y2 - 1 June 2013 through 4 June 2013

ER -

ID: 251870197