{"id":"735dd5bf-683e-4657-b675-9dab270ce8b2","arxiv_id":"2411.14267","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"First truly supercritical size-depth trade-offs for resolution and cutting planes, supercritical monotone circuit depth, and Weisfeiler-Leman dimension-iteration trade-offs.","lead":"Small circuits and short proofs can secretly require enormous depth, beyond the worst-case bound: this paper proves the first truly supercritical trade-offs for monotone circuits, resolution, and cutting planes, and transfers them to Weisfeiler-Leman. The results come from a refined Cop-Robber game analysis and new lifting theorems.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The central reduction has an off-by-one: Theorem 4.1's survival against k+c Cops only rules out refutations of width at most k+c-1, not the stated k+c, so Theorem 2.3 is not derived as written.","rationale":"The reader identified Proposition 4.10 and the concentration of minimal virtual cordons as the weakest point. That is indeed a subtle geometric lemma, and I found no clear error in its proof: the singleton-class argument for excluding the shift by L works because two vertices in the middle part cannot differ by exactly L, and Property (P3) correctly forces the common offset to be 0 or L. The lifting theorems also appear internally consistent; in particular the treelike lifting proof and the triangle-DAG lifting argument check out structurally, and the probabilistic Lemma 6.3 is valid once the base (1-1/m)/2 is parsed correctly. The most load-bearing defect I found is instead in the parameter counting of the central reduction: Lemma 3.14 attaches one extra Cop to the width, while Theorem 4.1's survival bound is stated for k+c Cops. Thus the proof as written establishes a width lower bound of k+c-1, not k+c. This is a small but real gap in the exact statement of the central theorem; it does not appear to destroy the qualitative results, since a parameter shift by one repairs all non-endpoint cases, but the c=k-1 range and the quoted width thresholds need explicit correction. For that reason I recommend a conditional acceptance rather than a rejection or an unchanged acceptance.","tokens_in":1115,"tokens_out":3929,"duration_ms":314310,"concrete_test":"Formally run the contrapositive of Lemma 3.14 with w=k+c. Verify that the resulting winning strategy uses k+c+1 Cops, and then check whether Theorem 4.1 provides Robber survival for that many Cops; if not, Theorem 2.3 must either lower its width threshold to k+c-1 or prove survival against k+c+1 Cops. Then re-check that all applications in Theorems 2.5, 2.8, 2.12, and 1.4 remain valid after replacing c by c+1, especially at the c=k-1 endpoint.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"Lemma 3.14 is the bridge from resolution to Cops: a width-w, depth-d refutation of the compressed Tseitin formula yields a winning strategy for w+1 Cops in d+1 rounds. Theorem 4.1 proves Robber survival only against at most k+c Cops. Contraposing gives: no refutation of width at most k+c-1 can have depth below the survival time, because such a refutation would give a strategy for (k+c-1)+1 = k+c Cops. It does not rule out width k+c: that would require survival against k+c+1 Cops. Therefore Theorem 2.3, which promises a lower bound for every refutation of width at most k+c, is not a consequence of the stated Cop-Robber bound. The same one-off is visible in Theorem 2.1: for c=1 it claims Robber survival against k+1 Cops even though the same theorem says k+1 Cops can win. The likely fix is to shift the parameter: applying the game theorem with c+1 Cops gives the desired width bound for c <= k-2, and the main applications in Theorems 2.5 and 2.8 are probably robust to this shift. But as written, the endpoint c=k-1 in Theorem 2.3, and the exact threshold 'width at most k+c', are not supported by the proof.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":54675,"tokens_out":21480,"duration_ms":176778,"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":[{"comment":"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.","section":"§2.4 (Theorem 2.3), §3.3 (Lemma 3.14), §4 (Theorem 4.1)"},{"comment":"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.","section":"§2.5 (Theorem 2.5), §2.6 (Theorems 2.8, 2.12, 2.13)"}],"minor_comments":[{"comment":"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.","section":"§4.1, Proposition 4.10"},{"comment":"In the restatement of the lemma, the domain is written as {m}^n, which should be [m]^n.","section":"Appendix B, Full Image Lemma"},{"comment":"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.","section":"§7.2, equation (7.13)"}],"recommendation":"major_revision","confidential_remarks":"The paper is technically ambitious and the core results are likely correct after fixing the systematic off-by-one in the width-to-Cops reduction. The error is load-bearing because it affects the central theorem and all derived trade-offs, but it appears repairable by shifting parameters and restating thresholds. The authors should also fix the c=1 contradiction in the Cop-Robber theorem and re-verify the parameter choices in Sections 2.5 and 2.6. The lifting theorems and the CFI translation appear sound at the level of detail provided. Given the significance of the results, I recommend major revision rather than reject."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know: this is a substantial paper with real new results — first truly supercritical size-depth trade-offs for resolution and cutting planes, a supercritical monotone circuit depth trade-off, and a robust Weisfeiler-Leman dimension-iteration trade-off. The lifting theorems (treelike, resolution, triangle-DAG) look like reusable tools, and the paper is honest about the concurrent work by Göös et al. The compressed Cop-Robber game with virtual cordons is a genuine technical advance. No circularity: the target results are derived from first principles.\n\nThat said, the stress-test note is correct, and I checked it against the text. Lemma 3.14 maps a width-w refutation to a winning strategy for w+1 Cops. Theorem 4.1 proves Robber survival against k+c Cops. Contraposing gives a depth lower bound only for refutations of width at most k+c-1, not k+c as Theorem 2.3 states. Worse, Theorem 2.1 for c=1 says both that k+1 Cops can win (in k rounds, by the proof of Theorem 4.1) and that the Robber survives Ω(n^k) rounds against k+1 Cops. That can't hold. The likely fix is a parameter shift — invoke the Cop-Robber theorem with c+1 Cops — which covers c ≤ k-2 and probably all the applications that appear later (Theorems 2.5, 2.8, 2.12, 2.13, and the concrete results in Section 1). The endpoint c=k-1 and the exact threshold 'width at most k+c' are not supported as written.\n\nBeyond that, the Cop-Robber lower bound itself is intricate and not machine-checked; the geometric-concentration step around Proposition 4.10 and equation (4.8) is subtle. I did not find a gap there, but it's the kind of place a small error could hide. The lifting proofs are detailed and plausible.\n\nBottom line: this deserves a serious referee, and my own verdict would be accept after major revision. The off-by-one is real but looks fixable, and the main results probably go through with modest changes. I'd bring it to the reading group and would cite it once the parameter issue is cleaned up.","headline":"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.","tokens_in":669,"tokens_out":879,"would_cite":true,"duration_ms":71129,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03F20","68Q17"],"pacs":[],"model":"deepseek-v4-flash","headline":"Small formulas force proof depth beyond worst case, and the same trade-off hits circuits and graph algorithms.","keywords":["resolution proof complexity","supercritical trade-offs","cutting planes","monotone circuits","Weisfeiler-Leman","Cop-Robber game","Tseitin formulas","lifting theorems"],"falsifier":"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.","tokens_in":54211,"feed_emoji":"⚖️","tokens_out":12360,"duration_ms":103721,"temperature":0.7,"pith_summary":"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.","feed_headline":"Small formulas force proof depth beyond worst case","feed_subtitle":"It is the first truly supercritical resolution trade-off, extending to circuits, cutting planes, and Weisfeiler–Leman.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the graph-compression and Cop-Robber framework that the proof refines and strengthens.","marker":"[GLNS23]"},{"why":"Introduces the notion of supercritical trade-offs via hardness condensation, the benchmark this paper surpasses with variable compression.","marker":"[Raz16]"},{"why":"Previous truly supercritical resolution width-depth trade-off, but with no robustness; Theorem 2.3 is the strengthening that holds across an interval of widths.","marker":"[Ber12]"},{"why":"Gives quasi-polynomial cutting planes proofs of Tseitin formulas with quasi-polynomial depth, the phenomenon that motivates truly supercritical size-depth lower bounds.","marker":"[DT20]"},{"why":"Supplies the rectangle-DAG lifting framework and search-problem reductions reused for monotone circuits and cutting planes.","marker":"[GGKS20]"},{"why":"Provides the Full Image Lemma and sunflower-based lifting ingredients adapted in the triangle-DAG proof.","marker":"[LMM+22]"},{"why":"Proves the spread-set Janson bound used inside the self-contained Full Image Lemma.","marker":"[FKNP21]"},{"why":"Establishes the equivalence between Weisfeiler-Leman dimensions and counting-logic variables used to translate the Weisfeiler-Leman trade-off to first-order logic.","marker":"[CFI92]"}],"fun_headline_variants":["Supercritical trade-offs: tiny formulas force massive proof depth","Resolution depth exceeds worst case in new supercritical trade-off","First truly supercritical resolution trade-off for width-depth","Small CNF refutations need super-linear depth in resolution","Supercritical proof depth: circuits, cutting planes, Weisfeiler-Leman"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Supercritical trade-offs: tiny formulas force massive proof depth","Resolution depth exceeds worst case in new supercritical trade-off","First truly supercritical resolution trade-off for width-depth","Small CNF refutations need super-linear depth in resolution","Supercritical proof depth: circuits, cutting planes, Weisfeiler-Leman"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000493,"raw_usage":{"total_tokens":2478,"prompt_tokens":1055,"completion_tokens":1423,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":671,"completion_tokens_details":{"reasoning_tokens":1338}},"tokens_in":671,"tokens_out":1423,"duration_ms":13874,"temperature":1.0,"reasoning_tokens":1338,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T15:21:09.648113+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}