Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Truly Supercritical Trade-Offs for Resolution, Cutting Planes, Monotone Circuits, and Weisfeiler–Leman

De Rezende, Susanna F. LU orcid ; Fleming, Noah LU orcid ; Janett, Duri Andrea ; Nordström, Jakob LU and Pang, Shuo (2025) 57th Annual ACM Symposium on Theory of Computing, STOC 2025 In Proceedings of the Annual ACM Symposium on Theory of Computing p.1371-1382
Abstract

We exhibit supercritical trade-off for monotone circuits, showing that there are functions computable by small circuits for which any small circuit must have depth superlinear or even super-polynomial in the number of variables, far exceeding the linear worst-case upper bound. We obtain similar trade-offs in proof complexity, where we establish the first size-depth trade-offs for cutting planes and resolution that are truly supercritical, i.e., in terms of formula size rather than number of variables, and also show supercritical trade-offs between width and size for treelike resolution. Our results build on a new supercritical width-depth trade-off for resolution, obtained by refining and strengthening the compression scheme for the... (More)

We exhibit supercritical trade-off for monotone circuits, showing that there are functions computable by small circuits for which any small circuit must have depth superlinear or even super-polynomial in the number of variables, far exceeding the linear worst-case upper bound. We obtain similar trade-offs in proof complexity, where we establish the first size-depth trade-offs for cutting planes and resolution that are truly supercritical, i.e., in terms of formula size rather than number of variables, and also show supercritical trade-offs between width and size for treelike resolution. Our results build on a new supercritical width-depth trade-off for resolution, obtained by refining and strengthening the compression scheme for the cop-robber game in [Grohe, Lichter, Neuen & Schweitzer 2023]. This yields robust supercritical trade-offs for dimension versus iteration number in the Weisfeiler-Leman algorithm, which also translate into trade-offs between number of variables and quantifier depth in first-order logic. Our other results follow from improved lifting theorems that might be of independent interest.

(Less)
Please use this url to cite or link to this publication:
author
; ; ; and
organization
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
keywords
Cutting planes, Monotone circuit complexity, Proof complexity, Resolution, Supercritical trade-off, Weisfeiler-Leman algorithm
host publication
STOC 2025 - Proceedings of the 57th Annual ACM Symposium on Theory of Computing
series title
Proceedings of the Annual ACM Symposium on Theory of Computing
editor
Koucky, Michal and Bansal, Nikhil
pages
12 pages
publisher
Association for Computing Machinery (ACM)
conference name
57th Annual ACM Symposium on Theory of Computing, STOC 2025
conference location
Prague, Czech Republic
conference dates
2025-06-23 - 2025-06-27
external identifiers
  • scopus:105009775763
ISSN
0737-8017
ISBN
9798400715105
DOI
10.1145/3717823.3718271
language
English
LU publication?
yes
id
c06c7aae-3109-4212-bd19-e7c6c9fff35c
date added to LUP
2025-07-14 13:18:35
date last changed
2025-11-06 08:49:46
@inproceedings{c06c7aae-3109-4212-bd19-e7c6c9fff35c,
  abstract     = {{<p>We exhibit supercritical trade-off for monotone circuits, showing that there are functions computable by small circuits for which any small circuit must have depth superlinear or even super-polynomial in the number of variables, far exceeding the linear worst-case upper bound. We obtain similar trade-offs in proof complexity, where we establish the first size-depth trade-offs for cutting planes and resolution that are truly supercritical, i.e., in terms of formula size rather than number of variables, and also show supercritical trade-offs between width and size for treelike resolution. Our results build on a new supercritical width-depth trade-off for resolution, obtained by refining and strengthening the compression scheme for the cop-robber game in [Grohe, Lichter, Neuen &amp; Schweitzer 2023]. This yields robust supercritical trade-offs for dimension versus iteration number in the Weisfeiler-Leman algorithm, which also translate into trade-offs between number of variables and quantifier depth in first-order logic. Our other results follow from improved lifting theorems that might be of independent interest.</p>}},
  author       = {{De Rezende, Susanna F. and Fleming, Noah and Janett, Duri Andrea and Nordström, Jakob and Pang, Shuo}},
  booktitle    = {{STOC 2025 - Proceedings of the 57th Annual ACM Symposium on Theory of Computing}},
  editor       = {{Koucky, Michal and Bansal, Nikhil}},
  isbn         = {{9798400715105}},
  issn         = {{0737-8017}},
  keywords     = {{Cutting planes; Monotone circuit complexity; Proof complexity; Resolution; Supercritical trade-off; Weisfeiler-Leman algorithm}},
  language     = {{eng}},
  pages        = {{1371--1382}},
  publisher    = {{Association for Computing Machinery (ACM)}},
  series       = {{Proceedings of the Annual ACM Symposium on Theory of Computing}},
  title        = {{Truly Supercritical Trade-Offs for Resolution, Cutting Planes, Monotone Circuits, and Weisfeiler–Leman}},
  url          = {{http://dx.doi.org/10.1145/3717823.3718271}},
  doi          = {{10.1145/3717823.3718271}},
  year         = {{2025}},
}