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 extended method for proving size lower bounds, and it is known that for these 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.

In this paper, we study the width complexity of CP refutations of graph isomorphism formulas. For a pair of non-isomorphic graphs $G$ and $H$, we show a direct connection between the Weisfeiler-Leman differentiation number $\mathsf{WL}(G, H)$ of the graphs and the width of a CP refutation for the corresponding isomorphism formula $\mathrm{Iso}(G, H)$. In particular, we show that if $\mathsf{WL}(G, H) \leq k$, then there is a CP refutation of $\mathrm{Iso}(G, H)$ with width $k$, and if $\mathsf{WL}(G, H) > k$, then there are no CP refutations of $\mathrm{Iso}(G, H)$ with width $k-2$. Similar results are known for other proof systems, like Resolution, Sherali–Adams, or Polynomial Calculus. We also obtain polynomial-size CP refutations from our width bound for isomorphism formulas for graphs with constant WL-dimension.