{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:02:51Z","timestamp":1750309371954,"version":"3.41.0"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T00:00:00Z","timestamp":1730160000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2024,10,31]]},"abstract":"The width complexity measure plays a central role in resolution and other propositional proof systems like Polynomial Calculus (under the name of degree). The study of width lower bounds is the most used method for proving size lower bounds, and it is known that for the mentioned proof systems, proofs with small width also imply the existence of proofs with small size. Not much has been studied, however, about the width parameter in the cutting planes (CP) proof system, a measure that was introduced by Dantchev and Martin in 2009 under the name of CP cutwidth.<\/jats:p>\n \n In this article, we study the width complexity of CP refutations of graph isomorphism formulas. For a pair of non-isomorphic graphs\n \n \\(G\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n and\n \n \\(H\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n , we show a direct connection between the Weisfeiler\u2013Leman differentiation number\n \n \\(\\mathsf{WL}(G,H)\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n of the graphs and the width of a CP refutation for the corresponding isomorphism formula\n \n \\(\\mathrm{Iso}(G,H)\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n . In particular, we show that if\n \n \\(\\mathsf{WL}(G,H)\\leq k\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n , then there is a CP refutation of\n \n \\(\\mathrm{Iso}(G,H)\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n with width\n \n \\(k\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n , and if\n \n \\(\\mathsf{WL}(G,H) \\gt k\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n , then there are no CP refutations of\n \n \\(\\mathrm{Iso}(G,H)\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n with width\n \n \\(k-2\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n . Similar results are known for other proof systems, like Resolution, Sherali\u2013Adams, or Polynomial Calculus. We also obtain polynomial-length CP refutations from our width bound for isomorphism formulas for graphs with constant Weisfeiler\u2013Leman dimension. Furthermore, we notice that a length lower bound for refuting graph isomorphism formulas in the subsystem of tree-like cutting planes with polynomially bounded coefficients follows from known results.\n <\/jats:p>","DOI":"10.1145\/3677121","type":"journal-article","created":{"date-parts":[[2024,7,18]],"date-time":"2024-07-18T16:31:53Z","timestamp":1721320313000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Cutting Planes Width and the Complexity of Graph Isomorphism Refutations"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2168-4969","authenticated-orcid":false,"given":"Jacobo","family":"Tor\u00e1n","sequence":"first","affiliation":[{"name":"Institute of Theoretical Computer Science, Universit\u00e4t Ulm, Ulm, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2463-8167","authenticated-orcid":false,"given":"Florian","family":"W\u00f6rz","sequence":"additional","affiliation":[{"name":"Institute of Theoretical Computer Science, Universit\u00e4t Ulm, Ulm, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,10,29]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1137\/120867834"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209186"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/2897518.2897542"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1137\/0209047"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(88)90028-1"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47672-7_13"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934560"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-0208(08)73545-X"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539799352474"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.4086\/toc.2006.v002a004"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01305232"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(73)90167-2"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237860"},{"key":"e_1_3_2_16_2","unstructured":"Paolo Codenotti Grant Schoenebeck and Aaron Snook. 2014. Graph Isomorphism and the Lasserre Hierarchy. arXiv:1401.0758. Retrieved from https:\/\/arxiv.org\/abs\/1401.0758"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(87)90039-4"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CCC.2020.34"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-011-9373-0"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.4064\/fm-49-2-129-141"},{"key":"e_1_3_2_22_2","first-page":"1022","article-title":"Sur une nouvelle classification des syst\u00e8mes de relations","volume":"230","author":"Fra\u00efss\u00e9 Roland","year":"1950","unstructured":"Roland Fra\u00efss\u00e9. 1950. Sur une nouvelle classification des syst\u00e8mes de relations. Comptes rendus hebdomadaires des s\u00e9ances de l\u2019Acad\u00e9mie des sciences 230 (Jun. 1950), 1022\u20131024. Retrieved from https:\/\/gallica.bnf.fr\/ark:\/12148\/bpt6k3182n In French.","journal-title":"Comptes rendus hebdomadaires des s\u00e9ances de l\u2019Acad\u00e9mie des sciences"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.4086\/toc.2020.v016a013"},{"key":"e_1_3_2_24_2","doi-asserted-by":"crossref","unstructured":"Ralph E. Gomory. 1958. Outline of an Algorithm for Integer Solutions to Linear Programs. Bull. Amer. Math. Soc. 64 5 (Sept. 1958) 275\u2013278. Retrieved from https:\/\/ralphgomory.org\/wp-content\/uploads\/2023\/02\/07_outline.pdf","DOI":"10.1090\/S0002-9904-1958-10224-4"},{"key":"e_1_3_2_25_2","unstructured":"Ralph E. Gomory. 1963. An Algorithm for Integer Solutions of Linear Programs. In Recent Advances in Mathematical Programming Robert L. Graves and Philip Wolfe (Eds.). McGraw-Hill New York NY 269\u2013302. Retrieved from https:\/\/ralphgomory.org\/wp-content\/uploads\/2023\/02\/Algorithm_for_integer-1.pdf"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68279-0_4"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1137\/16M1082007"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1017\/9781139028868"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2021.134"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS56636.2023.10175741"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1017\/jsl.2015.28"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1617"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1112\/jlms\/s1-10.37.26"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0070"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/bf02186368"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2017.20"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/2213977.2214000"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(82)90011-3"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0539-5"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316069"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050024"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24508-4"},{"key":"e_1_3_2_43_2","unstructured":"Leonid G. Khachiyan. 1979. A Polynomial Algorithm in Linear Programming. Doklady Akademii Nauk SSSR 224 5 (1979) 1093\u20131096. Retrieved from https:\/\/www.mathnet.ru\/eng\/dan42319"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1016\/0041-5553(80)90061-0"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3333003"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1987.11"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/2903266"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07003-1"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.disopt.2014.01.004"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1137\/0220062"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611973402.120"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.2307\/2275583"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1287\/moor.2016.0840"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2023.101"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-5060(08)70085-2"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.STACS.2021.58"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1137\/0403036"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02240204"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1137\/S009753970241096X"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39071-5_6"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/3580478"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-218X(99)00039-6"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-011-9356-9"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0089374"},{"key":"e_1_3_2_67_2","unstructured":"Boris Yu Weisfeiler and Andrei A. Leman. 1968. The Reduction of a Graph to Canonical Form and the Algebra Which Appears Therein. Nauchno-Technicheskaya Informatsia 2 9 (1968) 12\u201316. Original Russian version available at https:\/\/www.iti.zcu.cz\/wl2018\/pdf\/wl_paper_orig.pdf. Translation from Russian into English by Grigory Ryabov available at https:\/\/www.iti.zcu.cz\/wl2018\/pdf\/wl_paper_translation.pdf"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3677121","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3677121","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:06:17Z","timestamp":1750291577000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3677121"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,29]]},"references-count":64,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,10,31]]}},"alternative-id":["10.1145\/3677121"],"URL":"https:\/\/doi.org\/10.1145\/3677121","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2024,10,29]]},"assertion":[{"value":"2023-11-20","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-29","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}