{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T01:04:36Z","timestamp":1770339876192,"version":"3.49.0"},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2020,3,4]],"date-time":"2020-03-04T00:00:00Z","timestamp":1583280000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ERC","award":["FEALORA 339691"],"award-info":[{"award-number":["FEALORA 339691"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Theory"],"published-print":{"date-parts":[[2020,6,30]]},"abstract":"<jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>","DOI":"10.1145\/3378667","type":"journal-article","created":{"date-parts":[[2020,3,4]],"date-time":"2020-03-04T11:08:20Z","timestamp":1583320100000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Cops-Robber Games and the Resolution of Tseitin Formulas"],"prefix":"10.1145","volume":"12","author":[{"given":"Nicola","family":"Galesi","sequence":"first","affiliation":[{"name":"Sapienza Universit\u00e0 di Roma, Rome, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Navid","family":"Talebanfard","sequence":"additional","affiliation":[{"name":"Czech Academy of Sciences, Prague, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacobo","family":"Tor\u00e1n","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Ulm, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,3,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1384252.1384253"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-011-0033-1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700366735"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ejc.2007.11.004"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 18th IEEE Conference on Computational Complexity. 239--247","author":"Atserias A.","unstructured":"A. Atserias and V. Dalmau . 2003. A combinatorial characterization of resolution width . In Proceedings of the 18th IEEE Conference on Computational Complexity. 239--247 . A. Atserias and V. Dalmau. 2003. A combinatorial characterization of resolution width. In Proceedings of the 18th IEEE Conference on Computational Complexity. 239--247."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1137\/130914085"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 45th ACM Symposium on the Theory of Computing","author":"Beck C.","year":"2013","unstructured":"C. Beck , J. Nordstr\u00f6m , and B. Tang . 2013. Some trade-off results for polynomial calculus: Extended abstract . Proceedings of the 45th ACM Symposium on the Theory of Computing ( 2013 ), 813--822. C. Beck, J. Nordstr\u00f6m, and B. Tang. 2013. Some trade-off results for polynomial calculus: Extended abstract. Proceedings of the 45th ACM Symposium on the Theory of Computing (2013), 813--822."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1064"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2921"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.02.040"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(03)00030-8"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/21559.21567"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-017-0163-1"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1006\/jctb.1993.1027"},{"key":"e_1_2_1_18_1","first-page":"86","article-title":"Space and width in propositional resolution","volume":"83","author":"Tor\u00e1n J.","year":"2004","unstructured":"J. Tor\u00e1n . 2004 . Space and width in propositional resolution . Computational Complexity Column, Bulletin of EATCS 83 (2004), 86 -- 104 . J. Tor\u00e1n. 2004. Space and width in propositional resolution. Computational Complexity Column, Bulletin of EATCS 83 (2004), 86--104.","journal-title":"Computational Complexity Column, Bulletin of EATCS"},{"key":"e_1_2_1_19_1","first-page":"115","volume-title":"Studies in Constructive Mathematics and Mathematical Logic, Part 2","author":"Tseitin G. S.","year":"1968","unstructured":"G. S. Tseitin . 1968. On the complexity of derivation in propositional calculus . In Studies in Constructive Mathematics and Mathematical Logic, Part 2 , pages 115 -- 125 . Consultants Bureau , 1968 . G. S. Tseitin. 1968. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part 2, pages 115--125. Consultants Bureau, 1968."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/7531.8928"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-011-9356-9"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(2:8)2012"}],"container-title":["ACM Transactions on Computation Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3378667","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3378667","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:19Z","timestamp":1750200079000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3378667"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,3,4]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,6,30]]}},"alternative-id":["10.1145\/3378667"],"URL":"https:\/\/doi.org\/10.1145\/3378667","relation":{},"ISSN":["1942-3454","1942-3462"],"issn-type":[{"value":"1942-3454","type":"print"},{"value":"1942-3462","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,3,4]]},"assertion":[{"value":"2018-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-03-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}