License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2023.26
URN: urn:nbn:de:0030-drops-184884
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18488/
Go to the corresponding LIPIcs Volume Portal

Torán, Jacobo ; Wörz, Florian

Cutting Planes Width and the Complexity of Graph Isomorphism Refutations

pdf-format:
LIPIcs-SAT-2023-26.pdf (0.9 MB)

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 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 2011 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 WL(G, H) of the graphs and the width of a CP refutation for the corresponding isomorphism formula Iso(G, H). In particular, we show that if WL(G, H) ≤ k, then there is a CP refutation of Iso(G, H) with width k, and if WL(G, H) > k, then there are no CP refutations of 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.

BibTeX - Entry

@InProceedings{toran_et_al:LIPIcs.SAT.2023.26,
  author =	{Tor\'{a}n, Jacobo and W\"{o}rz, Florian},
  title =	{{Cutting Planes Width and the Complexity of Graph Isomorphism Refutations}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{26:1--26:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18488},
  URN =		{urn:nbn:de:0030-drops-184884},
  doi =		{10.4230/LIPIcs.SAT.2023.26},
  annote =	{Keywords: Cutting Planes, Proof Complexity, Linear Programming, Combinatorial Optimization, Weisfeiler-Leman Algorithm, Graph Isomorphism}
}

Keywords: Cutting Planes, Proof Complexity, Linear Programming, Combinatorial Optimization, Weisfeiler-Leman Algorithm, Graph Isomorphism
Collection: 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
Issue Date: 2023
Date of publication: 09.08.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI