Towards an Understanding of Polynomial Calculus : New Separations and Lower Bounds
(2025) In Theory of Computing 21.- Abstract
During the last two decades, 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 the resolution proof system are fairly well understood, but many open problems remain for the related but stronger proof system polynomial calculus (PC/PCR). 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 (and hence also PC space), providing some circumstantial evidence that degree might be a lower bound for space. More... (More)
During the last two decades, 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 the resolution proof system are fairly well understood, but many open problems remain for the related but stronger proof system polynomial calculus (PC/PCR). 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 (and hence also PC 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 if 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 Ω(√n). Our proofs use techniques introduced by Bonacina and Galesi (ITCS'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.
(Less)
- author
- Filmus, Yuval ; Lauria, Massimo ; Mikša, Mladen ; Nordström, Jakob LU and Vinyals, Marc
- organization
- publishing date
- 2025
- type
- Contribution to journal
- publication status
- published
- subject
- keywords
- degree, polynomial calculus, proof complexity, separations, size, space
- in
- Theory of Computing
- volume
- 21
- article number
- v021a004
- external identifiers
-
- scopus:105017428527
- DOI
- 10.4086/toc.2025.v021a004
- language
- English
- LU publication?
- yes
- id
- 27dfa428-ab8f-4630-aff6-bfba77b4f243
- date added to LUP
- 2025-12-08 10:55:39
- date last changed
- 2025-12-08 10:56:44
@article{27dfa428-ab8f-4630-aff6-bfba77b4f243,
abstract = {{<p>During the last two decades, 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 the resolution proof system are fairly well understood, but many open problems remain for the related but stronger proof system polynomial calculus (PC/PCR). 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 (and hence also PC 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 if 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 Ω(√n). Our proofs use techniques introduced by Bonacina and Galesi (ITCS'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.</p>}},
author = {{Filmus, Yuval and Lauria, Massimo and Mikša, Mladen and Nordström, Jakob and Vinyals, Marc}},
keywords = {{degree; polynomial calculus; proof complexity; separations; size; space}},
language = {{eng}},
series = {{Theory of Computing}},
title = {{Towards an Understanding of Polynomial Calculus : New Separations and Lower Bounds}},
url = {{http://dx.doi.org/10.4086/toc.2025.v021a004}},
doi = {{10.4086/toc.2025.v021a004}},
volume = {{21}},
year = {{2025}},
}