{"id":"c216a901-0a63-4b4d-9445-7418204d5e4b","arxiv_id":"2507.14504","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"New branch-and-search algorithms solve weighted #2-SAT in O*(1.1082^m) time and weighted #3-SAT in O*(1.4423^m) time, improving known clause-count bounds.","lead":"This paper gives faster worst-case algorithms for counting the satisfying assignments of 2-SAT and 3-SAT formulas, where runtime is measured by the number of clauses. The new bounds improve earlier results and may strengthen exact model counting tools used in probabilistic reasoning.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 9's q>=2 claim is false for constant-size reduced formulas; the proof of Theorem 4's branching vectors needs a size caveat before the 1.1082^m bound follows.","rationale":"The reader's weakest assumption was the unproved adaptation of Samer-Szeider pathwidth DP to weighted model counting. That is worth flagging, but it is less load-bearing: carrying literal weights through a pathwidth DP is a standard bookkeeping change, and even if the dual-graph DP requires tables over 3(p+1) variables rather than p+1, the #3-SAT phase-three time would be at most about 1.4142^m, still below the claimed 1.4423^m branch bound. The concrete mathematical defect I found is in Lemma 9: the proof that q2+q>=3 >= 2 fails when F1 is the whole formula, and explicit reduced 2-CNF formulas show the claimed branching vectors (5,11) and (4,11) are not achieved on those constant-size instances. This is a genuine error in the paper's internal argument. However, the counterexamples have bounded size, and the same reduction rules that the paper uses would route such small formulas to the brute-force phase if n <= n_epsilon, so the asymptotic central claim appears salvageable with a repaired lemma. Because the paper's proof as written does not establish the theorem and requires this repair, the reader's CONDITIONAL verdict remains appropriate; I do not see grounds to reject the algorithms outright.","tokens_in":21088,"tokens_out":42520,"duration_ms":355376,"concrete_test":"Analytically re-derive Lemma 9 with the F2=empty case separated: prove that for every reduced 2-CNF with n(F) > n_epsilon, either q2+q>=3 >= 2 or a reduction rule applies, and verify Lemmas 10 and 11 still yield branch vectors not worse than (5,11) and (4,11) on that domain. Then computationally instantiate Alg2CNF on the two explicit gadgets (the 5-neighbor 5-cycle and the 4-neighbor K4) and on connected chains of such gadgets formed by merging pairs of 4-variables so that n is unbounded; record (Δt,Δf) at the first branch. If any chain yields a branch vector worse than (4,11) on an unbounded family, the recurrence root exceeds 1.1082 and Theorem 4's bound fails; if the minimum for n>n_epsilon remains (4,11), the gap is confined to constant-size inputs and the asymptotic claim survives.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing step for the #2-SAT bound is Lemma 9(2), which underlies the (5,11) and (4,11) branching vectors in Lemmas 10 and 11. In the proof of Eq. (4), the paper asserts q>=3+q2 >= 2 for every reduced formula F, arguing that with F1 = S0 union S1 union S2 and F2 = F \\ F1, having q2+q>=3 = 0 triggers R-Rule 8 and having q2+q>=3 = 1 triggers R-Rule 9, since |var(F1)| = 1+d <= 8. This overlooks the case F2 = empty, which the rules' 'non-empty sub-formulas' requirement excludes. Example: clauses (x∨a_i) for i=1..5 plus (a1∨a2), (a2∨a3), (a3∨a4), (a4∨a5), (a5∨a1). This reduced 2-CNF has d=5, N(x) ⊆ N3(x), q2=q>=3=0, F1=F, and no split rule applies. Branching on x gives Δt=5 (x=1 leaves a 5-cycle) and Δf=10 (x=0 forces all a_i=1), so Δt+Δf=15, while Lemma 9(2) claims >=16. The analogous 4-variable construction (x adjacent to a,b,c,d plus a K4 on them) gives the Line-8 branch vector (4,10) instead of (4,11); its root τ(4,10) is about 1.1115, exceeding the phase-three base 2^{4/27} ≈ 1.1082. These bad gadgets are constant-size (n<=6), so an asymptotic proof can probably absorb them via the n<=n_epsilon brute-force phase, and the q>=2 claim may be repairable for all sufficiently large connected instances. But as written, Lemma 9 is false at a step the stated proof of Theorem 4 crucially depends on.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes two algorithms for weighted model counting. Alg2CNF solves WMC on 2-CNF formulas in claimed O*(1.1082^m) time, and Alg3CNF solves WMC on 3-CNF formulas in claimed O*(1.4423^m) time, where m is the number of clauses. The algorithms combine nine reduction rules, simple branching on high-degree variables, and phase-three calls to path-decomposition-based dynamic programming. The paper also reuses a pathwidth bound of Fomin et al. to control low-degree residual formulas and includes an appendix explaining a flaw in the earlier #3-SAT analysis of Zhou et al.","tokens_in":1298,"tokens_out":2042,"duration_ms":114539,"significance":"If the claimed bounds are correct, the paper gives a substantial improvement over the previous clause-parameter #2-SAT bound of O*(1.1892^m) and provides the first valid clause-parameter bound for weighted #3-SAT at O*(1.4423^m). The overall framework, combining a small set of reduction rules with a pathwidth phase, is attractive and could be useful beyond the two problems treated here. The reduction-rule correctness proofs and the #3-SAT measure analysis are largely clear. However, the proof of the central #2-SAT branching lemma contains a concrete false claim, and the weighted version of the path-decomposition algorithms is asserted without proof; both points must be repaired before the main theorems are fully supported.","major_comments":[{"comment":"The proof that q>=3 + q2 >= 2 for every reduced formula is incomplete: the argument applies R-Rule 8 to F1 = S0 union S1 union S2 and F2 = F \\ F1 only when both subformulas are non-empty, but the case F2 = empty is not excluded. This is not merely a formal gap. Consider the reduced 2-CNF formula F = (x v a_i) for 1 <= i <= 5 together with (a_i v a_{i+1}) for 1 <= i <= 5 with indices modulo 5. For this formula d = 5, N2(x) is empty, q2 = q>=3 = 0, F1 = F and F2 is empty; none of R-Rules 8 or 9 applies, and branching on x gives Delta_t = 5 and Delta_f = 10, so Delta_t + Delta_f = 15 < 16, contradicting Lemma 9(2). The problem also appears at the Line-8 branching: the analogous 4-variable construction with a K4 on the neighbors of x gives the branch vector (4,10), whose branching factor is about 1.1115, larger than the phase-three base 2^(4/27) which is about 1.1082. Since Lemma 10 and Lemma 11 derive their branching vectors from Lemma 9(2), the proof of Theorem 4 as written does not establish the claimed O*(1.1082^m) bound. A repair appears possible by restricting Lemma 9 to sufficiently large connected formulas and absorbing the bounded-size exceptions with the brute-force base, but that restriction and the resulting recurrence analysis are not present in the manuscript.","section":"Section 4.1, Lemma 9, Eq. (4)"},{"comment":"The paper states that the Samer-Szeider algorithms for #SAT can be adapted to solve the weighted version without increasing the time complexity, but it gives no proof, no construction, and no citation for a weighted version. Both Alg2CNF at Line 11 and Alg3CNF at Line 8 terminate by invoking these algorithms, so the claimed weighted bounds depend on this adaptation. In particular, the weighted dynamic program must maintain products of literal weights over the bags of the path decomposition, and the table size and transition complexity need to be stated precisely to confirm that the O*(2^p) time carries over with p as the pathwidth. Without this information, the weighted claims are not fully supported.","section":"Section 2.2, Theorems 2 and 3"}],"minor_comments":[{"comment":"In the paragraph beginning 'This paper focuses on #SAT', the phrase 'For comprehensive surveys, For comprehensive surveys' is duplicated.","section":"Section 1"},{"comment":"The word 'fomrula' should be 'formula'.","section":"Lemma 12 proof"},{"comment":"The word 'decreses' should be 'decreases'.","section":"Lemma 13 proof"},{"comment":"In the partition written as 'Sin_3 union Sout_3', the subscript 3 is likely intended to be 2; as written it conflicts with the definition of S2.","section":"Lemma 9 and Figure 1"},{"comment":"The displayed expression 'm = 2n2 + 3n3 + 4n4 / 2' is ambiguous; the numerator should be parenthesized as (2n2 + 3n3 + 4n4)/2.","section":"Lemma 12, Eq. (6)"},{"comment":"The phase-three entry '1.1225 1/alpha = 1.2011' is easy to misread; the text should explicitly state that the phase-three base is 1.1225^(1/alpha) approximately 1.2011 when alpha = 0.6309297.","section":"Table 1"}],"recommendation":"major_revision","confidential_remarks":"The concrete counterexample to Lemma 9 should be communicated to the authors, since it directly affects the proof of the main #2-SAT theorem. The weighted-path-decomposition gap is also substantive and needs to be addressed. Both issues seem repairable within the scope of the paper, so I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this paper has two big claims, and they are not in the same shape. The #3-SAT analysis is a real advance: a clean measure argument with alpha tuned to 0.6309297 gives the first valid sub-2^m clause-count bound for weighted #3-SAT, and the appendix correctly diagnoses why the earlier Zhou et al. analysis was invalid. The #2-SAT analysis, however, has a concrete hole that needs fixing before the advertised 1.1082^m bound follows.\n\nWhat is good: the reduction rules are mostly standard but the R-Rule 8/9 constant-size decomposition is used cleverly; Lemma 13 and Lemma 14 for #3-SAT check out; and the pathwidth phase is a sensible way to kill low-degree cases. The paper is honest in its appendix and does not overclaim. For the #3-SAT side, I would be comfortable sending this to a serious referee now.\n\nThe soft spot is Lemma 9(2), which is load-bearing for the #2-SAT branching vectors. The proof claims q2 + q>=3 >= 2 for every reduced formula, but that is false when F2 is empty. The stress-test gadget works: x connected to five degree-3 variables arranged in a 5-cycle is reduced, has q2 = q>=3 = 0, and branching on x gives (5,10), not (5,11). The analogous 4-variable version gives (4,10), whose branching factor is about 1.1115, bigger than the phase-three base 2^{4/27} ≈ 1.1082. These gadgets are constant-size, so the theorem is probably repairable by adding an explicit size caveat and absorbing small formulas into the brute-force phase, but the paper does not do that. As written, the proof of Theorem 4 does not go through.\n\nTwo smaller issues: the adaptation of Samer-Szeider pathwidth DP to weighted model counting (Theorems 2 and 3) is asserted with no details; I believe it is standard, but it should be spelled out. Also the introduction cites the previous #2-SAT bound as both 1.1892^m and 1.1740^m, and that inconsistency should be cleaned up.\n\nBottom line: the paper deserves peer review, not desk rejection. The #3-SAT result is likely publishable as is; the #2-SAT result is likely correct after a nontrivial but manageable fix. A referee should ask for the repair, not reject the manuscript.","headline":"Worth refereeing, but the #2-SAT proof has a real gap in Lemma 9; the #3-SAT side is the stronger part.","tokens_in":22103,"tokens_out":7489,"would_cite":true,"duration_ms":328876,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves that weighted model counting on 2-CNF formulas is solvable in O*(1.1082^m) time and on 3-CNF formulas in O*(1.4423^m) time, improving prior upper bounds for #2-SAT and #3-SAT.","keywords":["weighted model counting","#2-SAT","#3-SAT","branch-and-search","path decomposition","pathwidth","CNF formula","exact algorithms"],"falsifier":"Enumerate all reduced 2-CNF and 3-CNF formulas up to a fixed size and record the actual clause-decrease pairs from each branch plus the pathwidth of the remaining primal or dual graph; a single branch worse than the claimed vectors, or a remaining graph whose pathwidth exceeds the claimed (4/27+ε)m or (1/6+ε)m ratio, would refute the corresponding theorem.","tokens_in":20880,"feed_emoji":"🧮","tokens_out":8413,"duration_ms":95913,"temperature":0.7,"pith_summary":"This paper aims to prove faster worst-case algorithms for counting satisfying assignments of Boolean formulas whose clauses have at most two or three literals, including the weighted version where each literal carries a weight. It claims that weighted #2-SAT can be solved in O*(1.1082^m) time and weighted #3-SAT in O*(1.4423^m) time, where m is the number of clauses. These bounds improve the previous #2-SAT upper bound and supply a valid clause-count algorithm for #3-SAT, whose earlier analysis is shown to be flawed. Model counting is #P-complete and underpins probabilistic inference, reliability estimation, and explainable-AI tasks, so tighter worst-case bounds for restricted clause lengths advance both theory and practice.","feed_headline":"Counting 2-SAT and 3-SAT models drops to 1.1082^m and 1.4423^m","feed_subtitle":"The new worst-case bounds count weighted satisfying assignments and beat the previous #2-SAT and #3-SAT results.","key_machinery":"The machinery is a two-stage hybrid of branch-and-search and pathwidth dynamic programming. Path decompositions arrange a graph's vertices into overlapping bags along a line so that each edge appears in some bag, and the pathwidth is the maximum bag size minus one; the algorithms rely on a known bound that expresses pathwidth through the numbers of low-degree vertices. Nine reduction rules simplify formulas without changing the weighted model count, including rules that eliminate duplicate literals, tautologies, subsumed clauses, unit clauses, unused variables, and constant-size components. The central inequality Lemma 9 lower-bounds how much branching on a variable decreases m for 2-CNF formulas, producing branching vectors no worse than (5,11) and (4,11), while Lemma 13 bounds the decrease of the hybrid measure for 3-CNF formulas and yields the four α-dependent branching vectors used to balance the runtime.","core_discovery":"The central claim is that two algorithms, Alg2CNF and Alg3CNF, solve weighted model counting on 2-CNF and 3-CNF formulas in O*(1.1082^m) and O*(1.4423^m) time respectively. Both algorithms exhaustively apply nine reduction rules, then branch on high-degree variables, and finally, once only low-degree variables remain, build a path decomposition of the primal graph for #2-SAT or the dual graph for #3-SAT and run a pathwidth-based dynamic program. The #2-SAT analysis shows that the remaining primal graph has pathwidth at most (4/27+ε)m, giving phase-three time O*(1.1082^m); the #3-SAT analysis uses the measure μ(F)=m3(F)+α·m2(F) with α=0.6309297 and exploits a degree-at-most-2 dual graph to reach O*(1.4423^m). The paper also documents a flaw in the previous #3-SAT analysis: assigning a value to the chosen variable need not remove any clause, so the old branching vector of (2,2) was unjustified.","pith_inferences":["I would not treat the constants 1.1082 and 1.4423 as tight: the pathwidth bounds use worst-case degree distributions, and refined structural arguments could push them lower without changing the framework.","The weighted adaptation of the path-decomposition dynamic programs is worth testing directly: if literal weights force the DP tables to store sums over weighted products rather than plain counts, the O*(2^p) phase-three claim could fail on weighted formulas even though unweighted counting works.","A practical implementation could use this algorithm as a fallback for low-degree cores in modern model counters, since the phase-three structures (maximum degree 4 for 2-CNF and 2 for 3-CNF) are exactly the hard-to-branch cores that current counters handle heuristically.","The same hybrid measure idea may extend to k-CNF formulas for k>3 with more clause-length parameters, although the paper leaves whether any constant c<2 exists for fixed k as an open question."],"forward_implications":["Unweighted #2-SAT and #3-SAT inherit the same upper bounds, since unweighted counting is the special case of weighted model counting with all literal weights equal.","The #2-SAT bound O*(1.1082^m) improves on the previous O*(1.1892^m) algorithm of Zhou et al.","The #3-SAT bound O*(1.4423^m) is the first valid worst-case clause-count algorithm of that form for #3-SAT, because the earlier analysis failed to guarantee a clause decrease in every branch.","Because the algorithms solve the weighted problem directly, applications such as probabilistic inference and explainable-AI reasoning inherit the improved worst-case guarantee in clause count.","The branch-then-path-decompose recipe, with a tunable clause-length measure, may apply to other counting problems parameterized by the number of clauses."],"supporting_citations":[{"why":"Supplies the path-decomposition dynamic programs for model counting that the algorithms invoke in their final phase.","marker":"[28]"},{"why":"Supplies the pathwidth bound in Theorem 1 that turns low-degree structural conditions into the width used in the runtime bound.","marker":"[17]"},{"why":"Defines the previous #2-SAT bound and the #3-SAT approach whose analysis Appendix A shows to be flawed.","marker":"[34]"},{"why":"Provides the branching-vector recurrence framework and the comparison lemma used to certify all branching steps.","marker":"[16]"},{"why":"Shows that general CNF model counting cannot have an O*(c^m) algorithm with c<2 unless SETH fails, motivating the restriction to bounded clause length.","marker":"[7]"}],"fun_headline_variants":["Faster #2-SAT and #3-SAT counting: 1.1082^m and 1.4423^m","New bounds for #2-SAT and #3-SAT counting: 1.1082^m and 1.4423^m","#2-SAT and #3-SAT counting improved to 1.1082^m and 1.4423^m","Weighted #2-SAT and #3-SAT solved in 1.1082^m and 1.4423^m","New #2-SAT and #3-SAT counting algorithms hit 1.1082^m and 1.4423^m"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing assumption is that the known path-decomposition dynamic programs for counting satisfying assignments can be adapted to weighted model counting with the same O*(2^p) running time, and the paper asserts this adaptation without supplying details or a reference.","fun_headline_variants_meta":{"raw":{"variants":["Faster #2-SAT and #3-SAT counting: 1.1082^m and 1.4423^m","New bounds for #2-SAT and #3-SAT counting: 1.1082^m and 1.4423^m","#2-SAT and #3-SAT counting improved to 1.1082^m and 1.4423^m","Weighted #2-SAT and #3-SAT solved in 1.1082^m and 1.4423^m","New #2-SAT and #3-SAT counting algorithms hit 1.1082^m and 1.4423^m"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001655,"raw_usage":{"total_tokens":6583,"prompt_tokens":970,"completion_tokens":5613,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":586,"completion_tokens_details":{"reasoning_tokens":5448}},"tokens_in":586,"tokens_out":5613,"duration_ms":41959,"temperature":1.0,"reasoning_tokens":5448,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T15:59:00.943233+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Enumerate all reduced 2-CNF and 3-CNF formulas up to a fixed size and record the actual clause-decrease pairs from each branch plus the pathwidth of the remaining primal or dual graph; a single branch worse than the claimed vectors, or a remaining graph whose pathwidth exceeds the claimed (4/27+ε)m or (1/6+ε)m ratio, would refute the corresponding theorem.","supporting_citations":[{"cited_title":"Algorithms for propositional model counting","cited_arxiv_id":null,"evidence_quote":"Supplies the path-decomposition dynamic programs for model counting that the algorithms invoke in their final phase."},{"cited_title":"Fomin, Serge Gaspers, Saket Saurabh, and Alexey A","cited_arxiv_id":null,"evidence_quote":"Supplies the pathwidth bound in Theorem 1 that turns low-degree structural conditions into the width used in the runtime bound."},{"cited_title":"at least two clauses are removed when we assign a value to x","cited_arxiv_id":null,"evidence_quote":"Defines the previous #2-SAT bound and the #3-SAT approach whose analysis Appendix A shows to be flawed."}],"review_version":1}