{"id":"c5f187a8-c76a-456a-9b7a-1d7d81dce9c2","arxiv_id":"2506.06716","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"Two calls to a #2DNF oracle with a single subtraction characterize gapP, strictly sandwiching #P between one and two #2DNF calls.","lead":"This paper shows that subtracting the answers of two counting calls to simple 2-DNF formulas can compute functions as hard as gapP, a class larger than #P. The result refines Toda's theorem and gives new sparsification and tight lower bounds for counting 2-SAT.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Proposition 31's inclusion-exclusion identity is false: the E/O split counts assignments falsifying an even number of clauses, not models of φ, so Lemma 4 is unproven.","rationale":"Read in good faith, the paper's central technical claim is Lemma 4, and its proof is Proposition 31 plus Lemmas 28-30. The rogue-model machinery is complex, but the first step of Proposition 31 is already wrong: the simplified inclusion-exclusion expression omits the binomial coefficients and the requirement that a fixed set of clauses be falsified. The correct IE expansion is #(φ)=Σ_{M}(1-1)^{k(M)}; the paper's expression is Σ_{M}Σ_{nc≤k(M)}(-1)^{nc}. These differ whenever some assignment falsifies an even positive number of clauses. The E/O sets defined in Proposition 31 are therefore not the non-rogue model sets of ψ1/ψ2, and the equality #(φ)=(|E|+|R|)-(|O|+|R|) is unsupported. This is not an artifact of notation: the same false identity would make the difference count every assignment with even falsification count. The concrete test on a two-clause unit formula can determine whether the construction itself is salvageable. Given the absence of machine-checked proofs or released code, and a false proof of the central lemma, the appropriate verdict is REJECT as written; a corrected proof could lead to conditional acceptance. The reader's rationale did flag a questionable inclusion-exclusion identity, but the formal weakest assumption was placed on the rogue-model bijection; I see the invalid E/O identity as the more fundamental gap, hence partial agreement.","tokens_in":35469,"tokens_out":10960,"duration_ms":121755,"concrete_test":"Take φ=(x)∧(x), choose the two-node labeled path decomposition from Section IV, apply Equations (1)-(12) exactly as written to obtain ψ1 and ψ2, and brute-force count #(ψ1)-#(ψ2). If the result is not 1, Lemma 4 is false and the main theorem collapses; if it is 1, the proof of Proposition 31 is still invalid and must be replaced with a correct counting argument before the theorem can be accepted.","verdict_should_be":"REJECT","load_bearing_attack":"Proposition 31 derives #(φ)=Σ_{M,0≤nc≤|φ|, M falsifies ≥nc clauses in φ} (-1)^{nc} and splits this into E (even nc) and O (odd nc). For any fixed assignment M that falsifies exactly k clauses, that sum is Σ_{nc=0}^{k} (-1)^{nc}, which equals 1 when k is even and 0 when k is odd. The correct inclusion-exclusion contribution is 1 if k=0 and 0 otherwise; non-satisfying assignments with an even number of falsified clauses are not cancelled. Concretely, φ=(x)∧(x) has #(φ)=1, but the E/O expression on the two assignments (k=0 and k=2) gives 2. Since Proposition 31 is the proof that #(φ)=#(ψ1)-#(ψ2), the false identity is what connects the non-rogue counts of ψ1 and ψ2 to #(φ). The rogue-model bijection (Lemmas 28-29) only cancels rogue models; it cannot correct a miscount of non-rogue models. Thus the central equality in Lemma 4 and all consequences (Theorems 3, 7, 12-14) are not established by the proofs as written.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents a reduction from #SAT to the difference of two #2SAT (and #2DNF) oracle calls, claiming that #(φ) = #(ψ1) − #(ψ2) for 2CNF formulas ψ1, ψ2 computable in linear time and logspace. From this main lemma it derives a characterization of gapP as the logspace closure of differences of #2SAT/#2DNF calls, strict separation results for #P, refined Toda-style theorems with AC0/TC0 postprocessing, a sparsification lemma for #2SAT/#2DNF, and parameterized lower bounds under (S)ETH. The proof of the main lemma rests on an inclusion-exclusion argument (Proposition 31) and a bijection between 'rogue models' of the two constructed formulas (Lemmas 28–30).","tokens_in":35727,"tokens_out":6563,"duration_ms":69999,"significance":"If the central lemma holds, the results are strong and novel: they would place #P strictly between one and two #2DNF calls, give a clean gapP characterization, improve Toda's theorem in a logspace-many-one framework, and yield linear-time parameter-preserving reductions with only additive treewidth overhead. The paper's constructive reductions and the explicit examples are valuable. However, the correctness proof as written contains a false inclusion-exclusion identity; until that is repaired, the main theorems are unproven. The flaw is concrete and appears in a load-bearing proposition, so the manuscript needs substantial revision.","major_comments":[{"comment":"The stated inclusion-exclusion identity is incorrect. For a fixed assignment M that falsifies exactly k clauses of φ, the contribution to the sum Σ_{0≤nc≤|φ|, M does not satisfy ≥nc clauses} (−1)^nc is Σ_{nc=0}^{k} (−1)^nc, which equals 1 if k is even and 0 if k is odd, not the indicator of k=0. Consequently the identities #(φ)=|E|−|O| and #(φ)=#(ψ1)−#(ψ2) do not follow. A concrete counterexample is φ=(x)∧(x), where #(φ)=1 but the E/O expression counts the falsifying assignment x=false as contributing 1, giving 2. The standard inclusion-exclusion identity uses subsets S of falsified clauses with weight (−1)^|S| and hence binomial coefficients; the paper's sum over thresholds 'at least nc' is not equivalent. This invalidates the proof of Lemma 4 and, with it, Theorems 3, 7, 12–14, Corollaries 5, 15, 18, and Corollary 26. The construction's non-rogue models may well encode subsets correctly, but the proof as written must be replaced by a correct subset-based argument.","section":"Appendix 9, Proposition 31"},{"comment":"The rogue-model bijection is not rigorously established for all tree-decomposition node types. Lemma 28's case analysis is incomplete: in Case (iii), the situation where exactly one of c. or c̄. lies in M is not discussed, and such a model may still be rogue at t via condition (ii) or (iv). For join nodes, the clauses (9)–(12) depend on two child nodes simultaneously, but Definition 23 flips parities only along a single root-to-leaf path; it is not shown that flipping along that path preserves satisfaction of the join-node clauses involving the other child. The proof also relies on an informal 'lexicographically smallest path' argument that is not made precise for general trees with empty-label and join nodes. A complete proof must handle all combinations of conditions (i)–(iv) and all node types, including the cubic-bipartite variants in Appendix 9-C.","section":"Appendix 9, Lemmas 28–30 and Definitions 22–23"},{"comment":"The relationship between 'nc' in the inclusion-exclusion sum and 'nc' in Lemma 30 is ambiguous. In Proposition 31 the summation variable ranges over thresholds ('M does not satisfy ≥nc clauses'), while in Lemma 30(1) nc is defined as the number of c. variables set true in a model M, and Lemma 30(2) asserts that nc is odd exactly for models of ψ2. These are different uses of the same symbol. To make the proof valid, the authors must define E and O as sets of non-rogue models of ψ1 and ψ2, respectively, and then prove that |E|−|O| equals the number of satisfying assignments of φ, e.g., by showing that non-rogue models of ψ1 (resp. ψ2) correspond bijectively to pairs (β,S) where S is an even-sized (resp. odd-sized) subset of clauses falsified by β, with each subset counted exactly once. The current text does not supply such a bijection.","section":"Proposition 31 and Lemma 30"}],"minor_comments":[{"comment":"The reported counts #(ψ1)=204,452 and #(ψ2)=204,450 are not derived; a brief explanation or a small verification table would help the reader confirm the subtraction yields #(φ)=2.","section":"Section IV, Example 21"},{"comment":"The notation for the two clause-auxiliary variables is inconsistent across the paper: the main text uses 'c.' and 'c̄.', while some appendix definitions write 'c.' and 'c̄.' with different spacing. Please standardize the symbols.","section":"Definitions 22, 35, 41"},{"comment":"The switch and monswitch constructions are described tersely; for instance the claimed equality #(α)=#(ψ1)+#(ψ'2)+#(β)+1 for monswitch requires a case analysis of the four settings of the switch variables, which should be spelled out.","section":"Appendix 10, proof of Theorem 7"},{"comment":"The bandwidth-preservation proof is hard to follow and appears to introduce many auxiliary batches and implications; a cleaner formal argument with explicit bounds for the dilation is needed.","section":"Appendix 9-A, Lemma 34"},{"comment":"The sparsification statement says 'there exists t∈N such that in time t·poly(n)', but the dependency of t on k and the precise construction of the γ_i^1, γ_i^2 formulas is not fully specified; the proof refers only to modifications of a cited lemma.","section":"Corollary 26"}],"recommendation":"major_revision","confidential_remarks":"The flaw in Proposition 31 is serious enough that the paper's main theorems are not established as written. However, the concrete construction suggests the intended subset-based inclusion-exclusion may be repairable, and the overall framework is plausible and interesting. I recommend major revision rather than rejection, provided the authors replace the erroneous identity with a correct proof and substantially tighten the rogue-model bijection arguments. I would also ask the program committee to consider whether the appendix is sufficiently detailed for LICS; the main text refers to the appendix for most proofs, and several appendix proofs are still at the level of 'it is easy to see'."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe stress-test is right, and it lands on the load-bearing step. Proposition 31's inclusion-exclusion identity is false: for a fixed assignment M that falsifies exactly k clauses, the sum over nc of (-1)^nc for M falsifying at least nc clauses is Σ_{nc=0}^k (-1)^nc, which is 1 for even k and 0 for odd k. That is not the indicator of M being a model. Their example φ=(x)∧(x) already gives 2 instead of 1. So Lemma 4 is not proven, and the characterizations of gapP and the PH results rest on it.\n\nThat said, the paper has real substance. The reduction construction is new and interesting: the idea of building two nearly identical 2CNFs and aligning rogue models by a parity flip along a tree decomposition is clever. The linear-size, structure-preserving reduction would be a strong contribution if correctness holds. The sparsification corollary for #2SAT is also a nice byproduct. The paper is well-organized and the presentation of the construction is clear.\n\nThe soft spot is not a minor typo. The definitions of E and O in Proposition 31 count each assignment multiple times, and the parity split does not implement inclusion-exclusion. The rogue-model bijection is developed in detail, but it only cancels rogue models; it cannot correct the miscount of non-rogue models. The monotone and cubic variants inherit the same gap.\n\nI would not cite this version. The claims are significant enough that a serious referee should see it, but the referee's main job is to check whether the construction can be repaired. If the authors can provide a correct proof of Lemma 4, the paper will be a strong LICS contribution; as written, the central result is unproven.\n\nFor the reading group: maybe—useful as a case study in how a clean-looking inclusion-exclusion can go wrong.\n\nRecommendation: accept for peer review, but flag Appendix 9 as requiring a full rewrite and a verified proof of Proposition 31.","headline":"Main reduction is clever, but the central correctness proof contains a false inclusion-exclusion identity; results unproven as written.","tokens_in":36247,"tokens_out":3673,"would_cite":false,"duration_ms":36270,"reading_group":"maybe","serious_thinker":"no","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q15","68Q17","68Q25"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves that subtracting the model counts of two 2CNF or 2DNF formulas captures gapP, placing #P strictly between one and two calls to a #2DNF oracle.","keywords":["counting complexity","#P","gapP","#2SAT","#2DNF","spanL","sparsification","SETH"],"falsifier":"Run the construction on a small CNF whose tree decomposition includes a join node and an empty-label node, then brute-force count models of the two output formulas: any instance with #(ψ1) − #(ψ2) different from #(φ) falsifies the rogue-model bijection and with it the central claim.","tokens_in":35288,"feed_emoji":"➖","tokens_out":8453,"duration_ms":76506,"temperature":0.7,"pith_summary":"The paper proves that counting the satisfying assignments of a 2DNF formula is, by itself, weak, but subtracting the counts of two such formulas is very strong: the difference captures gapP, the class of all functions obtainable as accepting minus rejecting paths of a nondeterministic polynomial-time machine. Since #P sits strictly inside gapP, this places #P strictly between one and two calls to a #2DNF oracle, a gap that would collapse NL and NP or UP and SPP if closed. The construction is a direct, linear-time/logspace reduction from #SAT that encodes inclusion-exclusion and cancels all errors through a symmetry between the two formulas. The same machinery yields a single #2DNF call plus AC0 or TC0 postprocessing that captures gapP and, consequently, the polynomial hierarchy.","feed_headline":"Two #2DNF calls minus one another capture gapP","feed_subtitle":"If true, #P sits strictly between one and two DNF-counting calls, and Toda's theorem needs only AC0 or TC0 postprocessing.","key_machinery":"The load-bearing object is the 'rogue model': in the two constructed formulas ψ1 and ψ2, every satisfying assignment that does not correspond to a genuine model of φ is paired by an explicit bijection, the symmetric rogue model construction, which flips the even/odd parity bits along the unique lexicographically first root-to-leaf path containing a rogue node. Because each rogue model of ψ1 maps to exactly one rogue model of ψ2 and vice versa, subtracting the two counts cancels all errors and leaves #(φ). The reduction is guided by a labeled tree decomposition, which is also what gives the additive parameter preservation for treewidth, bandwidth, and their incidence variants.","core_discovery":"The central discovery is a characterization: gapP = [#2SAT−#2SAT]^log = [#IMPL2SAT−#IMPL2SAT]^log = [#0,1-2DNF−#0,1-2DNF]^log = [#2DNF−#2DNF]^log = [#MON2SAT−#MON2SAT]^log = [#MON2DNF−#MON2DNF]^log = spanL−spanL, and hence #P is strictly sandwiched between one and two #2DNF oracle calls. The proof rests on a new reduction from #SAT to two 2CNF formulas ψ1 and ψ2 with #(φ) = #(ψ1) − #(ψ2), computable in linear time or logspace and preserving treewidth, incidence treewidth, bandwidth, and incidence bandwidth up to small additive constants. The reduction works even for monotone 2CNF/2DNF and for cubic bipartite implication formulas, so subtraction compensates both for missing negations and for missing long clauses. As corollaries the paper derives sparsification for #2SAT and #2DNF, an O($2^{{itw(φ)}}$|φ|) algorithm for #SAT, SETH-tight lower bounds, and refined Toda-type inclusions PH ⊆ [#MON2SAT]^log_TC0 = [#MON2DNF]^log_TC0 and PH ⊆ [#IMPL2SAT]^log_AC0.","pith_inferences":["Beyond the paper, the rogue-model symmetry is a general template: any counting problem with a tree-decomposition-guided reduction and a parity-like error structure may admit a two-call subtraction characterization, even where negation is absent.","Because the two formulas differ by at most one literal or variable occurrence, the result suggests that 'subtraction strength' is measured by how much symmetry a fragment can support; testing fragments between MON2SAT and full 2SAT would map that trade-off.","The AC0/TC0 postprocessing results suggest a hierarchy of single-call characterizations: weaker fragments need stronger postprocessing; quantifying this trade-off for fragments such as 1DNF or HORN2SAT could refine the boundary of Toda's theorem.","The conjecture that [FP−#MON2SAT]^log is strictly weaker than [#MON2SAT−#MON2SAT]^log, if settled, would show that both calls must be to the same counting oracle; an FP oracle cannot replace one of them."],"forward_implications":["If correct, #P is strictly contained between one and two #2DNF oracle calls under standard assumptions; closing the gap would show NL = NP or UP = SPP.","A single subtraction exactly compensates for the absence of negation: monotone #2SAT and #2DNF differences still capture gapP.","One #2DNF call plus AC0 or TC0 postprocessing captures gapP and the polynomial hierarchy, giving a logspace-computable refinement of Toda's theorem.","Linear-time, parameter-preserving reduction yields an O(2^{itw(φ)}|φ|) algorithm for #SAT and SETH-tight lower bounds for #2SAT fragments.","Any d-CNF can be sparsified into a sum of differences of sparse 2-CNF (or 2-DNF) model counts, extending sparsification to the k=2 case."],"supporting_citations":[{"why":"Supplies the solution-preserving Cook-Levin reduction making #SAT #P-complete; the reduction being replaced and the basis for logspace many-one closures.","marker":"[44]"},{"why":"Defines spanL and shows #DNF is in spanL with spanL properly contained in #P unless NL = NP; establishes the 'one call' side of the sandwich.","marker":"[2]"},{"why":"Shows gapP equals the difference of two #P functions; the target class that Theorem 7 characterizes.","marker":"[20]"},{"why":"Proves PH is contained in P with one #P call; the theorem that the paper refines to AC0 and TC0 postprocessing.","marker":"[42]"},{"why":"Provides the #ETH sparsification framework for d-CNF used in Corollary 26.","marker":"[17]"},{"why":"Gives the O(2^{itw}|φ|) algorithm via zeta and Möbius transforms that Corollary 15 reproduces with a plain dynamic program.","marker":"[39]"},{"why":"Shows division is computable in TC0; used to extract counts in the single-call Theorems 12 and 13.","marker":"[27]"},{"why":"States SETH, the hypothesis behind the lower-bound Theorems 16 and 17.","marker":"[30]"}],"fun_headline_variants":["Subtract two #2DNF calls, capture gapP","gapP from subtracting two #2DNF counts","Two #2DNF calls, one subtraction, equals gapP","#P sandwiched between one and two #2DNF calls","One #2DNF call isn't enough; subtraction of two gives gapP"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The paper's central equality #(φ) = #(ψ1) − #(ψ2) collapses if the symmetric pairing of rogue models fails for any labeled tree-decomposition node, in particular for join nodes or nodes with empty labels; the entire sandwich and gapP characterization rests on that bijection.","fun_headline_variants_meta":{"raw":{"variants":["Subtract two #2DNF calls, capture gapP","gapP from subtracting two #2DNF counts","Two #2DNF calls, one subtraction, equals gapP","#P sandwiched between one and two #2DNF calls","One #2DNF call isn't enough; subtraction of two gives gapP"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001538,"raw_usage":{"total_tokens":6327,"prompt_tokens":1294,"completion_tokens":5033,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":910,"completion_tokens_details":{"reasoning_tokens":4944}},"tokens_in":910,"tokens_out":5033,"duration_ms":34549,"temperature":1.0,"reasoning_tokens":4944,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T05:52:45.462891+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the construction on a small CNF whose tree decomposition includes a join node and an empty-label node, then brute-force count models of the two output formulas: any instance with #(ψ1) − #(ψ2) different from #(φ) falsifies the rogue-model bijection and with it the central claim.","supporting_citations":[{"cited_title":"A very hard log-space counting class.Theor","cited_arxiv_id":null,"evidence_quote":"Defines spanL and shows #DNF is in spanL with spanL properly contained in #P unless NL = NP; establishes the 'one call' side of the sandwich."},{"cited_title":"A faster algorithm for propo- sitional model counting parameterized by incidence treewidth","cited_arxiv_id":null,"evidence_quote":"Gives the O(2^{itw}|φ|) algorithm via zeta and Möbius transforms that Corollary 15 reproduces with a plain dynamic program."},{"cited_title":"Mix Barrington","cited_arxiv_id":null,"evidence_quote":"Shows division is computable in TC0; used to extract counts in the single-call Theorems 12 and 13."},{"cited_title":"On the complexity of k- SAT.Journal of Computer and System Sciences, 62(2):367–375, 2001","cited_arxiv_id":null,"evidence_quote":"States SETH, the hypothesis behind the lower-bound Theorems 16 and 17."}],"review_version":1}