{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T19:35:43Z","timestamp":1787340943495,"version":"build-2736575974"},"reference-count":22,"publisher":"Society for Industrial & Applied Mathematics (SIAM)","issue":"5","funder":[{"DOI":"10.13039\/501100001711","name":"Swiss National Science Foundation","doi-asserted-by":"crossref","award":["200021-184656"],"award-info":[{"award-number":["200021-184656"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004063","name":"Knut och Alice Wallenbergs Stiftelse","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004063","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SIAM J. Comput."],"published-print":{"date-parts":[[2025,10,31]]},"abstract":"<jats:p>Abstract.<\/jats:p>\n                  <jats:p>We study Frege proofs using depth-[Formula: see text] Boolean formulas for the Tseitin contradiction on [Formula: see text] grids. We prove that if each line in the proof is of size [Formula: see text],\u00a0then the number of lines is exponential in [Formula: see text]. This strengthens a recent result of Pitassi, Ramakrishman, and Tan [2022 IEEE 62 nd Annual Symposium on Foundations of Computer Science, 2022, pp. 445\u2013456].\u00a0The key technical step is a multiswitching lemma extending the switching lemma of H\u00e5stad [ J. ACM, 68 (2021), 1]\u00a0for a space of restrictions related to the Tseitin contradiction. The strengthened lemma also allows us to improve the lower bound for standard proof size of bounded depth Frege refutations from exponential in [Formula: see text] to exponential in [Formula: see text]. This strengthens the bounds given in the preliminary version of this paper [J. H\u00e5stad and K. Risse, 2022 IEEE 63 rd Annual Symposium on Foundations of Computer Science, 2022, pp. 1138\u20131149].<\/jats:p>","DOI":"10.1137\/22m153851x","type":"journal-article","created":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T07:41:48Z","timestamp":1760600508000},"page":"FOCS22-288-FOCS22-339","source":"Crossref","is-referenced-by-count":0,"title":["On Bounded Depth Proofs for Tseitin Formulas on the Grid; Revisited"],"prefix":"10.1137","volume":"54","author":[{"given":"Johan","family":"H\u00e5stad","sequence":"first","affiliation":[{"name":"KTH Royal Institute of Technology, Stockholm, Sweden."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6913-3341","authenticated-orcid":true,"given":"Kilian","family":"Risse","sequence":"additional","affiliation":[{"name":"Lund University, LTH, Lund, Sweden."}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"351","published-online":{"date-parts":[[2025,10,16]]},"reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01302964"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-002-0172-5"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/BF01744431"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"ref6","doi-asserted-by":"crossref","unstructured":"J. H\u00e5stad, Almost optimal lower bounds for small depth circuits, in Proceedings of the Eighteenth Annual ACM Symposium on Theory of Computing, STOC \u201986, ACM, New York, 1986, pp. 6\u201320, https:\/\/doi.org\/10.1145\/12130.12132.","DOI":"10.1145\/12130.12132"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1137\/120897432"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3425606"},{"key":"ref9","doi-asserted-by":"crossref","unstructured":"J. H\u00e5stad and K. Risse, On bounded depth proofs for Tseitin formulas on the grid; revisited, in 2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS), 2022, pp. 1138\u20131149.","DOI":"10.1109\/FOCS54457.2022.00110"},{"key":"ref10","doi-asserted-by":"crossref","unstructured":"R. Impagliazzo, W. Matthews, and R. Paturi, A satisfiability algorithm for \\(\\sf{AC}^0\\), in Proceedings\u00a0of the Twenty-Third Annual ACM-SIAM Symposium on Discrete Algorithms, ACM, New York, SIAM, Philadelphia, 2012, pp. 961\u2013972, https:\/\/doi.org\/10.1137\/1.9781611973099.77.","DOI":"10.1137\/1.9781611973099.77"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.3240070103"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/BF01200117"},{"key":"ref13","doi-asserted-by":"crossref","unstructured":"T. Pitassi, P. Ramakrishnan, and L. Tan, Tradeoffs for small-depth Frege proofs, in 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS), IEEE Computer Society, Los Alamitos, CA, 2022, pp. 445\u2013456, https:\/\/doi.org\/10.1109\/FOCS52979.2021.00052.","DOI":"10.1109\/FOCS52979.2021.00052"},{"key":"ref14","doi-asserted-by":"crossref","unstructured":"T. Pitassi, B. Rossman, R. A. Servedio, and L.Y. Tan, Poly-logarithmic Frege depth lower bounds via an expander switching lemma, in Proceedings of the Forty-Eighth Annual ACM Symposium on Theory of Computing, STOC \u201916, Association for Computing Machinery, 2016, pp. 644\u2013657, https:\/\/doi.org\/10.1145\/2897518.","DOI":"10.1145\/2897518.2897637"},{"key":"ref15","first-page":"149","volume-title":"Problems of Cybernetics. Complexity Theory and Applied Mathematical Logic","author":"Razborov A.","year":"1988"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2566-9_12"},{"key":"ref17","doi-asserted-by":"crossref","unstructured":"B. Rossman, R. A. Servedio, and L. Tan, An average-case depth hierarchy theorem for Boolean circuits, in IEEE 56th Annual Symposium on Foundations of Computer Science, FOCS 2015, Berkeley, CA, 2015, pp. 1030\u20131048.","DOI":"10.1109\/FOCS.2015.67"},{"key":"ref18","doi-asserted-by":"crossref","unstructured":"M. Sipser, Borel sets and circuit complexity, in Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing, STOC \u201983, ACM, 1983, pp. 61\u201369, https:\/\/doi.org\/10.1145\/800061.808733.","DOI":"10.1145\/800061.808733"},{"key":"ref19","doi-asserted-by":"crossref","unstructured":"R. Smolensky, Algebraic methods in the theory of lower bounds for Boolean circuit complexity, in Proceedings of the Nineteenth Annual ACM Symposium on Theory of Computing, STOC \u201987, ACM, 1987, pp. 77\u201382, https:\/\/doi.org\/10.1145\/28395.28404.","DOI":"10.1145\/28395.28404"},{"key":"ref20","volume-title":"Studies in Constructive Mathematics and Mathematical Logic, Part II","author":"Tseitin G. S.","year":"1968"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1040046140"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1985.49"}],"container-title":["SIAM Journal on Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/epubs.siam.org\/doi\/pdf\/10.1137\/22M153851X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T18:57:31Z","timestamp":1787338651000},"score":1,"resource":{"primary":{"URL":"https:\/\/epubs.siam.org\/doi\/10.1137\/22M153851X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,16]]},"references-count":22,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2025,10,31]]}},"alternative-id":["10.1137\/22M153851X"],"URL":"https:\/\/doi.org\/10.1137\/22m153851x","relation":{},"ISSN":["0097-5397","1095-7111"],"issn-type":[{"value":"0097-5397","type":"print"},{"value":"1095-7111","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,16]]}}}