Polynomial calculus space and resolution width
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F19%3A00518434" target="_blank" >RIV/67985840:_____/19:00518434 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1109/FOCS.2019.00081" target="_blank" >http://dx.doi.org/10.1109/FOCS.2019.00081</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1109/FOCS.2019.00081" target="_blank" >10.1109/FOCS.2019.00081</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Polynomial calculus space and resolution width
Popis výsledku v původním jazyce
We show that if a k-CNF requires width w to refute in resolution, then it requires space √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 lower-bounding clause space in resolution by resolution width. 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 lower-bounded by 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.
Název v anglickém jazyce
Polynomial calculus space and resolution width
Popis výsledku anglicky
We show that if a k-CNF requires width w to refute in resolution, then it requires space √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 lower-bounding clause space in resolution by resolution width. 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 lower-bounded by 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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
—
OECD FORD obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Návaznosti výsledku
Projekt
<a href="/cs/project/GA19-05497S" target="_blank" >GA19-05497S: Složitost matematických důkazů a struktur</a><br>
Návaznosti
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Ostatní
Rok uplatnění
2019
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
60th Annual Symposium on Foundations of Computer Science (FOCS)
ISBN
978-1-7281-4952-3
ISSN
0272-5428
e-ISSN
—
Počet stran výsledku
13
Strana od-do
1325-1337
Název nakladatele
IEEE
Místo vydání
Piscataway
Místo konání akce
Baltimore
Datum konání akce
9. 11. 2019
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
000510015300072