{"id":"9acf057e-cec9-4972-a51d-8a95e2a64afc","arxiv_id":"2505.16012","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"For CNFs that encode a ternary tree crossed with a path, Decision DNNFs whose conjunction gates split variables imbalancedly require size at least n^{Ω((1−α)√k)}, ruling out FPT-sized representations.","lead":"This paper proves a lower bound on the size of Decision DNNFs, a type of decision diagram, when their conjunction gates are forced to be imbalanced. It shows that for certain CNF formulas of bounded treewidth, such restricted diagrams must be large, so this middle-ground model cannot match the efficiency of unrestricted Decision DNNFs.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 19's induction uses an unstated strengthening in Claim 3; as written, the top-down case of Lemma 8 is not fully justified, though the gap appears repairable.","rationale":"The paper's central contribution is a genuine lower-bound argument: an XP-style size lower bound for Decision DNNFs with α-imbalanced conjunction gates representing CNFs of bounded primal treewidth, via the combinatorial engine Lemma 8. The overall architecture — probability space over satisfying assignments, target triples, mainstream paths, and a union bound — is coherent and the surrounding lemmas are mostly detailed and checkable. The reader's verdict of CONDITIONAL is appropriate. My stress-test identifies the same weakest assumption: the induction in Theorem 19 uses an invariant that is not stated in the theorem. Claim 3 depends on the intersection size |π1 ∩ V_{>h0}(h,k,t1)| ≥ k, which is not part of the stated induction hypothesis. This is not a mere cosmetic omission; without it, the application of Lemma 18 and hence the lower bound in the top-down case of Lemma 8 does not follow. The gap appears repairable, because the base case supplies the intersection property via the definition of (h0,h1)-td permutations and the main case can plausibly preserve it by taking the prefix from the middle child. I also note the abstract/theorem exponent mismatch, but that is a statement-strength issue, not a correctness issue for the √k lower bound. No ad hominem or theatrical language is warranted: the paper is a serious theoretical effort with a repairable proof gap and an overstated abstract. Therefore the reader's CONDITIONAL verdict should stand unchanged.","tokens_in":25138,"tokens_out":9324,"duration_ms":79323,"concrete_test":"Restate Theorem 19 with the strengthened induction hypothesis: for every t ∈ V_{≥h1}(h), the produced prefix π_t satisfies |π_t ∩ V_{>h0}(h,k,t)| ≥ k, in addition to the independent path set and the disjoint S. Then re-run the main-case proof and verify that Claim 3 follows from the strengthened IH applied to t1, and that the returned prefix π2 inherits the new intersection property from t2. If the strengthened IH cannot be proved for the output prefix, Lemma 8's top-down case fails; if it can, amend the theorem statement accordingly. This is a pure proof-reconstruction check and needs no numerical experiment.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing weakness is in the proof of Lemma 8's top-down case, specifically Theorem 19 (Section 4). In the main induction step, the proof applies the induction hypothesis to three children t1, t2, t3 of t and obtains prefixes π1, π2, π3 with independent path sets P1, P2, P3 and disjoint sets S1, S2, S3. Claim 3 then asserts that |W0 ∩ π2 ∩ V_{>h0}(h,k,t)| ≥ k, justifying this by saying that W0 ∩ π1 ∩ V_{>h0}(h,k,t1) has size at least k 'by assumption'. But the stated induction hypothesis guarantees only the existence of a prefix, an independent path set of size at least c(h1,height(ti))·√k, and an S ∈ S_{h0}(h,k,ti) disjoint from πi; it does not state that |πi ∩ V_{>h0}(h,k,ti)| ≥ k. Without this intersection bound, Claim 3 does not follow, Lemma 18 cannot be applied with U = π2, and the rank lower bound for the top-down case is unsupported. The property does hold in the base case, since it comes directly from the definition of (h0,h1)-td permutations, and it is plausibly preserved by the main construction because V_{>h0}(h,k,t2) ⊆ V_{>h0}(h,k,t); however, the inductive invariant must be stated explicitly. A secondary issue is that the abstract claims n^{Ω((1−α)k)} while Theorem 7 and the proof establish only n^{Ω((1−α)√k)}; this affects the advertised strength, not the validity of the corrected theorem.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies Decision DNNFs (modeled as ∧d-FBDDs) in which every conjunction gate is α-imbalanced, meaning at most one input of each gate depends on more than n^α variables. It asks whether CNFs of bounded primal treewidth admit FPT-size representations in this model, and answers this negatively in the deterministic setting: for each sufficiently large k it constructs an infinite class of CNFs of primal treewidth at most k whose ∧d,α-FBDD representations have size n^{Ω((1−α)√k)}. The hard instances are graph CNFs φ(T[h,k]) where T[h,k] is the Cartesian product of a complete ternary tree of height h with a path of length k. The proof combines a probabilistic union-bound argument over satisfying assignments with a new combinatorial statement, Lemma 8, which asserts that every permutation of V(T[h,k]) contains a prefix and two disjoint sets forming a 'target triple' of large rank. Lemma 8 is proved by a case analysis depending on whether the permutation is 'top-down' or 'bottom-up' with respect to two height parameters; the top-down case relies on an inductive statement (Theorem 19) about independent path sets, and the bottom-up case on a direct construction (Lemma 21). The paper also introduces a notion of non-local width and discusses potential connections to bidimensionality and to the non-deterministic DNNF case, which remains open.","tokens_in":25363,"tokens_out":22454,"duration_ms":170712,"significance":"If the proof gaps identified below are repaired, the result is a solid and interesting lower bound: it is, to my knowledge, the first separation showing that imbalanced decomposable conjunction gates do not retain the FPT representability of bounded-treewidth CNFs in the deterministic setting. The paper is largely self-contained, builds transparently on the prior FBDD lower-bound approach of [13], and introduces a genuinely new combinatorial notion (target triples and the associated non-local width) that may have independent use. The main technical work is original and does not fit parameters to the conclusion; the probabilistic argument and the graph-family construction are explicit and falsifiable. The open question for general (non-deterministic) DNNFs is honestly stated and the limitations of the current approach are discussed in the conclusion.","major_comments":[{"comment":"The abstract states a lower bound of n^{Ω((1−α)·k)} for the representation size, but Theorem 1 and Theorem 7 state and prove only n^{Ω((1−α)√k)}. In the proof of Theorem 7 (Section 3), the probability bound uses |U0| ≥ Ω((1−α)·h√k) with h = Θ(log n), which yields n^{−Ω((1−α)√k)}, not n^{−Ω((1−α)k)}. The abstract and any summary statements must be corrected to the √k exponent unless the stronger bound is proved.","section":"Abstract; Theorems 1 and 7; Section 3"},{"comment":"The induction step of Theorem 19 applies the induction hypothesis to t1,t2,t3 and then asserts in Claim 3 that |W0 ∩ π2 ∩ V_{>h0}(h,k,t)| ≥ k 'by assumption', because |W0 ∩ π1 ∩ V_{>h0}(h,k,t1)| ≥ k. However, the stated induction hypothesis guarantees only the existence of an independent path set and a disjoint S ∈ S_{h0}(h,k,ti); it does not guarantee |πi ∩ V_{>h0}(h,k,ti)| ≥ k. Without this lower bound, Lemma 18 cannot be applied to U = π2, and the size lower bound in the top-down case of Lemma 8 does not follow. The fix is to add the condition |πi ∩ V_{>h0}(h,k,ti)| ≥ k to the inductive invariant; it is true in the base case by the definition of an (h0,h1)-td permutation and is preserved in the construction because V_{>h0}(h,k,t2) ⊆ V_{>h0}(h,k,t).","section":"Section 4, Theorem 19, Claim 3"},{"comment":"The proof of the induction step contains inconsistent notation that makes the argument unverifiable as written. The theorem statement requires an independent path set of size at least c(h1,height(t))√k, but the proof invokes the induction hypothesis with c(h0,height(ti)) and later states 'height(t2) = 4a' and '4(a+1) is exactly height(t)'. These assertions are false for the actual parameters h0,h1 (they ignore the contributions of h0 and h1). The intended calculation works if c is evaluated as c(h1,height(ti)) and the congruence condition is height(ti)−h1 ≡ 0 mod 4; with that reading, c(h1,height(t2)) + 1/65 = c(h1,height(t)). The same notational shift fixes the final reduction to a descendant t0, for which the equality c(h1,height(t0)) = c(h1,height(t)) is valid when height(t0) is the largest descendant height with height(t0)−h1 a multiple of 4 not exceeding height(t). This paragraph must be rewritten so that the parameter h1 is used consistently in the function c.","section":"Section 4, Theorem 19 proof (parameter handling)"}],"minor_comments":[{"comment":"The references to 'Lemma 12' when applying the statement that S(φ)|g does not break a connected unfixed set should refer to Lemma 3 in Section 2; Lemma 12 as numbered states a different property.","section":"Sections 3.1 and 3.2"},{"comment":"The definition of Iu(P,U0,U1) in the second case reads 'Iu(P,U0,U1) = N(u) ∩ W = {u}'; this should be 'Iu(P,U0,U1) = {u}', since N(u) ∩ W is not generally equal to {u}.","section":"Definition 14, item 2"},{"comment":"The line 'P r(Set(I(...))) ≤ 2^{|I|}' should involve the constant β from Claim 2 (or an equivalent constant absorbed into the exponent), and the subsequent bound 'n^{−Ω((1−α)·k)}' should read 'n^{−Ω((1−α)√k)}' to be consistent with the preceding h√k bound and with the theorem statement.","section":"Section 3, proof of Theorem 7"},{"comment":"There are several typos that should be corrected: 'number if variables' (Abstract), 'treewidht' (Introduction), 'collary' (Section 3), 'negaitvely' (Section 3.2), and 'hods' (Appendix).","section":"Throughout"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is close to correct: the main gap is a missing inductive invariant in Theorem 19, together with parameter-handling typos in the same theorem, and the abstract overstates the proved exponent. All of these appear locally repairable within the scope of a revision. I recommend major revision rather than rejection. Please ensure the abstract is aligned with the proved √k exponent; if the author can prove the k exponent, the advertised strength would be justified. The referee report is based on v2 of the manuscript."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper proves something real: Decision DNNFs with α-imbalanced conjunction gates need n^{Ω((1−α)√k)} size to represent the bounded-treewidth CNFs φ(T[h,k]), giving the first negative answer to a restricted version of the open question. The target-triple framework and the top-down/bottom-up permutation dichotomy are the genuinely new proof devices, and they look like they should outlive this specific application.\n\nWhat the paper does well: the proof is essentially self-contained, the probability space over satisfying assignments plus the union bound is clean, and the combinatorial engine (Lemma 8) is spelled out in serious detail. The prior FBDD work is cited for a standard probabilistic fact, not leaned on for the main claim. The discussion of why the argument does not extend to nondeterministic DNNFs is honest and points at a plausible path forward.\n\nNow the soft spots, in proportion. First, the abstract advertises n^{Ω((1−α)k)}, but Theorem 1 and Theorem 7 only establish n^{Ω((1−α)√k)}. That is a real overstatement of the strength, even though the corrected statement is still interesting. Second, and more load-bearing, the proof of Lemma 8 in the top-down case goes through Theorem 19, and the induction step has a genuine gap. Claim 3 asserts |W0 ∩ π2 ∩ V_{>h0}(h,k,t)| ≥ k by saying it holds \"by assumption,\" but the stated induction hypothesis only guarantees the existence of an independent set of paths and a disjoint anchor set—it does not state the ≥k intersection condition. Without that condition, Lemma 18 cannot be applied at that point, and the rank bound for the top-down case is unsupported as written. The gap looks repairable: the bound holds in the base case, and the construction plausibly preserves it because V_{>h0}(h,k,t2) ⊆ V_{>h0}(h,k,t). But it has to be stated as an explicit inductive invariant. There are also a few garbled passages in definitions and lemma statements that a careful revision should clean up.\n\nWho is this for? Knowledge compilation, branching program lower bounds, and parameterized complexity people will all want to know this. It deserves a serious referee—the result is novel and the gap is localized, not a sign of a broken core.\n\nMy recommendation: send it to review, and ask the author to fix the abstract-to-theorem mismatch and complete the induction in Theorem 19.","headline":"A genuinely new lower bound for Decision DNNFs with imbalanced gates, with a localized but repairable gap in the top-down case of the main combinatorial lemma.","tokens_in":26002,"tokens_out":1855,"would_cite":true,"duration_ms":17277,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q27","05C85","68R10"],"pacs":[],"model":"deepseek-v4-flash","headline":"Imbalanced Decision DNNFs cannot efficiently represent all CNFs of bounded primal treewidth; the hard family requires size $n^{\\Omega((1-\\alpha)\\sqrt{k})}$.","keywords":["Decision DNNF","imbalanced conjunction gates","knowledge compilation","bounded primal treewidth","non-local width parameters","parameterized lower bounds","free binary decision diagrams","Cartesian product of trees and paths"],"falsifier":"One concrete refutation would be a permutation of $V(T[h,k])$ in which every target triple has rank $o((1-\\alpha)h\\sqrt{k})$ for $h$ large relative to $k$, since Lemma 8 is necessary for the proof of Theorem 7. Alternatively, one can test the disputed induction step in Theorem 19: build a $(h_0,h_1)$-top-down permutation and a descendant subtree for which the stated hypotheses hold but the relevant prefix of that subtree contains fewer than $k$ vertices above height $h_0$, making Claim 3 unsupported.","tokens_in":24805,"feed_emoji":"📉","tokens_out":14649,"duration_ms":123798,"temperature":0.7,"pith_summary":"This paper asks whether the standard knowledge-compilation model DNNF keeps its tractable-size guarantee for CNFs of bounded primal treewidth when every conjunction gate is restricted to be $\\alpha$-imbalanced: at most one input of each gate may depend on more than $n^\\alpha$ variables. For the deterministic version of the model, Decision DNNF (viewed as a free BDD with decomposable conjunction gates, written $\\wedge_d,\\alpha$-fbdd), the answer is negative. For every sufficiently large $k$, there is an infinite family of CNFs of primal treewidth at most $k$ whose representation as $\\wedge_d,\\alpha$-fbdds has size $n^{\\Omega((1-\\alpha)\\sqrt{k})}$. This places the deterministic imbalanced model between read-once branching programs, which are not fixed-parameter tractable on bounded-treewidth CNFs, and unrestricted DNNFs, which are. The proof's engine is a graph-combinatorial statement about the Cartesian product of a ternary tree with a path, asserted to be of independent interest for parameterized complexity.","feed_headline":"Imbalanced Decision DNNFs fail on bounded-treewidth CNFs","feed_subtitle":"For every large k, treewidth-k CNFs need $n^{\\Omega((1-\\alpha)\\sqrt{k})}$ size in this model.","key_machinery":"The central objects are $\\wedge_d,\\alpha$-fbdds: free binary decision diagrams (read-once branching programs) augmented with decomposable conjunction gates, where every conjunction gate is $\\alpha$-imbalanced, meaning that at most one of its two children is large (depends on more than $n^\\alpha$ variables). The hard formulas are $\\varphi(T[h,k])$, edge CNFs of $T[h]\\square P_k$, where $T[h]$ is a complete ternary tree of height $h$ and $P_k$ a path of $k$ vertices; these graphs have treewidth at most $2k-1$. The load-bearing combinatorial object is the target triple $(W, U_0, U_1)$: each connected component of $G[U_1]$ has size greater than $n^\\alpha$; each vertex of $U_0$ is adjacent to both $U_1$ and $W$; $U_0$ is independent; the neighbours of $U_0$ inside $W$ are independent and private to each $U_0$-vertex. Lemma 8 asserts that every permutation of $V(T[h,k])$ admits a prefix $W$ and disjoint sets $U_0,U_1$ forming a target triple of rank $\\Omega((1-\\alpha)h\\sqrt{k})$. The triple is converted into an independent set $I(P,U_0,U_1)$ of variables that every satisfying assignment carried through the designated BDD node must set to $1$, exactly the event whose probability is small enough for a union bound.","core_discovery":"The central claim is Theorem 7: if $B$ is a $\\wedge_d,\\alpha$-fbdd computing $\\varphi(T[h,k])$, then for $h$ sufficiently large compared with $k$, $|B| \\ge n^{\\Omega((1-\\alpha)\\sqrt{k})}$. Since the primal treewidth of $T[h,k]$ is at most $2k-1$ (Proposition 2), Theorem 1 follows as a corollary: an infinite class of CNFs of primal treewidth at most $k$ requires size $n^{\\Omega((1-\\alpha)\\sqrt{k})}$ in this model. The hard instances are the edge formulas $\\varphi(T[h,k])$, whose clauses are $(u\\vee v)$ for the edges of the Cartesian product $T[h]\\square P_k$ of a complete ternary tree of height $h$ with a path on $k$ vertices. The argument follows a 'mainstream path' in the BDD, a target path all of whose skipped alternatives are small; imbalance of the gates guarantees that such a path exists. Along that path, the combinatorial Lemma 8 produces a target triple whose large connected components are unfixed, so Lemma 5 forces them into the variable set of the final node, and Lemma 11 shows every satisfying assignment carried through that node assigns $1$ to an independent set of size $\\Omega((1-\\alpha)h\\sqrt{k})$. A probability estimate and a union bound then force $n^{\\Omega((1-\\alpha)\\sqrt{k})}$ distinct nodes. The abstract announces the stronger exponent $(1-\\alpha)\\cdot k$; the theorem statements and proof in the body establish the square-root form.","pith_inferences":["Editorial inference: the abstract promises exponent $(1-\\alpha)k$, but the body proves only $(1-\\alpha)\\sqrt{k}$; closing that gap would require a stronger version of Lemma 8, with rank $\\Omega((1-\\alpha)hk)$ rather than $h\\sqrt{k}$.","Editorial inference: because the proof's cornerstone, that unfixed connected sets cannot be split by decomposable gates, fails for non-deterministic DNNFs, the same target-triple machinery will need a genuinely different probabilistic argument if the conjectured lower bound for general imbalanced DNNFs is to go through.","Editorial inference: the target-triple construction transfers naturally to other graph products; testing it on grids or on $H$-minor-free families would show whether the $\\sqrt{k}$ factor is an artifact of the tree-rooted structure or a general feature of the non-local width parameter."],"forward_implications":["For each large $k$, the constructed family $\\Phi_k$ rules out fixed-parameter tractable representations: the required size grows as $n^{\\Omega((1-\\alpha)\\sqrt{k})}$, so no $f(k)\\cdot n^{O(1)}$ bound can hold uniformly for this model on these instances.","The deterministic version of the open question is settled negatively, while general (non-deterministic) DNNF remains open; thus the boundary of FPT behaviour for bounded-treewidth CNFs lies inside the conjunction-splitting power of DNNFs.","As a combinatorial corollary, every path decomposition of $T[h,k]$ has a bag of size $\\Omega(\\log n \\cdot \\sqrt{k})$ positioned so that all components of the corresponding suffix are larger than $n^\\alpha$; this is the non-local width lower bound the paper proposes as a new form of bidimensionality.","Because $|V(T[h,k])| = \\Theta(3^h k)$ and the rank bound reads $h\\sqrt{k}$, the construction is an XP, not ETH-style, lower bound: for each fixed $k$ the required size is polynomial with degree growing like $\\sqrt{k}$."],"supporting_citations":[{"why":"Defines DNNF and establishes the FPT-sized representation of bounded-treewidth CNFs that the imbalanced restriction is measured against.","marker":"[4]"},{"why":"Introduces the notion of imbalanced conjunction gates in an OBDD setting, which the paper adapts to Decision DNNFs.","marker":"[11]"},{"why":"Defines Decision DNNF and the compilation task that Theorem 1 addresses.","marker":"[12]"},{"why":"Gives the equivalent view of Decision DNNF as a free BDD with decomposable conjunction gates, used as the paper's working model.","marker":"[2]"},{"why":"Supplies the read-once branching program lower-bound method, including the permutation-based linear mim-width argument and the probability estimate used in the union bound.","marker":"[13]"}],"fun_headline_variants":["Imbalanced decision DNNFs fail hard on treewidth-k CNFs","Imbalanced gates limit decision DNNFs on bounded-treewidth CNFs","Bounded-width CNFs resist imbalanced DNNFs","Imbalanced decision DNNFs can't handle treewidth-bounded CNFs","Treewidth-bounded CNFs stump imbalanced decision DNNFs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole lower bound rests on the combinatorial engine Lemma 8, which says that every ordering of the vertices of $T[h,k]$ contains a prefix and two disjoint sets forming a target triple of rank $\\Omega((1-\\alpha)h\\sqrt{k})$; as written, the proof of that lemma uses an induction hypothesis stronger than the one it states, so the engine is not fully verified.","fun_headline_variants_meta":{"raw":{"variants":["Imbalanced decision DNNFs fail hard on treewidth-k CNFs","Imbalanced gates limit decision DNNFs on bounded-treewidth CNFs","Bounded-width CNFs resist imbalanced DNNFs","Imbalanced decision DNNFs can't handle treewidth-bounded CNFs","Treewidth-bounded CNFs stump imbalanced decision DNNFs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001564,"raw_usage":{"total_tokens":6379,"prompt_tokens":1212,"completion_tokens":5167,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":828,"completion_tokens_details":{"reasoning_tokens":5074}},"tokens_in":828,"tokens_out":5167,"duration_ms":35215,"temperature":1.0,"reasoning_tokens":5074,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T15:10:28.823015+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"One concrete refutation would be a permutation of $V(T[h,k])$ in which every target triple has rank $o((1-\\alpha)h\\sqrt{k})$ for $h$ large relative to $k$, since Lemma 8 is necessary for the proof of Theorem 7. Alternatively, one can test the disputed induction step in Theorem 19: build a $(h_0,h_1)$-top-down permutation and a descendant subtree for which the stated hypotheses hold but the relevant prefix of that subtree contains fewer than $k$ vertices above height $h_0$, making Claim 3 unsupported.","supporting_citations":[{"cited_title":"Decomposable negation normal form","cited_arxiv_id":null,"evidence_quote":"Defines DNNF and establishes the FPT-sized representation of bounded-treewidth CNFs that the imbalanced restriction is measured against."},{"cited_title":"New canonical representations by augmenting obdds with conjunctive decomposition","cited_arxiv_id":null,"evidence_quote":"Introduces the notion of imbalanced conjunction gates in an OBDD setting, which the paper adapts to Decision DNNFs."},{"cited_title":"On compiling CNF into decision-dnnf","cited_arxiv_id":null,"evidence_quote":"Defines Decision DNNF and the compilation task that Theorem 1 addresses."},{"cited_title":"Lower bounds for exact model counting and applications in probabilistic databases","cited_arxiv_id":null,"evidence_quote":"Gives the equivalent view of Decision DNNF as a free BDD with decomposable conjunction gates, used as the paper's working model."},{"cited_title":"On the read-once property of branching programs and cnfs of bounded treewidth","cited_arxiv_id":null,"evidence_quote":"Supplies the read-once branching program lower-bound method, including the permutation-based linear mim-width argument and the probability estimate used in the union bound."}],"review_version":1}