Truly supercritical trade-offs for resolution, cutting planes, monotone circuits, and Weisfeiler-Leman
(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)
- author
- De Rezende, Susanna F.
LU
; Fleming, Noah ; Janett, Duri Andrea ; Nordström, Jakob LU and Pang, Shuo
- organization
- publishing date
- 2025-06-15
- 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
- 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-07-31 17:46:14
@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 & 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}}, month = {{06}}, pages = {{1371--1382}}, publisher = {{Association for Computing Machinery}}, 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}}, }