Pith. sign in

REVIEW 2 major objections 3 minor 61 references

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

T0 review · 2 major / 3 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Small formulas force proof depth beyond worst case, and the same trade-off hits circuits and graph algorithms.

desk verdict Strong and genuinely new trade-offs, but the main width-depth theorem as stated has a real off-by-one in the Cops-to-width reduction that needs fixing before the paper is final. read the letter →

arxiv 2411.14267 v1 pith:2QJIAYKG submitted 2024-11-21 cs.CC cs.LO

Susanna F. de Rezende , Noah Fleming , Duri Andrea Janett , Jakob Nordström , Shuo Pang This is my paper · ORCID
classification cs.CCcs.LO MSC 03F2068Q17
keywords resolutionproofcomplexitysupercriticaltrade-offscuttingplanesmonotonecircuitsWeisfeiler-LemanCop-RobbergameTseitinformulasliftingtheorems
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper establishes the first 'truly supercritical' trade-offs in proof complexity and circuit complexity: trade-offs measured against the size of the input formula, not merely against the number of variables. Its load-bearing result is a width-depth trade-off for resolution: for a range of parameters there is a linear-size 4-CNF formula that has a small-width, small-size refutation, yet every refutation of only slightly larger width must have depth $\Omega(n^k)$, far exceeding the linear worst-case upper bound. From this one theorem the authors derive supercritical size-depth trade-offs for cutting planes and resolution, supercritical width-size trade-offs for treelike resolution, and dimension-versus-iteration trade-offs for the Weisfeiler-Leman graph algorithm. Because the blow-up is measured against formula size, these lower bounds cannot be explained away by growing the number of variables. A reader should care because these are the first results of this strength for several models, and they show that small circuits and short proofs can be forced to pay super-linear or super-polynomial depth.

What carries the argument

The carrying mechanism is the compressed Cop-Robber game on a cylinder graph with $k$ rows and roughly $nk$ columns, where vertices on each row are identified periodically with a row-specific modulus. The Robber's survival strategy is organized around virtual cordons, the minimal vertex separators that respect the rows on which the Cops have at most one vertex. Proposition 4.10 shows that any two minimal virtual cordons of a set of at most $k+c$ Cops coincide on those unique rows, so all cordons lie in a column interval of length at most $2(k+c)-1$; the Robber uses this concentration to keep his distance for $\Omega(n^k)$ rounds. Separately, the lifting theorems convert the width-depth trade-off into size-depth trade-offs: the triangle-DAG lifting theorem covers each triangle of a search problem by strips of pre-structured rectangles, and a Full Image Lemma guarantees that each such rectangle yields a low-width clause.

What would settle it

Run the compressed Cop-Robber game on the cylinder from Section 3 with a small $k$, $c=2$, and row moduli chosen so that Property (P2) fails (for example, drop one prime factor from one modulus), and search for two minimal virtual cordons of a critical Cop set that differ by more than $2(k+c)-1$ columns. If such a pair exists, Proposition 4.10 fails and the Robber's $\Omega(n^k)$ survival strategy no longer has its geometric basis.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is Theorem 2.3: for any integers $3 \le c \le k-1 < n/(2 \ln n)$, there is a linear-size 4-CNF formula $F$ with between $2k^2 n^{c+1}$ and $40k^2(2n)^{c+1}$ variables, a resolution refutation of width $k+3$ and size $O(k^2(4n)^k)$, and the property that every refutation of width at most $k+c$ has depth $\Omega(n^k)$. This is the first truly supercritical width-depth trade-off for resolution that holds for an interval of widths rather than only at the minimum width. The formula is a parity-check (Tseitin) formula on a compressed cylinder graph, where edges are identified by a periodic equivalence relation; the paper calls this mechanism variable compression. By applying new lifting theorems, the authors translate this one trade-off into monotone (real) circuits of small size that need super-linear or super-polynomial depth, the first truly supercritical size-depth trade-offs for cutting planes and resolution, a truly supercritical width-size trade-off for treelike resolution, and Weisfeiler-Leman graph pairs distinguished in dimension $k$ yet requiring $\Omega(n^{k/(c+1)})$ iterations in dimension $k+c-1$. The paper also proves tighter lifting theorems, including a resolution lifting theorem based on random restrictions and a triangle-DAG lifting theorem that covers triangles by strips.

Load-bearing premise

The whole chain collapses if the Cops' barrier positions do not concentrate: the proof needs that any two minimal barriers of a critical Cop set agree on the rows where the Cops are alone, forcing all barriers into one column interval of length about $2(k+c)$; if that concentration fails, the Robber's distance invariant cannot last $\Omega(n^k)$ rounds.

Editorial extensions

If this is right

  • There are $N$-variate monotone functions computable in polynomial size such that any monotone real circuit of size at most $s^{1.4}$ needs depth at least $N^{2.4}$; with quasipolynomial size, any circuit of size at most $s\cdot \exp((\log N)^{1.9})$ needs super-polynomial depth.
  • There are 3-CNF formulas of polynomial size, refutable by resolution in polynomial size, such that every cutting planes refutation of size at most $S^{1.4}$ has depth at least $S^{2.4}$.
  • There are CNF formulas refutable in width $o(\log N)$ for which every treelike resolution refutation of width at most $1.4W$ has size at least $\exp(S^{2.4})$; a second choice of parameters gives size $\exp(S^{\omega(1)})$ at width $W + 40\log N/\log\log N$.
  • There are $n$-vertex graph pairs distinguished by $k$-dimensional Weisfeiler-Leman, while $(k+c-1)$-dimensional Weisfeiler-Leman needs $\Omega(n^{k/(c+1)})$ iterations; the standard translation turns this into a trade-off between number of variables and quantifier depth in first-order logic with counting.
  • The paper's lifting theorems, including the random-restriction lifting for resolution and the strip-based triangle-DAG lifting, are tight enough to use as black boxes and may be of independent interest.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The variable-compression scheme, replacing many edge variables with a few periodic class variables, may yield supercritical trade-offs in proof systems where XOR-condensation fails, such as polynomial calculus or stabbing planes.
  • Because the Weisfeiler-Leman trade-off holds across a range of dimensions and iteration counts, it should transfer to higher-order graph neural networks: the same graph pairs would require either higher order or many more message-passing rounds to distinguish.
  • The strip construction for triangle-DAGs does not use the arithmetic of cutting planes; it should also give size-depth trade-offs for semantic cutting planes with bounded coefficients, since it only needs shapes closed under intersections with rectangles.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 3 minor

Summary. The paper proves a new supercritical width-depth trade-off for resolution on compressed Tseitin formulas, obtained by refining the Cop-Robber game analysis of Grohe, Lichter, Neuen, and Schweitzer. Using new lifting theorems, the authors derive truly supercritical size-depth trade-offs for resolution and cutting planes, width-size trade-offs for treelike resolution, supercritical depth lower bounds for monotone real circuits, and trade-offs between dimension and iteration number for Weisfeiler-Leman. The central technical result, Theorem 2.3, states that for parameters 3 ≤ c ≤ k−1 < n/(2 ln n) there is a linear-size 4-CNF formula F with Θ(k^2 n^{c+1}) variables, refutable in width k+3 and size O(k^2(4n)^k), but every refutation of width at most k+c has depth Ω(n^k). The paper also contains new lifting theorems for resolution, treelike resolution, and triangle-DAGs, and a detailed translation to Weisfeiler-Leman via the CFI construction.

Significance. If the central theorem is repaired, this is a major contribution: it would give the first truly supercritical (formula-size-based) width-depth trade-off for resolution and the first truly supercritical size-depth trade-offs for cutting planes, together with new results for treelike resolution, monotone circuits, and Weisfeiler-Leman. The paper is technically detailed: the Cop-Robber analysis introduces virtual cordons, the lifting proofs are self-contained, and the CFI translation is written out in an appendix. However, my verification found a systematic off-by-one error in the reduction from resolution width to the Cop-Robber game that propagates to the main applications. The qualitative supercritical results appear salvageable, but the statements and proofs need correction before the paper can be accepted.

major comments (2)
  1. [§2.4 (Theorem 2.3), §3.3 (Lemma 3.14), §4 (Theorem 4.1)] The lower-bound direction of Theorem 2.3 is not a consequence of the stated Cop-Robber theorem. Lemma 3.14 converts a resolution refutation of width w and depth d into a winning strategy for w+1 Cops in d+1 rounds. Theorem 4.1 gives Robber survival for Ω(n^k) rounds against at most k+c Cops, so the contrapositive only rules out refutations of width at most (k+c)−1 = k+c−1, not width k+c. Therefore the claim in Theorem 2.3 that every refutation of width at most k+c has depth Ω(n^k) is not established. The same off-by-one makes Theorem 2.1 and Theorem 4.1 internally inconsistent at c=1: they assert both that k+1 Cops can win (in k rounds, by the proof of Theorem 4.1) and that the Robber survives against k+c = k+1 Cops. The parameter range should be corrected to c ≥ 2, or the survival statement should be against at most k+c−1 Cops.
  2. [§2.5 (Theorem 2.5), §2.6 (Theorems 2.8, 2.12, 2.13)] The applications inherit the off-by-one and require further parameter adjustment. In the proof of Theorem 2.5, the parameter is set to c := ⌊εk⌋−1, so the lower bound for F covers widths at most k+⌊εk⌋−1. However, a treelike refutation of width (m−1)(1+ε)k lifts, by Theorem 5.3, to a resolution refutation of F of width at most ⌊(1+ε)k⌋ = k+⌊εk⌋, which is one above the covered range. Hence the step 'by Theorem 2.3 implies log s = Ω(n^k)' does not follow as written. A repair by applying the Cop-Robber theorem with parameter c+1 changes the variable count in Theorem 2.3 to Θ(k^2 n^{c+2}), so the bounds 2k^2 n^{c+1} ≤ N ≤ 40k^2(2n)^{c+1} in Theorem 2.3 and the size thresholds in Theorems 2.8, 2.12, and 2.13 would need to be restated accordingly.
minor comments (3)
  1. [§4.1, Proposition 4.10] The proof contains a duplicated sentence: 'So ∆ = 0 and thus aj = bj for all j = 1, . . . , t, proving the proposition.' appears twice and should be reduced to a single occurrence.
  2. [Appendix B, Full Image Lemma] In the restatement of the lemma, the domain is written as {m}^n, which should be [m]^n.
  3. [§7.2, equation (7.13)] The equation uses 'C^{-1}(0)' where 'C_β^{-1}(0)' is meant; as written, it is unclear which clause's falsifying assignments are being denoted.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central trade-offs are derived from new Cop-Robber and lifting arguments rather than assumed from the target statements.

full rationale

The derivation chain is self-contained in the relevant sense. The central lower bound (Theorem 4.1) is a new Robber strategy proved explicitly from the parameter choice in Definition 3.9 via Propositions 4.6, 4.7, and 4.10, Lemma 4.11, and the invariant argument in Section 4.3; it does not assume the resolution trade-off it is used to prove. The translation from resolution refutations to Cop strategies (Lemma 3.14) is proved directly by simulating a refutation with Cops, and the upper bound (Lemma 3.13) is an explicit construction. The later lifting theorems (Theorems 2.4, 2.6, and 2.11) are proved within the paper, and the applications in Theorems 2.5, 2.8, 2.12, and 2.13 simply compose those lifting theorems with the width-depth trade-off. The external inputs, such as the CFI/Weisfeiler-Leman equivalence in [CFI92], the compression scheme of [GLNS23], and the Full Image Lemma argument of [LMM+22] and [FKNP21], are prior independent results rather than author-created assumptions of the present theorems. The paper's self-citations, chiefly [BN20] and [BN23], appear in introductory or related-work context and are not load-bearing for the new claims. No step was found in which a fitted parameter is renamed a prediction, an ansatz is smuggled in via citation, or a known result is merely renamed. An apparent parameter-range discrepancy between Lemma 3.14 (a width-w refutation gives a strategy for w+1 Cops) and Theorem 4.1 (survival against at most k+c Cops) is a potential correctness issue about the exact threshold in Theorem 2.3, but it is not circularity: the proof does not assume the conclusion it derives. Under the circularity rubric, the honest finding is no significant circularity.

Assumptions & free parameters 0 free parameters · 4 assumptions · 1 invented entities

The paper introduces no data-fitted free parameters; construction parameters such as k, c, n, m, and delta are quantified variables in theorem statements. The proof relies on standard background results in number theory, finite model theory, probability, and proof complexity. 'Virtual cordons' is the main new mathematical construct, used as an analysis tool rather than as a postulated physical entity.

assumptions (4)
  • standard math Prime number theorem ensures the existence of k pairwise coprime integers P_1, ..., P_k in [n, 2n] for sufficiently large n.
    Used in Definition 3.9 to construct the moduli m_i and length L of the cylinder graph; the lower bound requires Property 3.10, which follows from this choice.
  • standard math The CFI construction and the equivalence between k-dimensional Weisfeiler-Leman and the (k+1)-variable fragment of first-order logic with counting.
    Invoked in Appendix A to translate Cop-Robber lower bounds into Weisfeiler-Leman iteration lower bounds and into first-order logic quantifier depth trade-offs.
  • standard math Janson's inequality and the spread-family lemma of Frankston, Kahn, Narayanan and Park used in the Full Image Lemma.
    The Full Image Lemma underpins the triangle-DAG lifting theorem in Section 7, which is used for monotone circuits and cutting planes.
  • standard math Standard reductions between resolution refutations, rectangle-DAGs, monotone Karchmer-Wigderson relations, and monotone circuits (Fact 2.10).
    These reductions, attributed to Razborov and Gal, connect the proof complexity lower bounds to circuit and cutting planes lower bounds.
invented entities (1)
  • Virtual cordons
    purpose: Formalizes closures of Cop vertex separators to analyze the Robber's survival strategy in the compressed Cop-Robber game.
    Internal proof device introduced in Definition 4.8; it has no falsifiable handle outside the paper and is not an empirical entity.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Truly Supercritical Trade-offs for Resolution, Cutting Planes, Monotone Circuits, and Weisfeiler-Leman." pith.science (2026). https://pith.science/paper/2QJIAYKG

@misc{pith2026241114267,
  author       = {Pith},
  title        = {Pith review of: Truly Supercritical Trade-offs for Resolution, Cutting Planes, Monotone Circuits, and Weisfeiler-Leman},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2QJIAYKG}},
  note         = {Machine review of arXiv:2411.14267}
}
read the original abstract

We exhibit supercritical trade-off for monotone circuits, showing that there are functions computable by small circuits for which any circuit must have depth super-linear 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 we 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.

Figures

Figures reproduced from arXiv: 2411.14267 by the authors.

Figure 1
Figure 1. An illustration of trade-offs. Blue dots represent provable upper bounds on measures µ and ν. Proofs with measures in the shaded region are ruled out by the trade-off, where µworst and νworst are the worst-case upper bound on µ and ν, respectively. Figure 1a illustrates a non-supercritical trade-off and Figure 1b illustrates a supercritical one. 1.1 Supercritical Trade-offs in Circuit Complexity Perfect matching is … view at source ↗
Figure 2
Figure 2. Hardness condensation in Figure 2a substitutes the x-variables with an XOR over some y-variables, while variable compression in Figure 2b substitutes with y-variables directly. Note that m ≪ n. 1.4 Techniques Most of the previously known supercritical trade-offs are based on hardness condensation [Raz16], which works by substituting the variables of a problem instance with XOR gadgets over a much smaller set of vari… view at source ↗
Figure 3
Figure 3. The compression of two rows in the middle part is depicted. The parameters are chosen as L = P1 · P2 · P3 = 2 · 3 · 5, c = 1, m1 = P1 · P2 = 6, and m2 = P2 · P3 = 15. Equivalent vertical edges are drawn in the same color. are partitioned into 2(r − 1) + mi subsets: a singleton for each edge within the left or within the right part, and Hi(1), . . . , Hi(mi), where Hi(a) = {{x, x + 1} | x ∈ [r, r + L], x = a mod mi}.… view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: A special move P starting in column a is shown as the segmented path, where I is the underlying row set. Remark 4.3 (Periodic paths give special compressible moves). Suppose W is the set of vertices occu￾pied by Cops in the compressed game (Definition 3.11). If P is an…
Figure 5
Figure 5. Figure 5: The green circles are vertices in W≡ (i.e., they are in the equivalent classes of the Cops). The red and blue curves illustrate two minimal vertex separators contained in W≡. The yellow region represents all virtual cordons associated with W. Intuitively, the set of vi…
Figure 6
Figure 6. Figure 6: The structured rectangle Rin β for triangle T , whose quadrant Q is contained entirely within child T1. Applying Corollary 7.3 to Q, we get a row x ∗ ∈ QX ⊆ T X 1 such that IND({x ∗} × QY ) = C −1 β (0). As we have removed XT1 err and Y T1 err from T in the Error Remov…
Figure 7
Figure 7. Figure 7: A strip S of a triangle, including two pre-structured rectangles Rξ, Rβ, a set of error columns Y S err, and an example of a secured row. We first argue that the error, security and maximality properties of the Triangle Lemma hold. The error property holds by construct…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

61 extracted references · 60 canonical work pages

  1. [1]

    Noga Alon and Ravi B. Boppana. The monotone circuit complexity of B oolean functions. Combinatorica , 7(1):1 --22, March 1987

    work page 1987

  2. [2]

    Alexander E. Andreev. On a method for obtaining lower bounds for the complexity of individual monotone functions. Soviet Mathematics Doklady , 31(3):530 --534, 1985. E nglish translation of a paper in Doklady Akademii Nauk SSSR

    work page 1985

  3. [3]

    Graph isomorphism in quasipolynomial time [extended abstract]

    L \' a szl \' o Babai. Graph isomorphism in quasipolynomial time [extended abstract]. In Proceedings of the 48th Annual ACM Symposium on Theory of Computing ( STOC '16) , pages 684 --697, June 2016

    work page 2016

  4. [4]

    Time-space tradeoffs in resolution: Superpolynomial lower bounds for superlinear space

    Paul Beame, Chris Beck, and Russell Impagliazzo. Time-space tradeoffs in resolution: Superpolynomial lower bounds for superlinear space. SIAM Journal on Computing , 45(4):1612 --1645, August 2016. Preliminary version in STOC '12

    work page 2016

  5. [5]

    On the complexity of finding narrow proofs

    Christoph Berkholz. On the complexity of finding narrow proofs. In Proceedings of the 53rd Annual IEEE Symposium on Foundations of Computer Science ( FOCS '12) , pages 351 --360, October 2012

    work page 2012

  6. [6]

    Stabbing planes

    Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere. Stabbing planes. In Proceedings of the 9th Innovations in Theoretical Computer Science Conference ( ITCS '18) , volume 94 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 10:1 --10:20, January 2018

    work page 2018

  7. [7]

    Rank bounds and integrality gaps for cutting planes procedures

    Joshua Buresh-Oppenheim , Nicola Galesi, Shlomo Hoory, Avner Magen, and Toniann Pitassi. Rank bounds and integrality gaps for cutting planes procedures. Theory of Computing , 2(4):65 --90, 2006. Preliminary version in FOCS '03

    work page 2006

  8. [8]

    Supercritical size-width tree-like resolution trade-offs for graph isomorphism

    Christoph Berkholz, Moritz Lichter, and Harry Vinall-Smeeth. Supercritical size-width tree-like resolution trade-offs for graph isomorphism. arXiv preprint arXiv 2407.17947 , July 2024

    arXiv 2024

Show all 61 references
  1. [9]

    Supercritical space-width trade-offs for resolution

    Christoph Berkholz and Jakob Nordström. Supercritical space-width trade-offs for resolution. SIAM Journal on Computing , 49(1):98 --118, February 2020. Preliminary version in ICALP '16

    2020

  2. [10]

    Buss and Jakob Nordström

    Samuel R. Buss and Jakob Nordström. Proof complexity and SAT solving. In Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability , volume 336 of Frontiers in Artificial Intelligence and Applications , chapter 7, pages 233 --350. IO...

    2021

  3. [11]

    Near-optimal lower bounds on quantifier depth and W eisfeiler- L eman refinement steps

    Christoph Berkholz and Jakob Nordström. Near-optimal lower bounds on quantifier depth and W eisfeiler- L eman refinement steps. Journal of the ACM , 70(5):32:1 --32:32, October 2023. Preliminary version in LICS '16

    2023

  4. [12]

    Some trade-off results for polynomial calculus

    Chris Beck, Jakob Nordström, and Bangsheng Tang. Some trade-off results for polynomial calculus. In Proceedings of the 45th Annual ACM Symposium on Theory of Computing ( STOC '13) , pages 813 --822, May 2013

    2013

  5. [13]

    Propositional proof complexity: Past, present, and future

    Paul Beame and Toniann Pitassi. Propositional proof complexity: Past, present, and future. Bulletin of the European Association for Theoretical Computer Science , 65:66 --89, June 1998

    1998

  6. [14]

    Lower bounds for cutting planes proofs with small coefficients

    Mar \'i a Bonet, Toniann Pitassi, and Ran Raz. Lower bounds for cutting planes proofs with small coefficients. In Proceedings of the 27th Annual ACM Symposium on Theory of Computing ( STOC '95) , pages 575 --584, May 1995

    1995

  7. [15]

    A simple supercritical tradeoff between size and height in resolution

    Sam Buss and Neil Thapen. A simple supercritical tradeoff between size and height in resolution. Technical Report TR24-001, Electronic Colloquium on Computational Complexity (ECCC), January 2024

    2024

  8. [16]

    Super-critical trade-offs in resolution over parities via lifting

    Arkadev Chattopadhyay and Pavel Dvo r \' a k. Super-critical trade-offs in resolution over parities via lifting. Technical Report TR24-132, Electronic Colloquium on Computational Complexity (ECCC), September 2024

    2024

  9. [17]

    An optimal lower bound on the number of variables for graph identifications

    Jin - yi Cai, Martin F \" u rer, and Neil Immerman. An optimal lower bound on the number of variables for graph identifications. Combinatorica , 12(4):389 --410, 1992. Preliminary version in FOCS '89

    1992

  10. [18]

    Edmonds polytopes and a hierarchy of combinatorial problems

    Va s ek Chv \'a tal. Edmonds polytopes and a hierarchy of combinatorial problems. Discrete Mathematics , 4(1):305 --337, 1973

    1973

  11. [19]

    On the complexity of branching proofs

    Daniel Dadush and Samarth Tiwari. On the complexity of branching proofs. In Proceedings of the 35th Annual Computational Complexity Conference ( CCC '20) , volume 169 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 34:1 --34:35, July 2020

    2020

  12. [20]

    Paths, trees, and flowers

    Jack Edmonds. Paths, trees, and flowers. Canadian Journal of Mathematics , 17:449 --467, 1965

    1965

  13. [21]

    On the power and limitations of branch and cut

    Noah Fleming, Mika Göös, Russell Impagliazzo, Toniann Pitassi, Robert Robere, Li-Yang Tan, and Avi Wigderson. On the power and limitations of branch and cut. In Proceedings of the 36th Annual Computational Complexity Conference ( CCC '21) , volume 200 of Leibniz International ...

    2021

  14. [22]

    Thresholds versus fractional expectation-thresholds

    Keith Frankston, Jeff Kahn, Bhargav Narayanan, and Jinyoung Park. Thresholds versus fractional expectation-thresholds. Annals of Mathematics , 194(2):475--495, September 2021

    2021

  15. [23]

    Reflections on proof complexity and counting principles

    Noah Fleming and Toniann Pitassi. Reflections on proof complexity and counting principles. In Ivo D\" u nsch and Edwin Mares, editors, Alasdair Urquhart on Nonclassical and Algebraic Logic and Complexity of Proofs , volume 22 of Outstanding Contributions to Logic , chapter 18,...

    2022

  16. [24]

    Random ( n) - CNFs are hard for cutting planes

    Noah Fleming, Denis Pankratov, Toniann Pitassi, and Robert Robere. Random ( n) - CNFs are hard for cutting planes. Journal of the ACM , 69(3):19:1 --19:32, June 2022. Preliminary version in FOCS '17

    2022

  17. [25]

    Extremely deep proofs

    Noah Fleming, Toniann Pitassi, and Robert Robere. Extremely deep proofs. In Proceedings of the 13th Innovations in Theoretical Computer Science Conference ( ITCS '22) , pages 70:1 --70:23. Schloss Dagstuhl-Leibniz-Zentrum f \"u r Informatik, January 2022

    2022

  18. [26]

    W eisfeiler- L ehman refinement requires at least a linear number of iterations

    Martin F \" u rer. W eisfeiler- L ehman refinement requires at least a linear number of iterations. In Proceedings of the 28th International Colloquium on Automata, Languages and Programming ( ICALP '01) , volume 2076 of Lecture Notes in Computer Science , pages 322 --333. Spr...

    2001

  19. [27]

    A characterization of span program size and improved lower bounds for monotone span programs

    Anna G \'a l. A characterization of span program size and improved lower bounds for monotone span programs. Computational Complexity , 10(4):277 --296, December 2001. Preliminary version in STOC '98

    2001

  20. [28]

    Monotone circuit lower bounds from resolution

    Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov. Monotone circuit lower bounds from resolution. Theory of Computing , 16(13):1 --30, 2020. Preliminary version in STOC '18

    2020

  21. [29]

    Rectangles are nonnegative juntas

    Mika Göös, Shachar Lovett, Raghu Meka, Thomas Watson, and David Zuckerman. Rectangles are nonnegative juntas. SIAM Journal on Computing , 45(5):1835 --1869, October 2016. Preliminary version in STOC '15

    2016

  22. [30]

    The iteration number of the W eisfeiler- L eman algorithm

    Martin Grohe, Moritz Lichter, and Daniel Neuen. The iteration number of the W eisfeiler- L eman algorithm. In Proceedings of the 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '23) , pages 1 --13, June 2023

    2023

  23. [31]

    Compressing CFI graphs and lower bounds for the W eisfeiler- L eman refinements

    Martin Grohe, Moritz Lichter, Daniel Neuen, and Pascal Schweitzer. Compressing CFI graphs and lower bounds for the W eisfeiler- L eman refinements. In Proceedings of the 64th Annual IEEE Symposium on Foundations of Computer Science ( FOCS '23) , pages 798 --809, November 2023

    2023

  24. [32]

    Supercritical tradeoffs for monotone circuits

    Mika G\" o \" o s, Gilbert Maystre, Kilian Risse, and Dmitry Sokolov. Supercritical tradeoffs for monotone circuits. Technical report, November 2024

    2024

  25. [33]

    Rank logic is dead, long live rank logic! The Journal of Symbolic Logic , 84(1):54--87, March 2019

    Erich Gr \"a del and Wied Pakusa. Rank logic is dead, long live rank logic! The Journal of Symbolic Logic , 84(1):54--87, March 2019. Preliminary version in CSL '15

    2019

  26. [34]

    The logic of graph neural networks

    Martin Grohe. The logic of graph neural networks. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science ( LICS '21) , pages 1 --17, June 2021

    2021

  27. [35]

    Cops-robber games and the resolution of T seitin formulas

    Nicola Galesi, Navid Talebanfard, and Jacobo Tor \'a n. Cops-robber games and the resolution of T seitin formulas. ACM Transactions on Computation Theory (TOCT) , 12(2):1--22, May 2020. Preliminary version in SAT '18

    2020

  28. [36]

    Random formulas, monotone circuits, and interpolation

    Pavel Hrube s and Pavel Pudl \'a k. Random formulas, monotone circuits, and interpolation. In Proceedings of the 58th Annual IEEE Symposium on Foundations of Computer Science ( FOCS '17) , pages 121 --131, October 2017

    2017

  29. [37]

    Describing graphs: A first-order approach to graph canonization

    Neil Immerman and Eric Lander. Describing graphs: A first-order approach to graph canonization. In Alan L. Selman, editor, Complexity Theory Retrospective: In Honor of Juris Hartmanis on the Occasion of His Sixtieth Birthday, July 5, 1988 , pages 59--81. Springer, June 1990

    1988

  30. [38]

    Boolean Function Complexity - Advances and Frontiers , volume 27 of Algorithms and combinatorics

    Stasys Jukna. Boolean Function Complexity - Advances and Frontiers , volume 27 of Algorithms and combinatorics . Springer, 2012

    2012

  31. [39]

    The W eisfeiler- L eman algorithm: an exploration of its power

    Sandra Kiefer. The W eisfeiler- L eman algorithm: an exploration of its power. ACM SIGLOG News , 7(3):5 --27, July 2020

    2020

  32. [40]

    Proof Complexity , volume 170 of Encyclopedia of Mathematics and Its Applications

    Jan Kraj \' c ek. Proof Complexity , volume 170 of Encyclopedia of Mathematics and Its Applications . Cambridge University Press, March 2019

    2019

  33. [41]

    Upper bounds on the quantifier depth for graph differentiation in first order logic

    Sandra Kiefer and Pascal Schweitzer. Upper bounds on the quantifier depth for graph differentiation in first order logic. Logical Methods in Computer Science , 15(2):19:1 --19:19, May 2019. Preliminary version in LICS '16

    2019

  34. [42]

    Monotone circuits for connectivity require super-logarithmic depth

    Mauricio Karchmer and Avi Wigderson. Monotone circuits for connectivity require super-logarithmic depth. SIAM Journal on Discrete Mathematics , 3(2):255 --265, 1990. Preliminary version in STOC '88

    1990

  35. [43]

    Lifting with Sunflowers

    Shachar Lovett, Raghu Meka, Ian Mertz, Toniann Pitassi, and Jiapeng Zhang. Lifting with Sunflowers . In Proceedings of the 13th Innovations in Theoretical Computer Science Conference ( ITCS '22) , volume 215 of Leibniz International Proceedings in Informatics (LIPIcs) , pages ...

    2022

  36. [44]

    Walk refinement, walk logic, and the iteration number of the W eisfeiler- L eman algorithm

    Moritz Lichter, Ilia Ponomarenko, and Pascal Schweitzer. Walk refinement, walk logic, and the iteration number of the W eisfeiler- L eman algorithm. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science ( LICS '19) , pages 1 --13, June 2019

    2019

  37. [45]

    Kriege, Martin Grohe, Matthias Fey, and Karsten Borgwardt

    Christopher Morris, Yaron Lipman, Haggai Maron, Bastian Rieck, Nils M. Kriege, Martin Grohe, Matthias Fey, and Karsten Borgwardt. Weisfeiler and leman go machine learning: The story so far. Journal of Machine Learning Research , 24(333):1 --59, 2023

    2023

  38. [46]

    Hamilton, Jan Eric Lenssen, Gaurav Rattan, and Martin Grohe

    Christopher Morris, Martin Ritzert, Matthias Fey, William L. Hamilton, Jan Eric Lenssen, Gaurav Rattan, and Martin Grohe. Weisfeiler and leman go neural: Higher-order graph neural networks. In Proceedings of the 23rd AAAI Conference on Artificial Intelligence ( AAAI '19) , pag...

    2019

  39. [47]

    Lower bounds for resolution and cutting plane proofs and monotone computations

    Pavel Pudl\' a k. Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic , 62(3):981 --998, September 1997

    1997

  40. [48]

    On extracting computations from propositional proofs (a survey)

    Pavel Pudl\' a k. On extracting computations from propositional proofs (a survey). In Proceedings of the 30th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science ( FSTTCS '10) , volume 8 of Leibniz International Proceedings in Informa...

    2010

  41. [49]

    Coding for sunflowers

    Anup Rao. Coding for sunflowers. Discrete Analysis , February 2020

    2020

  42. [50]

    Razborov

    Alexander A. Razborov. Lower bounds for the monotone complexity of some Boolean functions. Soviet Mathematics Doklady , 31(2):354 --357, 1985. E nglish translation of a paper in Doklady Akademii Nauk SSSR

    1985

  43. [51]

    Razborov

    Alexander A. Razborov. Applications of matrix methods to the theory of lower bounds in computational complexity. Combinatorica , 10(1):81 --93, March 1990

    1990

  44. [52]

    Razborov

    Alexander A. Razborov. Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic. Izvestiya: Mathematics , 59:205--227, February 1995

    1995

  45. [53]

    Razborov

    Alexander A. Razborov. A new kind of tradeoffs in propositional proof complexity. Journal of the ACM , 63(2):16:1 --16:14, April 2016

    2016

  46. [54]

    Razborov

    Alexander A. Razborov. On the width of semialgebraic proofs and algorithms. Mathematics of Operations Research , 42(4):1106 --1134, May 2017

    2017

  47. [55]

    Razborov

    Alexander A. Razborov. On space and depth in resolution. Computational Complexity , 27(3):511 --559, September 2018

    2018

  48. [56]

    Monotone circuits for matching require linear depth

    Ran Raz and Avi Wigderson. Monotone circuits for matching require linear depth. Journal of the ACM , 39(3):736 --744, July 1992

    1992

  49. [57]

    Dag-like communication and its applications

    Dmitry Sokolov. Dag-like communication and its applications. In Proceedings of the 12th International Computer Science Symposium in Russia ( CSR '17) , volume 10304 of Lecture Notes in Computer Science , pages 294 --307. Springer, June 2017

    2017

  50. [58]

    Random ( n) - CNF are hard for cutting planes (again)

    Dmitry Sokolov. Random ( n) - CNF are hard for cutting planes (again). In Proceedings of the 56th Annual ACM Symposium on Theory of Computing ( STOC '24) , pages 2008 --–2015, June 2024

    2008

  51. [59]

    Graph searching and a min-max theorem for tree-width

    Paul D Seymour and Robin Thomas. Graph searching and a min-max theorem for tree-width. Journal of Combinatorial Theory, Series B , 58(1):22--33, May 1993

    1993

  52. [60]

    On the complexity of derivation in propositional calculus

    Grigori Tseitin. On the complexity of derivation in propositional calculus. In A. O. Silenko, editor, Structures in Constructive Mathematics and Mathematical Logic, Part II , pages 115 --125. Consultants Bureau, New York-London, 1968

    1968

  53. [61]

    A reduction of a graph to a canonical form and an algebra arising during this reduction

    Boris Weisfeiler and Andrei Leman. A reduction of a graph to a canonical form and an algebra arising during this reduction. Nauchno-Technicheskaya Informatsiya, Ser. 2 , 9:12 --16, 1968. English translation by G rigory R yabov available at https://www.iti.zcu.cz/wl2018/pdf/wl_...

    1968

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.