{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,17]],"date-time":"2026-01-17T21:32:56Z","timestamp":1768685576718,"version":"3.49.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2023,10,11]],"date-time":"2023-10-11T00:00:00Z","timestamp":1696982400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"European Research Council under the European Union\u2019s Seventh Framework Programme","award":["FP7\/2007\u20132013"],"award-info":[{"award-number":["FP7\/2007\u20132013"]}]},{"name":"ERC","award":["279611"],"award-info":[{"award-number":["279611"]}]},{"DOI":"10.13039\/501100004359","name":"Swedish Research Council","doi-asserted-by":"crossref","award":["621-2010-4797, 621-2012-5645, and 2016-00782"],"award-info":[{"award-number":["621-2010-4797, 621-2012-5645, and 2016-00782"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Independent Research Fund Denmark","award":["9040-00389B"],"award-info":[{"award-number":["9040-00389B"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2023,10,31]]},"abstract":"<jats:p>\n            We prove near-optimal tradeoffs for quantifier depth (also called quantifier rank) versus number of variables in first-order logic by exhibiting pairs of\n            <jats:italic>n<\/jats:italic>\n            -element structures that can be distinguished by a\n            <jats:italic>k<\/jats:italic>\n            -variable first-order sentence but where every such sentence requires quantifier depth at least\u00a0\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>\n              \u03a9 (\n              <jats:italic>k<\/jats:italic>\n              \/log\n              <jats:italic>k<\/jats:italic>\n              )\n            <\/jats:sup>\n            . Our tradeoffs also apply to first-order counting logic and, by the known connection to the\n            <jats:italic>k<\/jats:italic>\n            -dimensional Weisfeiler\u2013Leman algorithm, imply near-optimal lower bounds on the number of refinement iterations.\n          <\/jats:p>\n          <jats:p>A key component in our proof is the hardness condensation technique introduced by Razborov in the context of proof complexity. We apply this method to reduce the domain size of relational structures while maintaining the minimal quantifier depth needed to distinguish them in finite variable logics.<\/jats:p>","DOI":"10.1145\/3195257","type":"journal-article","created":{"date-parts":[[2023,7,20]],"date-time":"2023-07-20T12:03:32Z","timestamp":1689854612000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Near-optimal Lower Bounds on Quantifier Depth and Weisfeiler\u2013Leman Refinement Steps"],"prefix":"10.1145","volume":"70","author":[{"given":"Christoph","family":"Berkholz","sequence":"first","affiliation":[{"name":"Humboldt-Universit\u00e4t zu Berlin, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jakob","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[{"name":"University of Copenhagen, Denmark and Lund University, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,11]]},"reference":[{"key":"e_1_3_3_2_2","first-page":"18","article-title":"Lower bounds for polynomial calculus: Non-binomial case","volume":"242","author":"Alekhnovich Michael","year":"2003","unstructured":"Michael Alekhnovich and Alexander A. Razborov. 2003. Lower bounds for polynomial calculus: Non-binomial case. Proc. Steklov Inst. Math. 242 (2003), 18\u201335. Retrieved from http:\/\/people.cs.uchicago.edu\/razborov\/files\/misha.pdf","journal-title":"Proc. Steklov Inst. Math."},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2007.06.025"},{"key":"e_1_3_3_4_2","first-page":"684","volume-title":"Proceedings of the 48th Annual ACM Symposium on Theory of Computing (STOC\u201916)","author":"Babai L\u00e1szl\u00f3","year":"2016","unstructured":"L\u00e1szl\u00f3 Babai. 2016. Graph isomorphism in quasipolynomial time. In Proceedings of the 48th Annual ACM Symposium on Theory of Computing (STOC\u201916). 684\u2013697."},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.2307\/2272133"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/2488608.2488711"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-002-0172-5"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/509907.509975"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1137\/080723880"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2008.42"},{"key":"e_1_3_3_11_2","first-page":"401","volume-title":"Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS\u201911)","author":"Ben-Sasson Eli","year":"2011","unstructured":"Eli Ben-Sasson and Jakob Nordstr\u00f6m. 2011. Understanding space in proof complexity: Separations and trade-offs via substitutions. In Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS\u201911). 401\u2013416."},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10428-7_14"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1137\/16M1109072"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1203350790"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1726"},{"key":"e_1_3_3_17_2","series-title":"(Frontiers in Artificial Intelligence and Applications","first-page":"233","volume-title":"Handbook of Satisfiability (2nd ed.)","author":"Buss Samuel R.","year":"2021","unstructured":"Samuel R. Buss and Jakob Nordstr\u00f6m. 2021. Proof complexity and SAT solving. In Handbook of Satisfiability (2nd ed.) (Frontiers in Artificial Intelligence and Applications, Vol. 336), Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh (Eds.). IOS Press233\u2013350."},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01305232"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(74)80046-2"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39206-1_37"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48224-5_27"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68804-8_3"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00157-2"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.2307\/420954"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s004939970004"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2371656.2371662"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2301.13317"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.2307\/2275675"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3425606"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0070"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90039-8"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(82)90011-3"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4478-3_5"},{"key":"e_1_3_3_34_2","series-title":"Proceedings of the 47th International Colloquium on Automata, Languages and Programming (ICALP\u201920)","first-page":"73:1\u201373:19","volume":"168","author":"Kiefer Sandra","year":"2020","unstructured":"Sandra Kiefer and Brendan D. McKay. 2020. The iteration number of colour refinement. In Proceedings of the 47th International Colloquium on Automata, Languages and Programming (ICALP\u201920) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 168). 73:1\u201373:19."},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933595"},{"issue":"2","key":"e_1_3_3_36_2","article-title":"Upper bounds on the quantifier depth for graph differentiation in first-order logic","volume":"15","author":"Kiefer Sandra","year":"2019","unstructured":"Sandra Kiefer and Pascal Schweitzer. 2019. Upper bounds on the quantifier depth for graph differentiation in first-order logic. Logic. Meth. Comput. Sci. 15, 2 (2019).","journal-title":"Logic. Meth. Comput. Sci."},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/11786986_29"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1017\/9781108242066"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.69"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.5555\/3470152.3470185"},{"key":"e_1_3_3_41_2","series-title":"Proceedings of the 30th Annual Computational Complexity Conference (CCC\u201915)","first-page":"467","volume":"33","author":"Mik\u0161a Mladen","year":"2015","unstructured":"Mladen Mik\u0161a and Jakob Nordstr\u00f6m. 2015. A generalized method for proving polynomial calculus degree lower bounds. In Proceedings of the 30th Annual Computational Complexity Conference (CCC\u201915) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 33). 467\u2013487."},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(3:15)2013"},{"key":"e_1_3_3_43_2","first-page":"644","volume-title":"Proceedings of the 48th Annual ACM Symposium on Theory of Computing (STOC\u201916)","author":"Pitassi Toniann","year":"2016","unstructured":"Toniann Pitassi, Benjamin Rossman, Rocco Servedio, and Li-Yang Tan. 2016. Poly-logarithmic Frege depth lower bounds. In Proceedings of the 48th Annual ACM Symposium on Theory of Computing (STOC\u201916). 644\u2013657."},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/2858790"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2008.74"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/7531.8928"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/212433.212474"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3195257","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3195257","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:08:51Z","timestamp":1750208931000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3195257"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,11]]},"references-count":46,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2023,10,31]]}},"alternative-id":["10.1145\/3195257"],"URL":"https:\/\/doi.org\/10.1145\/3195257","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,11]]},"assertion":[{"value":"2016-10-04","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-05-28","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-10-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}