Pith. sign in

REVIEW 3 major objections 3 minor 44 references

Supercritical Tradeoffs for Monotone Circuits

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

Pith's one-line read The paper constructs a monotone function computable in quasipolynomial size for which every polynomial-depth monotone circuit needs exponential size.

desk verdict First supercritical monotone circuit tradeoff via a new bracket-formula width-depth lower bound; the proof is intricate but the stress-test holds, so this deserves serious refereeing. read the letter →

arxiv 2411.14268 v1 pith:N545RHQV submitted 2024-11-21 cs.CC

classification cs.CC MSC 68Q1703F20
keywords monotonecircuitssize-depthtradeoffresolutionproofcomplexitybracketformulassupercriticalwidth-depthliftingprover-adversarygames
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

The paper proves a supercritical size–depth tradeoff for monotone circuits: there is a monotone function f that some monotone circuit computes in quasipolynomial size, yet every monotone circuit of polynomial depth needs exponential size. This is the first result of this kind in the regime where the allowed depth is well above the critical value, and it answers a conjecture from earlier work even though it does not yet reach the conjectured quantitative parameters. The proof goes through proof complexity: the paper introduces a new family of unsatisfiable 3-CNF formulas, the bracket formulas, that have quasipolynomial-size resolution refutations but require exponential size for any polynomial-depth refutation. A lifting theorem then carries that tradeoff from resolution to monotone circuits.

What carries the argument

The load-bearing object is the bracket formula Brn, a 3-CNF encoding of the bracket principle using pointer variables that name each bracket's mate; a well-parenthesised string is forced to contain the forbidden substring ][. The proof works in the prover–adversary game characterization of resolution width and depth. The upper bound is a recursive prover strategy that queries and forgets whole bracket pairs, keeping only O(log n) symbols in memory. The lower bound is an adversary strategy maintaining a 'container', a minimal monotone set of top-level bracket pairs that dominates the game state; nested recursion, buffer intervals, and the Cover, Size, and Buffer Lemmas bound how many indices the container may cover. Finally, dag-like lifting theorems from resolution to monotone circuits convert the width–depth tradeoff into size–depth tradeoffs.

What would settle it

Run the resolution game on the bracket formula with memory about $n^{{1/3}}$ and count the rounds: if the prover can force a falsified axiom in fewer than $n^{{Ω(log n / log w)}}$ rounds, the width–depth lower bound is false, and since the circuit tradeoff is derived from it by lifting, the main circuit theorem would fall as well.

Watch

Extended reading notes

Core claim

The central claim is that a simple combinatorial principle about brackets—every red/blue well-parenthesised string starting with a red bracket and ending with a blue bracket must contain the substring ][—can be encoded as a 3-CNF that is easy to refute in width but hard to refute in depth. Concretely, the bracket formula Brn admits a resolution refutation of width O(log n), and every width-w resolution refutation of Brn has depth $n^{{Ω(log n/log w)}}$. Lifting theorems then turn this width–depth tradeoff into the main circuit theorem: a monotone function computable in size $n^{{O(log n)}}$ such that every depth-$n^{{O(1)}}$ monotone circuit computing it has size exp($n^{{Ω(1)}}$). The same argument yields the analogous size–depth tradeoff for resolution, with the lower bound actually holding for semantic cutting planes as well.

Load-bearing premise

The lower bound rests on the recursive adversary maintaining a minimal 'container' of the game state, together with the Cover, Size, and Buffer Lemmas that bound how many positions that container covers; if those interval-area estimates are off, the exponential depth lower bound collapses.

Editorial extensions

If this is right

  • Every polynomial-depth monotone circuit for the exhibited function needs size exp(n^{Ω(1)}), so polynomial depth does not buy small size in the supercritical regime.
  • The bracket formulas give the first resolution size–depth tradeoff for a genuine 3-CNF, avoiding the quasipolynomial-clause limitation of prior tradeoffs.
  • The same lifting route yields an analogous size–depth tradeoff for cutting planes refutations.
  • Because the depth lower bound holds for every width w, the proof also yields a width–depth tradeoff: refuting Brn at width w requires depth n^{Ω(log n/log w)}.
  • The gap in the circuit result is from quasipolynomial size in the unrestricted-depth upper bound to exponential size under any polynomial depth restriction.

Reading between the lines

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

  • Beyond the paper: the natural strengthening is to make the blow-up occur already at depth S^ε, where S is the quasipolynomial size of the efficient circuit; the conjecture from earlier work asks for exactly this, and the bracket-formula construction does not obviously obstruct it.
  • Beyond the paper: the bracket principle is known to sit between the TFNP classes UEOPL and EOPL, and the paper's low-width refutation shows the principle is easy in a PLS-like sense; classifying whether the principle is complete for any named class would tie these proof-complexity tradeoffs to search problems.
  • Beyond the paper: the paper leaves open whether bracket formulas can give Weisfeiler–Leman refinements analogous to those obtained from condensed Tseitin formulas; testing the bracket formulas in that setting is a concrete transfer question.
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

3 major / 3 minor

Summary. The paper proves a supercritical size-depth tradeoff for monotone circuits: it exhibits a monotone function f on n bits that is computable by monotone circuits of quasipolynomial size, while every monotone circuit of polynomial depth computing f requires exponential size. The proof goes through a new family of unsatisfiable 3-CNF formulas, called bracket formulas Br_n. The authors show that Br_n has resolution refutations of width O(log n) (Section 3) and, by a recursive prover-adversary strategy maintaining containers and buffers, that every width-w resolution refutation of Br_n has depth n^{Omega(log n / log w)} (Section 4). These width-depth tradeoffs are then lifted through known dag-like lifting theorems to size-depth tradeoffs for resolution and, ultimately, to the monotone circuit result (Section 5). The paper also discusses the relationship of bracket formulas to TFNP classes and compares the result with concurrent work.

Significance. If the proofs are completed as intended, this is an important result: it is the first supercritical size-depth tradeoff for monotone circuits, resolving a direction conjectured in prior work, and it introduces a clean new combinatorial principle that may be of independent interest. The paper is careful to state exactly how its parameters compare with the stronger conjectures and with the concurrent work of de Rezende et al. The upper-bound argument and the overall lifting architecture are clear. The main lower-bound proof in Section 4 is intricate and not machine-checked; in its current written form it contains a miscomputed estimate and a missing implication in the last lifting step, so I cannot recommend acceptance without revision.

major comments (3)
  1. [Section 5, proof of Theorem 1] The step 'For small delta this contradicts Theorem 2' is not justified as written. Theorem 21 applied to F := Br_n yields a resolution refutation Pi of Br_n, whereas Theorem 2 is a lower bound for the composed formula Br_n composed with the indexing gadget. No statement in the paper converts a shallow and small resolution proof of Br_n into a shallow and small resolution proof of that composed formula: Claim 20 controls only size, not depth, and the alternative route of applying Theorem 21 directly to the composed formula is not what is written. This is a load-bearing gap for the monotone circuit lower bound. Please either insert an explicit depth-preserving (and, where needed, width-preserving) simulation lemma for composition with the indexing gadget, or restructure the proof to apply Theorem 21 to Br_n composed with Ind and then invoke Theorem 19.
  2. [Section 4.3, Eq. (4)] The displayed bound A_l <= O(d^{ell0} w^{ell0}) = O(n^{3 epsilon}) does not follow from the recurrence A_l = w(A_{l+1} + 3d), A_{ell0} = 3d. Solving the recurrence gives A_l = O(d * w^{ell0 - l}), which with the stated parameters is O(n^{2 epsilon}) at l = 0; the term d^{ell0} is not polynomial in n. Since Eq. (4) is used in the Size Lemma to guarantee |I_i| >= n/(4w)^{ell+1}, the estimate must be corrected (or proved by a different induction) before the proof of Lemma 12 can be considered complete. The intended estimate is probably sufficient, but the written bound is false.
  3. [Section 4.2, Lemma 11] The proof of Lemma 11 says 'By construction it should be evident' and leaves the main invariant (that the maintained interval I is a subinterval of the separation interval and that Move preserves the domination of the game state rho) largely informal. Because the container invariant is what prevents the prover from winning, the induction should be stated with explicit invariant conditions and a precise definition of the failure condition. This may be a presentation issue rather than an error, but as written it makes the correctness of the adversary strategy difficult to verify.
minor comments (3)
  1. [Section 5, proof of Theorem 2] The symbol n is used both for the number of variables of Br_n and for the number of variables of the composed formula Br_n composed with Ind, which has about n^{2+epsilon} variables. The proof should state the final lower bound with explicit variable counts or a reparameterization, so that width n^delta / log n and depth n^{gamma + delta / log n} are not ambiguous.
  2. [Section 4.3, Lemma 17] In the proof of Lemma 17, the sentence about adding 'all trivial bracket pairs in tilde C_i' to the set U should say that the areas of those trivial pairs are added; otherwise the size bound |U_{i+1}| <= 3w is not immediate.
  3. [Section 4.3, Size Lemma] In Eq. (3) and the surrounding text, tilde I_i and I_i are used somewhat interchangeably; the distinction between the interval found before the Move operation and the interval after the Move operation should be made explicit, and Eq. (5) should be checked against Algorithm 1.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: bracket formulas and their width–depth tradeoff are developed from first principles; external lifting theorems are independent published results.

full rationale

The derivation chain is: define bracket formulas Brn (Section 2); prove upper-bound width O(log n) (Theorem 3, Section 3); prove lower bound on depth for width-w refutations (Theorem 4, Sections 4.1–4.4); apply pre-existing dag-like lifting theorems (Theorems 19 and 21, cited to GGKS20/LMM+/FPR22) to get resolution and monotone-circuit size–depth tradeoffs. The only inputs shared with the target results are the formula family itself; Theorem 4 is not obtained by assuming the tradeoff it is used to prove. The lifting theorems are stated as imported results from earlier literature (including GGKS20, whose author list overlaps with the present paper), but they are fixed independent theorems with proofs published elsewhere and are not derived from the bracket formulas or from Theorems 1–2. Thus the self-overlap is not load-bearing in a circular way. The recursive adversary lower bound rests on internal Cover/Size/Buffer Lemmas (Lemmas 12, 13, 15), which are proved by induction and area estimates; even if the bound in Eq. (4) is written loosely as O(n^{3ε}) rather than the tighter O(n^{2ε}) obtained from recurrence A_ell = w(A_{ell+1}+3d), that slack does not make Theorem 4 equivalent to an input. No fitted parameter is relabelled as a prediction, no ansatz is imported solely to force uniqueness, and the bracket principle is not a renaming of a previously known tradeoff. Result: no significant circularity found.

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

No free parameters are fitted to data; the constants ε and δ are arbitrary small constants used in the asymptotic statements. The proofs rely on standard results from proof complexity and the lifting theorems, which are cited but not re-proved. The bracket formulas are introduced as a new construction but are not postulated entities in the sense of unexplained objects.

free parameters (2)
  • epsilon in Theorem 19 parameters = any constant in (0,1)
    Used in Section 4.2 to set recursion depth ℓ0 = ⌊ε log n / log w⌋ and iteration count d = ⌊n^ε⌋. The proof works for any sufficiently small ε, so it is a hand-chosen parameter rather than a fitted value.
  • delta in size bound 2^{n^δ} = small positive constant
    Used in the contradiction proofs of Theorems 2 and 1. The result holds for all sufficiently small δ, so it is a hand-chosen constant.
assumptions (4)
  • standard math Resolution width-size relation: any width-w resolution refutation has size n^{O(w)}
    Used in Section 5 to derive the size upper bound (i') in Theorem 2 from the width upper bound in Theorem 3.
  • standard math Prover-adversary game characterization of resolution width and depth (Pudlak 2000, Atserias-Dalmau 2008)
    Used throughout Sections 3 and 4 to prove Theorems 3 and 4 via games.
  • domain assumption Dag-like lifting theorem for resolution (Theorem 19, from GGKS20, LMM+22, FPR22)
    Used in Section 5 to translate size-depth tradeoffs for composed formulas into resolution width-depth tradeoffs. Not proved in this paper.
  • domain assumption Dag-like lifting theorem for monotone circuits (Theorem 21, from GGKS20, LMM+22, FPR22)
    Used in Section 5 to convert resolution refutations of the bracket formula into monotone circuit bounds. Not proved in this paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Supercritical Tradeoffs for Monotone Circuits." pith.science (2026). https://pith.science/paper/N545RHQV

@misc{pith2026241114268,
  author       = {Pith},
  title        = {Pith review of: Supercritical Tradeoffs for Monotone Circuits},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/N545RHQV}},
  note         = {Machine review of arXiv:2411.14268}
}
read the original abstract

We exhibit a monotone function computable by a monotone circuit of quasipolynomial size such that any monotone circuit of polynomial depth requires exponential size. This is the first size-depth tradeoff result for monotone circuits in the so-called supercritical regime. Our proof is based on an analogous result in proof complexity: We introduce a new family of unsatisfiable 3-CNF formulas (called bracket formulas) that admit resolution refutations of quasipolynomial size while any refutation of polynomial depth requires exponential size.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

44 extracted references · 26 canonical work pages

  1. [1]

    A combinatorial characterization of resolution width

    Albert Atserias and V \' ctor Dalmau. A combinatorial characterization of resolution width. Journal of Computer and System Sciences , 74(3):323--334, 2008. https://doi.org/10.1016/j.jcss.2007.06.025 doi:10.1016/j.jcss.2007.06.025

  2. [2]

    The complexity of hex and the J ordan curve theorem

    Aviv Adler, Constantinos Daskalakis, and Erik Demaine. The complexity of hex and the J ordan curve theorem. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP) , volume 55 of LIPIcs , pages 24:1--24:14. Schloss Dagstuhl, 2016. https://doi.org/10.4230/LIPIcs.ICALP.2016.24 doi:10.4230/LIPIcs.ICALP.2016.24

  3. [3]

    Time-space trade-offs in resolution: Superpolynomial lower bounds for superlinear space

    Paul Beame, Christopher Beck, and Russell Impagliazzo. Time-space trade-offs in resolution: Superpolynomial lower bounds for superlinear space. SIAM Journal on Computing , 45(4):1612--1645, 2016. https://doi.org/10.1137/130914085 doi:10.1137/130914085

  4. [4]

    On the complexity of finding narrow proofs

    Christoph Berkholz. On the complexity of finding narrow proofs. In Proceedings of the 53rd Symposium on Foundations of Computer Science (FOCS) , volume 40, pages 351--360. IEEE, 2012. https://doi.org/10.1109/FOCS.2012.48 doi:10.1109/FOCS.2012.48

  5. [5]

    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. Technical report, arXiv, 2024. https://doi.org/10.48550/ARXIV.2407.17947 doi:10.48550/ARXIV.2407.17947

  6. [6]

    Supercritical space-width trade-offs for resolution

    Christoph Berkholz and Jakob Nordstr \" o m. Supercritical space-width trade-offs for resolution. SIAM Journal on Computing , 49(1):98--118, 2020. https://doi.org/10.1137/16M1109072 doi:10.1137/16M1109072

  7. [7]

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

    Christoph Berkholz and Jakob Nordstr \" o 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, 2023. https://doi.org/10.1145/3195257 doi:10.1145/3195257

  8. [8]

    Some trade-off results for polynomial calculus: extended abstract

    Chris Beck, Jakob Nordstr \" o m, and Bangsheng Tang. Some trade-off results for polynomial calculus: extended abstract. In Proceedings of the 45th Symposium on Theory of Computing (STOC) , pages 813--822. ACM, 2013. https://doi.org/10.1145/2488608.2488711 doi:10.1145/2488608.2488711

Show all 44 references
  1. [9]

    Making hard problems harder

    Joshua Buresh - Oppenheim and Rahul Santhanam. Making hard problems harder. In Proceedings of the 21st Conference on Computational Complexity (CCC) , pages 73--87. IEEE, 2006. https://doi.org/10.1109/ccc.2006.26 doi:10.1109/ccc.2006.26

  2. [10]

    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), 2024. URL: https://eccc.weizmann.ac.il/report/2024/001

  3. [11]

    Short proofs are narrow---resolution made simple

    Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow---resolution made simple. Journal of the ACM , 48(2):149--169, 2001. https://doi.org/10.1145/375827.375835 doi:10.1145/375827.375835

  4. [12]

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

    Arkadev Chattopadhyay and Pavel Dvo r \'ak. Super-critical trade-offs in resolution over parities via lifting. Technical Report TR24-132, Electronic Colloquium on Computational Complexity (ECCC), 2024. URL: https://eccc.weizmann.ac.il/report/2024/132/

  5. [13]

    Truly supercritical trade-offs for resolution, cutting planes, monotone circuits, and W eisfeiler-- L eman

    Susanna de Rezende, Noah Fleming, Duri Janett, Jakob Nordstr \"o m, and Shuo Pang. Truly supercritical trade-offs for resolution, cutting planes, monotone circuits, and W eisfeiler-- L eman. Technical report, 2024

  6. [14]

    Lifting with simple gadgets and applications to circuit and proof complexity

    Susanna de Rezende, Or Meir, Jakob Nordstr \"o m, Toniann Pitassi, Robert Robere, and Marc Vinyals. Lifting with simple gadgets and applications to circuit and proof complexity. In Proceedings of the 61st Symposium on Foundations of Computer Science (FOCS) , volume 169, pages ...

  7. [15]

    How limited interaction hinders real communication (and what it means for proof and circuit complexity)

    Susanna de Rezende, Jakob Nordstr \"o m, and Marc Vinyals. How limited interaction hinders real communication (and what it means for proof and circuit complexity). In Proceedings of the 57th Symposium on Foundations of Computer Science (FOCS) , pages 295--304, 2016. https://do...

  8. [16]

    On the power and limitations of branch and cut

    Noah Fleming, Mika G\" o \" o 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 Conference on Computational Complexity (CCC) . Schloss Dagstuhl, 2021. https://doi.o...

  9. [17]

    Unique end of potential line

    John Fearnley, Spencer Gordon, Ruta Mehta, and Rahul Savani. Unique end of potential line. Journal of Computer and System Sciences , 114:1--35, 2020. https://doi.org/10.1016/j.jcss.2020.05.007 doi:10.1016/j.jcss.2020.05.007

  10. [18]

    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) , volume 215 of LIPIcs , pages 70:1--70:23. Schloss Dagstuhl, 2022. https://doi.org/10.4230/LIPICS.ITCS.2022.70 doi...

  11. [19]

    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. In Proceedings of the 30th Symposium on Theory of Computing (STOC) , pages 429--437. ACM, 1998. https://doi.org/10.1145/276698.276855 doi:10.1145/276698.276855

  12. [20]

    Monotone circuit lower bounds from resolution

    Ankit Garg, Mika G \"o \"o s, Pritish Kamath, and Dmitry Sokolov. Monotone circuit lower bounds from resolution. Theory of Computing , 16(1):1--30, 2020. https://doi.org/10.4086/toc.2020.v016a013 doi:10.4086/toc.2020.v016a013

  13. [21]

    Further collapses in TFNP

    Mika G \"o \"o s, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Further collapses in TFNP . SIAM Journal on Computing , 53(3):573--587, 2024. https://doi.org/10.1137/22M1498346 doi:10.1137/22M1498346

  14. [22]

    Separations in proof complexity and TFNP

    Mika G\" o \" o s, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Separations in proof complexity and TFNP . Journal of the ACM , 71(4), 2024. https://doi.org/10.1145/3663758 doi:10.1145/3663758

  15. [23]

    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 Symposium on Logic in Computer Science (LICS) , pages 1--13, 2023. https://doi.org/10.1109/LICS56636.2023.10175741 doi:10.1109/LICS56636.2023.10175741

  16. [24]

    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 Symposium on Foundations of Computer Science (FOCS) , pages 798--809. IEEE, 2023. https://doi.org/10....

  17. [25]

    Hardness condensation by restriction

    Mika G\" o \" o s, Ilan Newman, Artur Riazanov, and Dmitry Sokolov. Hardness condensation by restriction. In Proceedings of the 56th Symposium on Theory of Computing (STOC) , pages 2016--2027. ACM, 2024. https://doi.org/10.1145/3618260.3649711 doi:10.1145/3618260.3649711

  18. [26]

    Communication lower bounds via critical block sensitivity

    Mika G \"o \"o s and Toniann Pitassi. Communication lower bounds via critical block sensitivity. SIAM Journal on Computing , 47(5):1778--1806, 2018. https://doi.org/10.1137/16M1082007 doi:10.1137/16M1082007

  19. [27]

    Unpublished manuscript, 2024

    Alexandros Hollender, Gilbert Maystre, and Kilian Risse. Unpublished manuscript, 2024

  20. [28]

    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 Symposium on Foundations of Computer Science (FOCS) , pages 121--131. IEEE, 2017. https://doi.org/10.1109/FOCS.2017.20 doi:10.1109/FOCS.2017.20

  21. [29]

    Hard submatrices for non-negative rank and communication complexity

    Pavel Hrube s . Hard submatrices for non-negative rank and communication complexity. In Proceedings of the 39th Conference on Computational Complexity (CCC) , volume 300 of LIPIcs , pages 13:1--13:12. Schloss Dagstuhl, 2024. https://doi.org/10.4230/LIPIcs.CCC.2024.13 doi:10.42...

  22. [30]

    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. https://doi.org/10.1007/978-3-642-24508-4 doi:10.1007/978-3-642-24508-4

  23. [31]

    On monotone formulae with restricted depth

    Maria Klawe, Wolfgang Paul, Nicholas Pippenger, and Mihalis Yannakakis. On monotone formulae with restricted depth. In Proceedings of the 16th Symposium on Theory of Computing (STOC) , pages 480--487. ACM, 1984. https://doi.org/10.1145/800057.808717 doi:10.1145/800057.808717

  24. [32]

    Monotone circuits for connectivity require super-logarithmic depth

    Mauricio Karchmer and Avi Wigderson. Monotone circuits for connectivity require super-logarithmic depth. In Proceedings of the 20th Symposium on Theory of Computing (STOC) , pages 539--550. ACM, 1988. https://doi.org/10.1145/62212.62265 doi:10.1145/62212.62265

  25. [33]

    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) , volume 215 of LIPIcs , pages 104:1--104:24. Schloss Dagstuhl, 2022. https://doi.org/10...

  26. [34]

    Space characterizations of complexity measures and size-space trade-offs in propositional proof systems

    Theodoros Papamakarios and Alexander Razborov. Space characterizations of complexity measures and size-space trade-offs in propositional proof systems. Journal of Computer and System Sciences , 137:20--36, 2023. https://doi.org/10.1016/j.jcss.2023.04.006 doi:10.1016/j.jcss.2023.04.006

  27. [35]

    Proofs as games

    Pavel Pudl\' a k. Proofs as games. American Mathematical Monthly , pages 541--550, 2000. https://doi.org/10.2307/2589349 doi:10.2307/2589349

  28. [36]

    Applications of matrix methods to the theory of lower bounds in computational complexity

    Alexander Razborov. Applications of matrix methods to the theory of lower bounds in computational complexity. Combinatorica , 10(1):81--93, 1990. https://doi.org/10.1007/BF02122698 doi:10.1007/BF02122698

  29. [37]

    A new kind of tradeoffs in propositional proof complexity

    Alexander Razborov. A new kind of tradeoffs in propositional proof complexity. Journal of the ACM , 63(2):16:1--16:14, 2016. https://doi.org/10.1145/2858790 doi:10.1145/2858790

  30. [38]

    On space and depth in resolution

    Alexander Razborov. On space and depth in resolution. Computational Complexity , 27(3):511--559, 2017. https://doi.org/10.1007/s00037-017-0163-1 doi:10.1007/s00037-017-0163-1

  31. [39]

    On the width of semialgebraic proofs and algorithms

    Alexander Razborov. On the width of semialgebraic proofs and algorithms. Mathematics of Operations Research , 42(4):1106--1134, 2017. https://doi.org/10.1287/moor.2016.0840 doi:10.1287/moor.2016.0840

  32. [40]

    Separation of the monotone NC hierarchy

    Ran Raz and Pierre McKenzie. Separation of the monotone NC hierarchy. Combinatorica , 19(3):403--435, 1999. https://doi.org/10.1007/s004930050062 doi:10.1007/s004930050062

  33. [41]

    Unified Lower Bounds for Monotone Computation

    Robert Robere. Unified Lower Bounds for Monotone Computation . PhD thesis, University of Toronto, Canada, 2018. URL: http://hdl.handle.net/1807/92007

  34. [42]

    Correlation bounds against monotone NC ^1

    Benjamin Rossman. Correlation bounds against monotone NC ^1 . In Proceedings of the 30th Conference on Computational Complexity (CCC) , volume 33 of LIPIcs , pages 392--411. Schloss Dagstuhl, 2015. https://doi.org/10.4230/LIPIcs.CCC.2015.392 doi:10.4230/LIPIcs.CCC.2015.392

  35. [43]

    Formula size-depth tradeoffs for iterated sub-permutation matrix multiplication

    Benjamin Rossman. Formula size-depth tradeoffs for iterated sub-permutation matrix multiplication. In Proceedings of the 56th Symposium on Theory of Computing (STOC) , pages 1386--1395. ACM, 2024. https://doi.org/10.1145/3618260.3649628 doi:10.1145/3618260.3649628

  36. [44]

    A switching lemma for small restrictions and lower bounds for k - DNF resolution

    Nathan Segerlind, Sam Buss, and Russell Impagliazzo. A switching lemma for small restrictions and lower bounds for k - DNF resolution. SIAM Journal on Computing , 33(5):1171--1200, 2004. https://doi.org/10.1137/S0097539703428555 doi:10.1137/S0097539703428555

Pith tools

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