Cops-Robber games and the resolution of Tseitin formulas

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F20%3A00523857" target="_blank" >RIV/67985840:_____/20:00523857 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1145/3378667" target="_blank" >https://doi.org/10.1145/3378667</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/3378667" target="_blank" >10.1145/3378667</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Cops-Robber games and the resolution of Tseitin formulas

Popis výsledku v původním jazyce

We characterize several complexity measures for the resolution of Tseitin formulas in terms of a two person cop-robber game. Our game is a slight variation of the one Seymour and Thomas used in order to characterize the tree-width parameter. For any undirected graph, by counting the number of cops needed in our game in order to catch a robber in it, we are able to exactly characterize the width, variable space, and depth measures for the resolution of the Tseitin formula corresponding to that graph. We also give an exact game characterization of resolution variable space for any formula.nWe show that our game can be played in a monotone way. This implies that the associated resolution measures on Tseitin formulas correspond exactly to those under the restriction of Davis-Putnam resolution, implying that this kind of resolution is optimal on Tseitin formulas for all the considered measures.nUsing our characterizations, we improve the existing complexity bounds for Tseitin formulas showing that resolution width, depth, and variable space coincide up to a logarithmic factor, and that variable space is bounded by the clause space times a logarithmic factor.n

Název v anglickém jazyce

Cops-Robber games and the resolution of Tseitin formulas

Popis výsledku anglicky

We characterize several complexity measures for the resolution of Tseitin formulas in terms of a two person cop-robber game. Our game is a slight variation of the one Seymour and Thomas used in order to characterize the tree-width parameter. For any undirected graph, by counting the number of cops needed in our game in order to catch a robber in it, we are able to exactly characterize the width, variable space, and depth measures for the resolution of the Tseitin formula corresponding to that graph. We also give an exact game characterization of resolution variable space for any formula.nWe show that our game can be played in a monotone way. This implies that the associated resolution measures on Tseitin formulas correspond exactly to those under the restriction of Davis-Putnam resolution, implying that this kind of resolution is optimal on Tseitin formulas for all the considered measures.nUsing our characterizations, we improve the existing complexity bounds for Tseitin formulas showing that resolution width, depth, and variable space coincide up to a logarithmic factor, and that variable space is bounded by the clause space times a logarithmic factor.n

Druh

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

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2020

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

ACM Transactions on Computation Theory

ISSN

1942-3454

e-ISSN

—

Svazek periodika

12

Číslo periodika v rámci svazku

2

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

22

Strana od-do

9

Kód UT WoS článku

000583676000002

EID výsledku v databázi Scopus

2-s2.0-85085257046