{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T18:17:00Z","timestamp":1781288220718,"version":"3.54.1"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2021,8,27]],"date-time":"2021-08-27T00:00:00Z","timestamp":1630022400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,8,27]],"date-time":"2021-08-27T00:00:00Z","timestamp":1630022400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["comput. complex."],"published-print":{"date-parts":[[2021,12]]},"DOI":"10.1007\/s00037-021-00213-2","type":"journal-article","created":{"date-parts":[[2021,8,27]],"date-time":"2021-08-27T14:05:44Z","timestamp":1630073144000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Near-Optimal Lower Bounds on Regular Resolution Refutations of Tseitin Formulas for All Constant-Degree Graphs"],"prefix":"10.1007","volume":"30","author":[{"given":"Dmitry","family":"Itsykson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Artur","family":"Riazanov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Danil","family":"Sagunov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2246-0273","authenticated-orcid":false,"given":"Petr","family":"Smirnov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,8,27]]},"reference":[{"key":"213_CR1","doi-asserted-by":"crossref","unstructured":"Michael Alekhnovich & Alexander A. Razborov (2011).\nSatisfiability, Branch-Width and Tseitin tautologies. Computational\nComplexity 20(4), 649\u2013678. URL https:\/\/doi.org\/10.1007\/s00037-011-0033-1.","DOI":"10.1007\/s00037-011-0033-1"},{"key":"213_CR2","doi-asserted-by":"crossref","unstructured":"A. Atserias & M. M\u00fcller (2019). Automating Resolution is NPHard.\nIn 2019 IEEE 60th Annual Symposium on Foundations of Computer\nScience (FOCS), 498\u2013509.","DOI":"10.1109\/FOCS.2019.00038"},{"key":"213_CR3","doi-asserted-by":"crossref","unstructured":"Albert Atserias (2008). On digraph coloring problems and treewidth\nduality. European Journal of Combinatorics 29(4), 796 \u2013 820. ISSN\n0195-6698. URL http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0195669807002004. Homomorphisms: Structure and Highlights.","DOI":"10.1016\/j.ejc.2007.11.004"},{"key":"213_CR4","doi-asserted-by":"crossref","unstructured":"Paul Beame, Chris Beck & Russell Impagliazzo (2016). Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear\nSpace. SIAM J. Comput. 45(4), 1612\u20131645. URL https:\/\/doi.org\/10.1137\/130914085.","DOI":"10.1137\/130914085"},{"key":"213_CR5","doi-asserted-by":"crossref","unstructured":"Eli Ben-Sasson (2002). Size Space Tradeoffs for Resolution. In Proceedings\nof the Thiry-fourth Annual ACM Symposium on Theory of\nComputing, STOC \u201902, 457\u2013464. ACM, New York, NY, USA. ISBN\n1-58113-495-9. URL http:\/\/doi.acm.org\/10.1145\/509907.509975.","DOI":"10.1145\/509907.509975"},{"key":"213_CR6","doi-asserted-by":"crossref","unstructured":"Eli Ben-Sasson & Avi Wigderson (2001). Short proofs are narrow\n- resolution made simple. J. ACM 48(2), 149\u2013169. URL https:\/\/doi.org\/10.1145\/375827.375835.","DOI":"10.1145\/375827.375835"},{"key":"213_CR7","doi-asserted-by":"crossref","unstructured":"Dan Bienstock (1990). On embedding graphs in trees. Journal\nof Combinatorial Theory, Series B 49(1), 103 \u2013 136. ISSN 0095-8956. URL http:\/\/www.sciencedirect.com\/science\/article\/pii\/0095895690900669.","DOI":"10.1016\/0095-8956(90)90066-9"},{"key":"213_CR8","doi-asserted-by":"crossref","unstructured":"Hans L Bodlaender & Arie MCA Koster (2006). Safe separators\nfor treewidth. Discrete Mathematics 306(3), 337\u2013350.","DOI":"10.1016\/j.disc.2005.12.017"},{"key":"213_CR9","doi-asserted-by":"crossref","unstructured":"Maria Luisa Bonet & Nicola Galesi (1999). A Study of Proof\nSearch Algorithms for Resolution and Polynomial Calculus. In 40th\nAnnual Symposium on Foundations of Computer Science, FOCS \u201999,\n17-18 October, 1999, New York, NY, USA, 422\u2013432. IEEE Computer\nSociety. URL https:\/\/doi.org\/10.1109\/SFFCS.1999.814614.","DOI":"10.1109\/SFFCS.1999.814614"},{"key":"213_CR10","unstructured":"Sam Buss, Dmitry Itsykson, Alexander Knop & Dmitry\nSokolov (2018). Reordering Rule Makes OBDD Proof Systems\nStronger. In 33rd Computational Complexity Conference (CCC 2018),\nRocco A. Servedio, editor, volume 102 of Leibniz International Proceedings\nin Informatics (LIPIcs), 16:1\u201316:24. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. ISBN 978-3-95977-069-9.\nISSN 1868-8969. URL http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2018\/8872."},{"key":"213_CR11","doi-asserted-by":"crossref","unstructured":"Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo & Toniann\nPitassi (1999). Linear Gaps Between Degrees for the Polynomial\nCalculus Modulo Distinct Primes (Abstract). In Proceedings of the 14th\nAnnual IEEE Conference on Computational Complexity, Atlanta, Georgia,\nUSA, May 4-6, 1999, 5. URL http:\/\/dx.doi.org\/10.1109\/CCC.1999.766254.","DOI":"10.1109\/CCC.1999.766254"},{"key":"213_CR12","doi-asserted-by":"crossref","unstructured":"Julia Chuzhoy (2015). Excluded Grid Theorem: Improved and Simplified.\nIn Proceedings of the Forty-Seventh Annual ACM on Symposium\non Theory of Computing, STOC 2015, Portland, OR, USA, June 14-17,\n2015, 645\u2013654. URL https:\/\/doi.org\/10.1145\/2746539.2746551.","DOI":"10.1145\/2746539.2746551"},{"key":"213_CR13","doi-asserted-by":"crossref","unstructured":"Julia Chuzhoy & Zihan Tan (2019). Towards Tight(Er) Bounds\nfor the Excluded Grid Theorem. In Proceedings of the Thirtieth Annual\nACM-SIAM Symposium on Discrete Algorithms, SODA \u201919, 1445\u2013\n1464. Society for Industrial and Applied Mathematics, Philadelphia,\nPA, USA. URL http:\/\/dl.acm.org\/citation.cfm?id=3310435.3310523.","DOI":"10.1137\/1.9781611975482.88"},{"key":"213_CR14","doi-asserted-by":"crossref","unstructured":"Alexis de Colnet & Stefan Mengel (2021). Characterizing\nTseitin-Formulas with Short Regular Resolution Refutations. In Theory\nand Applications of Satisfiability Testing \u2013 SAT 2021, Chu-Min Li\n& Felip Many\u00e0, editors, 116\u2013133. Springer International Publishing,\nCham. ISBN 978-3-030-80223-3.","DOI":"10.1007\/978-3-030-80223-3_9"},{"key":"213_CR15","doi-asserted-by":"crossref","unstructured":"Stephen A. Cook & Robert A. Reckhow (1979). The Relative\nEfficiency of Propositional Proof Systems. J. Symb. Log. 44(1), 36\u201350.\nURL https:\/\/doi.org\/10.2307\/2273702.","DOI":"10.2307\/2273702"},{"key":"213_CR16","doi-asserted-by":"crossref","unstructured":"Marek Cygan, Fedor V. Fomin, Lukasz Kowalik, Daniel\nLokshtanov, D\u00e1niel Marx, Marcin Pilipczuk, Michal\nPilipczuk & Saket Saurabh (2015). Parameterized Algorithms.\nSpringer. ISBN 978-3-319-21274-6. URL https:\/\/doi.org\/10.1007\/978-3-319-21275-3.","DOI":"10.1007\/978-3-319-21275-3_1"},{"key":"213_CR17","doi-asserted-by":"crossref","unstructured":"Stefan S. Dantchev & S\u00f8ren Riis (2001). Tree Resolution Proofs\nof the Weak Pigeon-Hole Principle. In Proceedings of the 16th Annual\nIEEE Conference on Computational Complexity, Chicago, Illinois,\nUSA, June 18-21, 2001, 69\u201375. IEEE Computer Society. ISBN 0-7695-1053-1. URL https:\/\/doi.org\/10.1109\/CCC.2001.933873.","DOI":"10.1109\/CCC.2001.933873"},{"key":"213_CR18","unstructured":"Nicola Galesi, Dmitry Itsykson, Artur Riazanov & Anastasia\nSofronova (2019). Bounded-Depth Frege Complexity of Tseitin\nFormulas for All Graphs. In 44th International Symposium on Mathematical\nFoundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, 49:1\u201349:15. URL https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2019.49."},{"key":"213_CR19","doi-asserted-by":"crossref","unstructured":"Nicola Galesi, Navid Talebanfard & Jacobo Tor\u00e1n (2020).\nCops-Robber Games and the Resolution of Tseitin Formulas. ACM\nTrans. Comput. Theory 12(2), 9:1\u20139:22. URL https:\/\/doi.org\/10.1145\/3378667.","DOI":"10.1145\/3378667"},{"key":"213_CR20","doi-asserted-by":"crossref","unstructured":"Zvi Galil (1977). On the Complexity of Regular Resolution and the\nDavis-Putnam Procedure. Theor. Comput. Sci. 4(1), 23\u201346. URL\nhttps:\/\/doi.org\/10.1016\/0304-3975(77)90054-8.","DOI":"10.1016\/0304-3975(77)90054-8"},{"key":"213_CR21","unstructured":"L. Glinskih & D. Itsykson (2017). Satisfiable Tseitin Formulas\nAre Hard for Nondeterministic Read-Once Branching Programs. In\nMFCS-2017, 26:1\u201326:12. URL https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2017.26."},{"key":"213_CR22","doi-asserted-by":"crossref","unstructured":"Ludmila Glinskih & Dmitry Itsykson (2021). On Tseitin Formulas,\nRead-Once Branching Programs and Treewidth. Theory\nComput. Syst. 65(3), 613\u2013633. URL https:\/\/doi.org\/10.1007\/s00224-020-10007-8.","DOI":"10.1007\/s00224-020-10007-8"},{"key":"213_CR23","doi-asserted-by":"crossref","unstructured":"Dima Grigoriev (2001). Linear lower bound on degrees of Positivstellensatz\ncalculus proofs for the parity. Theor. Comput. Sci. 259(1-2),\n613\u2013622. URL https:\/\/doi.org\/10.1016\/S0304-3975(00)00157-2.","DOI":"10.1016\/S0304-3975(00)00157-2"},{"key":"213_CR24","doi-asserted-by":"crossref","unstructured":"Daniel J. Harvey & David R. Wood (2018). The treewidth of line\ngraphs. Journal of Combinatorial Theory, Series B 132, 157 \u2013 179.\nISSN 0095-8956. URL http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0095895618300236.","DOI":"10.1016\/j.jctb.2018.03.007"},{"key":"213_CR25","doi-asserted-by":"crossref","unstructured":"Johan H\u00e5stad (2017). On Small-Depth Frege Proofs for Tseitin for\nGrids. In 58th IEEE Annual Symposium on Foundations of Computer\nScience, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, Chris\nUmans, editor, 97\u2013108. IEEE Computer Society. ISBN 978-1-5386-3464-6. URL https:\/\/doi.org\/10.1109\/FOCS.2017.18.","DOI":"10.1109\/FOCS.2017.18"},{"key":"213_CR26","doi-asserted-by":"crossref","unstructured":"Marijn J. H. Heule, Oliver Kullmann & Victor W. Marek\n(2016). Solving and Verifying the Boolean Pythagorean Triples Problem\nvia Cube-and-Conquer. In Theory and Applications of Satisfiability\nTesting \u2013 SAT 2016, Nadia Creignou & Daniel Le Berre, editors,\n228\u2013245. Springer International Publishing, Cham. ISBN 978-3-319-40970-2.","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"213_CR27","doi-asserted-by":"crossref","unstructured":"D.M. Itsykson & A.A. Kojevnikov (2006). Lower bounds of static\nLovasz-Schrijver calculus proofs for Tseitin tautologies. Zapiski Nauchnykh\nSeminarov POMI 340, 10\u201332.","DOI":"10.1007\/11786986_29"},{"key":"213_CR28","unstructured":"Dmitry Itsykson, Alexander Knop, Andrey Romashchenko &\nDmitry Sokolov (2017). On OBDD-Based Algorithms and Proof Systems\nThat Dynamically Change Order of Variables. In 34th Symposium\non Theoretical Aspects of Computer Science (STACS 2017), Heribert\nVollmer & Brigitte Vallee, editors, volume 66 of Leibniz\nInternational Proceedings in Informatics (LIPIcs), 43:1\u201343:14. Schloss\nDagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. ISBN\n978-3-95977-028-6. ISSN 1868-8969. URL http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2017\/6991."},{"key":"213_CR29","doi-asserted-by":"crossref","unstructured":"Dmitry Itsykson & Vsevolod Oparin (2013). Graph Expansion,\nTseitin Formulas and Resolution Proofs for CSP. In Computer Science\n- Theory and Applications - 8th International Computer Science\nSymposium in Russia, CSR 2013, Ekaterinburg, Russia, June 25-29,\n2013. Proceedings, Andrei A. Bulatov & Arseny M. Shur, editors,\nvolume 7913 of Lecture Notes in Computer Science, 162\u2013173.\nSpringer. ISBN 978-3-642-38535-3. URL https:\/\/doi.org\/10.1007\/978-3-642-38536-0_14.","DOI":"10.1007\/978-3-642-38536-0_14"},{"key":"213_CR30","doi-asserted-by":"crossref","unstructured":"L\u00e1szl\u00f3 Lov\u00e1sz, Moni Naor, Ilan Newman & Avi Wigderson\n(1995). Search Problems in the Decision Tree Model. SIAM J.\nDiscrete Math. 8(1), 119\u2013132. URL http:\/\/dx.doi.org\/10.1137\/S0895480192233867.","DOI":"10.1137\/S0895480192233867"},{"key":"213_CR31","doi-asserted-by":"crossref","unstructured":"Igor L Markov & Yaoyun Shi (2011). Constant-Degree Graph Expansions\nthat Preserve Treewidth. Algorithmica 59(4), 461\u2013470.","DOI":"10.1007\/s00453-009-9312-5"},{"key":"213_CR32","doi-asserted-by":"crossref","unstructured":"Toniann Pitassi, Benjamin Rossman, Rocco A. Servedio & Li-Yang Tan (2016). Poly-logarithmic Frege depth lower bounds via an\nexpander switching lemma. In Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2016, Cambridge,\nMA, USA, June 18-21, 2016, Daniel Wichs & Yishay Mansour,\neditors, 644\u2013657. ACM. ISBN 978-1-4503-4132-5. URL https:\/\/doi.org\/10.1145\/2897518.2897637.","DOI":"10.1145\/2897518.2897637"},{"key":"213_CR33","doi-asserted-by":"crossref","unstructured":"Neil Robertson & Paul D. Seymour (1983). Graph minors. I.\nExcluding a forest. J. Comb. Theory, Ser. B 35(1), 39\u201361.","DOI":"10.1016\/0095-8956(83)90079-5"},{"key":"213_CR34","doi-asserted-by":"crossref","unstructured":"Gert Sabidussi (1959). Graph multiplication. Mathematische\nZeitschrift 72(1), 446\u2013457.","DOI":"10.1007\/BF01162967"},{"key":"213_CR35","doi-asserted-by":"crossref","unstructured":"Petra Scheffler (1992). Optimal embedding of a tree into an interval\ngraph in linear time. In Annals of Discrete Mathematics, volume 51,\n287\u2013291. Elsevier.","DOI":"10.1016\/S0167-5060(08)70644-7"},{"key":"213_CR36","unstructured":"G.S. Tseitin (1968). On the complexity of derivation in the propositional\ncalculus. In Studies in Constructive Mathematics and Mathematical\nLogic Part II. A. O. Slisenko, editor."},{"key":"213_CR37","doi-asserted-by":"crossref","unstructured":"A. Urquhart (1987). Hard Examples for Resolution. JACM 34(1),\n209\u2013219.","DOI":"10.1145\/7531.8928"},{"key":"213_CR38","doi-asserted-by":"crossref","unstructured":"Alasdair Urquhart (2012). Width and size of regular resolution\nproofs. Logical Methods in Computer Science 8.","DOI":"10.2168\/LMCS-8(2:8)2012"},{"key":"213_CR39","unstructured":"Lintao Zhang, Conor F. Madigan, Matthew H. Moskewicz &\nSharad Malik (2001). Efficient Conflict Driven Learning in a Boolean\nSatisfiability Solver. In Proceedings of the 2001 IEEE\/ACM International\nConference on Computer-Aided Design, ICCAD \u201901, 279\u2013285.\nIEEE Press. ISBN 0780372492."}],"updated-by":[{"DOI":"10.1007\/s00037-021-00216-z","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2021,11,17]],"date-time":"2021-11-17T00:00:00Z","timestamp":1637107200000}}],"container-title":["computational complexity"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00037-021-00213-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00037-021-00213-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00037-021-00213-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,2]],"date-time":"2021-12-02T03:04:19Z","timestamp":1638414259000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00037-021-00213-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,27]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["213"],"URL":"https:\/\/doi.org\/10.1007\/s00037-021-00213-2","relation":{"correction":[{"id-type":"doi","id":"10.1007\/s00037-021-00216-z","asserted-by":"object"}]},"ISSN":["1016-3328","1420-8954"],"issn-type":[{"value":"1016-3328","type":"print"},{"value":"1420-8954","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,27]]},"assertion":[{"value":"24 December 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 August 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 November 2021","order":3,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":4,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":5,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s00037-021-00216-z","URL":"https:\/\/doi.org\/10.1007\/s00037-021-00216-z","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"13"}}