{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:43:42Z","timestamp":1781077422548,"version":"3.54.1"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T00:00:00Z","timestamp":1725840000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100006769","name":"Russian Science Foundation","doi-asserted-by":"crossref","award":["18-71-10042"],"award-info":[{"award-number":["18-71-10042"]}],"id":[{"id":"10.13039\/501100006769","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Theory"],"published-print":{"date-parts":[[2024,9,30]]},"abstract":"<jats:p>\n            We consider the proof system Res\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\((\\oplus)\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            introduced by Itsykson and Sokolov (Ann. Pure Appl. Log.\u201920), which is an extension of the resolution proof system and operates with disjunctions of linear equations over\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\({\\mathbb {F}}_2\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            .\n          <\/jats:p>\n          <jats:p>\n            We study characterizations of tree-like size and space of Res\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\((\\oplus)\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            refutations using combinatorial games. Namely, we introduce a class of extensible formulas and prove tree-like size lower bounds on it using Prover\u2013Delayer games, as well as space lower bounds. This class is of particular interest since it contains many classical combinatorial principles, including the pigeonhole, ordering, and dense linear ordering principles. Furthermore, we present the width-space relation for Res\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\((\\oplus)\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            generalizing the results by Atserias and Dalmau (J. Comput. Syst. Sci.\u201908) and their variant of Spoiler\u2013Duplicator games.\n          <\/jats:p>","DOI":"10.1145\/3675415","type":"journal-article","created":{"date-parts":[[2024,7,11]],"date-time":"2024-07-11T10:47:55Z","timestamp":1720694875000},"page":"1-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Resolution Over Linear Equations: Combinatorial Games for Tree-like Size and Space"],"prefix":"10.1145","volume":"16","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5648-8194","authenticated-orcid":false,"given":"Svyatoslav","family":"Gryaznov","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9478-1949","authenticated-orcid":false,"given":"Sergei","family":"Ovcharov","sequence":"additional","affiliation":[{"name":"St. Petersburg State University, St. Petersburg, Russian Federation"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7892-1502","authenticated-orcid":false,"given":"Artur","family":"Riazanov","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,9,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700366735"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JCSS.2007.06.025"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237860"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2921"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/1838552.1838556"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3243126"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1137\/16M1082007"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-19955-5_15"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0273-0979-06-01126-8"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66263-3_4"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2019.102722"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CCC.2015.467"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-020-00202-x"},{"key":"e_1_3_1_17_2","first-page":"128","volume-title":"Proceedings of the Eleventh Annual ACM-SIAM Symposium on Discrete Algorithms, January 9\u201311, 2000, San Francisco, CA, USA","author":"Pudl\u00e1k Pavel","year":"2000","unstructured":"Pavel Pudl\u00e1k and Russell Impagliazzo. 2000. A lower bound for DLL algorithms for k-SAT (preliminary version). In Proceedings of the Eleventh Annual ACM-SIAM Symposium on Discrete Algorithms, January 9\u201311, 2000, San Francisco, CA, USA, David B. Shmoys (Ed.). ACM\/SIAM, San Francisco, CA, 128\u2013136. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=338219.338244"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2008.04.001"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/S00037-001-8194-Y"}],"container-title":["ACM Transactions on Computation Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3675415","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3675415","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:04:05Z","timestamp":1750291445000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3675415"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,9]]},"references-count":18,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,9,30]]}},"alternative-id":["10.1145\/3675415"],"URL":"https:\/\/doi.org\/10.1145\/3675415","relation":{},"ISSN":["1942-3454","1942-3462"],"issn-type":[{"value":"1942-3454","type":"print"},{"value":"1942-3462","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,9]]},"assertion":[{"value":"2022-10-18","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-24","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-09-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}