Polynomial calculus space and resolution width

Kód výsledku v 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>

Výsledek na webu

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

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

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

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10101 - Pure mathematics

Projekt

<a href="/cs/project/GA23-04825S" target="_blank" >GA23-04825S: Logika a nesplnitelnost</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2025

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ů

Název periodika

Theory of Computing

ISSN

1557-2862

e-ISSN

1557-2862

Svazek periodika

21

Číslo periodika v rámci svazku

September

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

29

Strana od-do

6

Kód UT WoS článku

001572856900001

EID výsledku v databázi Scopus

2-s2.0-105019799881