Polynomial calculus space and resolution width
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F25%3A00639752" target="_blank" >RIV/67985840:_____/25:00639752 - isvavai.cz</a>
Result on the web
<a href="http://doi.org/10.4086/toc.2025.v021a006" target="_blank" >http://doi.org/10.4086/toc.2025.v021a006</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.4086/toc.2025.v021a006" target="_blank" >10.4086/toc.2025.v021a006</a>
Alternative languages
Result language
angličtina
Original language name
Polynomial calculus space and resolution width
Original language description
We show that if a k-CNF requires width w to refute in resolution, then it requires space root w to refute in polynomial calculus, where the space of a polynomial calculus refutation is the number of monomials that must be kept in memory when working through the proof. This is the first analogue, in polynomial calculus, of Atserias and Dalmau's result that, in resolution, width is a lower bound on clause space. As a by-product of our new approach to space lower bounds we give a simple proof of Bonacina's recent result that total space in resolution (the total number of variable occurrences that must be kept in memory) is at least the width squared. As corollaries of the main result we obtain some new lower bounds on the PCR space needed to refute specific formulas, as well as partial answers to some open problems about relations between space, size, and degree for polynomial calculus.
Czech name
—
Czech description
—
Classification
Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10101 - Pure mathematics
Result continuities
Project
<a href="/en/project/GA23-04825S" target="_blank" >GA23-04825S: Logic and unsatisfiability</a><br>
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2025
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Theory of Computing
ISSN
1557-2862
e-ISSN
1557-2862
Volume of the periodical
21
Issue of the periodical within the volume
September
Country of publishing house
US - UNITED STATES
Number of pages
29
Pages from-to
6
UT code for WoS article
001572856900001
EID of the result in the Scopus database
2-s2.0-105019799881