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

Cops-Robber Games and the Resolution of Tseitin Formulas / Galesi, N.; Talebanfard, N.; Toran, J.. - In: ACM TRANSACTIONS ON COMPUTATION THEORY. - ISSN 1942-3454. - 12:2(2020), pp. 1-22. [10.1145/3378667]

Cops-Robber Games and the Resolution of Tseitin Formulas

Galesi N.
Primo
Membro del Collaboration Group
;
2020

Abstract

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. We 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. Using 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.
2020
cops-robber game; resolution
01 Pubblicazione su rivista::01a Articolo in rivista
Cops-Robber Games and the Resolution of Tseitin Formulas / Galesi, N.; Talebanfard, N.; Toran, J.. - In: ACM TRANSACTIONS ON COMPUTATION THEORY. - ISSN 1942-3454. - 12:2(2020), pp. 1-22. [10.1145/3378667]
File allegati a questo prodotto
File Dimensione Formato  
Galesi_Cops-Robber_2020.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 279 kB
Formato Adobe PDF
279 kB Adobe PDF   Contatta l'autore

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/1422847
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 5
social impact