{"id":"9341fa45-e51d-43e2-9b74-c184c0d63114","arxiv_id":"2508.06264","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Weighted model counts can be computed with guaranteed decimal precision by a hybrid of floating-point, interval, and rational arithmetic, with a proven rounding bound for nonnegative weights on decision-DNNF formulas.","lead":"This paper shows how to compute weighted model counts with guaranteed numerical precision by combining floating-point arithmetic, interval arithmetic, and exact rational arithmetic. For nonnegative weights it proves that rounding errors in decision-DNNF counting grow only logarithmically with the number of variables, so certified precision is feasible at high speed.","discovery_kind":"first_principles","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1 is a rounding-error bound conditional on no under/overflow; plain IEEE double violates that assumption in the paper's own data, and ERD's range extension is not analyzed as part of the theorem.","rationale":"Theorem 1 appears mathematically sound under its stated assumptions: the Lemma 1 induction and the multiplication/addition recurrences satisfy the n <= 1/(2*sqrt(epsilon)) constraint, and the constants leave enough slack to absorb cross terms. The weakest point is not the rounding analysis but the gap between the theorem's idealized floating-point model and the implementations advertised in the headline. The paper's own data demonstrate that plain IEEE Double routinely violates the no-underflow/overflow assumption, so the p=53 guarantee is not usable for IEEE Double without the ERD extension. For ERD, the paper gives a plausible implementation sketch but no rigorous proof that ERD operations are equivalent to correctly rounded p=53 arithmetic; without that, Theorem 1 does not automatically transfer. This is exactly the reader's weakest assumption, and it is load-bearing for the central claim. The decision-DNNF restriction in the abstract is a real overstatement but does not undermine the theorem itself. The verdict should remain CONDITIONAL, matching the reader's assessment.","tokens_in":19526,"tokens_out":28887,"duration_ms":352875,"concrete_test":"Run the 1000 nonnegative-weight instances with the ERD library, using MPQ (or a high-precision rational fallback) as ground truth, and check every instance against the Equation 8 lower bound for p=53, 8.11 decimal digits. If any ERD result falls below that bound while the ground-truth computation completes, ERD's arithmetic is not a faithful p=53 model and Theorem 1 does not support the ERD row of Table 1. If all meet the bound, the range-extension claim is validated and the remaining issue is the overstatement for plain IEEE Double.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central guarantee (Theorem 1, Eq. 8) is proved only under the Section 3 assumption that 'all floating-point computations can be performed without underflow or overflow.' That assumption is load-bearing: the paper's own nonnegative-weight experiments show plain IEEE double fails on 628 of 1000 random instances (419 overflows, 209 underflows) and 45 of 100 original instances (5 overflows, 40 underflows). The abstract and Table 1 nevertheless present p=53 as guaranteeing about 8.11 decimal digits for 'IEEE Double / ERD.' For plain IEEE Double this is not a guarantee about the computation that actually runs; for ERD the guarantee is not a consequence of Theorem 1 unless ERD's addition and multiplication are proved to introduce no more error than one correctly rounded p=53 operation per arithmetic step. The paper asserts ERD's correctness informally (Section 7) but does not provide a rounding-error analysis of the representation. Thus the practical headline 'floating-point can be fully trusted' is only as strong as the range-extension implementation. Separately, the abstract's nonnegative-weight claim omits the theorem's decision-DNNF restriction; this overstates scope but is not a proof gap.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies numerical precision in weighted model counting. It proves that for a decision-DNNF formula over n variables with nonnegative literal weights, a p-bit floating-point evaluation — provided no underflow or overflow occurs and log2 n <= p/2 - 1 — yields decimal precision at least p log10 2 - log10 n - c, where c = log10 7 when rescaling is used and log10 4 otherwise (Theorem 1, Eq. 8). To make this practical, the paper introduces ERD, a representation pairing an IEEE double with a 64-bit exponent, and combines ERD/MPF with MPFI interval arithmetic and MPQ rational arithmetic in a hybrid strategy. Experiments on MC2024 benchmarks and adversarially constructed formulas validate the bound and demonstrate large speedups over rational arithmetic while achieving target precision D = 30.","tokens_in":19838,"tokens_out":17793,"duration_ms":211324,"significance":"If the claims hold, this is a useful and nontrivial result: it gives a parameter-free, a-priori precision guarantee for floating-point weighted model counting on decision-DNNF formulas, and it provides a practical hybrid scheme that is substantially faster than exact rational arithmetic. The proof of Theorem 1 is clean, the constants are not fitted, and validation against exact MPQ ground truth makes the bound falsifiable. The practical headline, however, is currently stronger than what is proved: the theorem is conditional on no under/overflow, and the ERD representation is not formally analyzed. There is also a small but real off-by-one error in the generalized sum bound of Section 4.4. These issues are fixable and do not undermine Theorem 1 itself.","major_comments":[{"comment":"The recursive bound for sums is off by one. The text defines e(v)=1 for a rounded constant and states e(sum_{i=1..k} psi_i) = ceil(log2(k-1)) + max_i e(psi_i). For k=2 constants, a balanced binary addition performs one rounded addition; from §4.2 the error coefficient is max(e1,e2)+1 = 2, but the formula gives ceil(log2 1) + 1 = 1. Thus the claimed integer bound understates the true rounding error, which invalidates the stated precision guarantee for the general d-DNNF/MDD evaluation method. Replacing k-1 by k (or otherwise adding 1 to the bound) fixes the problem.","section":"§4.4"},{"comment":"Theorem 1 is conditional on the standing assumption in §3 that all floating-point computations are performed without underflow or overflow. The paper's own data show plain IEEE double fails on 628 of 1000 nonnegative instances and 45 of 100 original instances, so the Table 1 entry 'IEEE Double / ERD' is not a guarantee for computations that actually run in IEEE double. For ERD, the theorem can only apply if ERD addition and multiplication introduce no more error than one correctly rounded p=53 operation per arithmetic step. Section 7 gives an algorithm but no lemma establishing this: the e1 > 54+e2 shortcut, the normalization step, and the claim that the 64-bit exponent prevents range failures in all intermediate operations are asserted informally. Without such a lemma, the stated p=53 guarantee for ERD is an assertion rather than a consequence of Theorem 1. I request a formal statement","section":"§3, §7, Table 1"}],"minor_comments":[{"comment":"The abstract's claim 'When all weights are nonnegative, we prove that the precision loss ... can be tightly bounded' omits the decision-DNNF restriction and the no-underflow/no-overflow condition. These are central hypotheses of Theorem 1 and should be stated or at least clearly referenced.","section":"Abstract"},{"comment":"After Lemma 2, the text says that combining the lemmas gives Theorem 1, but it does not show the cross-term control for the product W(phi)·P. Under n <= 1/(2 sqrt(epsilon)) the cross term contributes at most 3 epsilon, yielding the coefficient 7n for the rescaling case. Adding this one-line derivation would make the constant c = log10 7 self-contained.","section":"§4.3"},{"comment":"There are several typographical errors: 'Indecision decomposable negation-normal form' in §2 should be 'decision'; 'satisifes' in §7; 'diagrmas' in reference [1]; 'reliablity' in reference [23]; 'arithetic' in §6; 'suprisingly' in §4.6; and 'nonnnegative' in the Table 2 caption.","section":"Typos"},{"comment":"The phrase 'the precision provided by IEEE Double and ERD guarantees decimal precisions 8.11' should be qualified: for IEEE Double, this holds only when the computation stays within the representable range; ERD is the mechanism that makes the range assumption plausible. As written, it reads as a guarantee for plain IEEE double.","section":"§4.3, Table 1"}],"recommendation":"major_revision","confidential_remarks":"The off-by-one in Section 4.4 is a genuine mathematical slip but is trivially corrected. The larger issue is the missing formal analysis of ERD: the central practical claim depends on it, and a referee report can reasonably ask for a lemma before accepting. I see no grounds for rejection, since Theorem 1 itself appears sound and the experiments are consistent with it. The paper's self-citations are background and are not circular."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Main take: this is a genuinely useful numerical analysis for weighted model counting. Theorem 1 gives an explicit, tight bound on decimal precision loss for floating-point evaluation on decision-DNNF formulas with nonnegative weights, and it appears to be correct. The induction in Lemma 1 and Theorem 1 is clean, the constants check out, and the experiments (MC2024 benchmarks, MPQ ground truth) stay above the predicted bound. The ERD representation plus the interval/rational hybrid is practical; the hybrid completes all 2500 instances with substantial speedups over rational arithmetic. This is a real contribution to the WMC/BDD community.\n\nThe soft spots are mostly about scope versus headline. The abstract states the nonnegative guarantee without the decision-DNNF restriction and without the no-underflow/no-overflow assumption. That matters because plain IEEE double fails on 45 of 100 original and 628 of 1000 random instances in the paper's own data. The theorem is conditional on no under/overflow, and for plain double that condition is often false. For ERD, the range extension is described but not formally analyzed; the theorem's bound only applies if each ERD add and multiply has the same one-unit rounding error as a standard double operation. That is probably true given how ERD is implemented, but the paper should prove it or at least state it as an assumption. Section 4.4's general structural bound is only sketched and not validated; treat it as a heuristic. No code or data is shipped, so reproduction is harder.\n\nNone of this breaks the core result. The mathematical argument is sound and the experiments are honest, including showing where double fails. I would send this to review. The right revision is to qualify the abstract, give a short proof or explicit assumption for ERD's error properties, and ideally release the ERD library and benchmark scripts.","headline":"Real precision bound for WMC with honest experiments; abstract oversells scope but core math holds.","tokens_in":20239,"tokens_out":4049,"would_cite":true,"duration_ms":39566,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["65G50","65G30"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper proves that weighted model counting over decision-DNNF formulas with nonnegative weights can be performed with floating-point arithmetic while guaranteeing a tightly bounded loss of precision: roughly p\\cdot\\log_{10}2 - \\log_{10}","keywords":["weighted model counting","floating-point arithmetic","rounding error","decision-DNNF","interval arithmetic","extended-range double","rational arithmetic","precision guarantee"],"falsifier":"Evaluate a smooth decision-DNNF formula over n variables (with n ≤ $2^{{p/2−1}}$) using all literal weights equal to a value slightly greater than 1, a p-bit floating-point format, and directed rounding so every operation rounds upward. The theorem predicts the relative error of the computed count versus an exact rational computation is at most (4n−2)·$2^{{−p}}$; any observed relative error exceeding this bound would refute Theorem 1.","tokens_in":19456,"feed_emoji":"🧮","tokens_out":5327,"duration_ms":60990,"temperature":0.7,"pith_summary":"This paper's central claim is that weighted model counting over decision-DNNF Boolean formulas with nonnegative literal weights can be done with floating-point arithmetic while guaranteeing a tightly bounded loss of precision. The bound is Theorem 1: with a p-bit fraction and n variables, the computed count has decimal precision at least p log10 2 − log10 n − c, where c is a small constant (about 0.6–0.85). The proof works by chaining per-operation rounding-error bounds through an induction on formula structure, exploiting the two structural properties of the decision-DNNF representation: decomposable conjunctions (whose variable sets are disjoint) and disjunctions that branch on a single decision variable (which bounds addition depth by n). The paper also introduces the extended-range double (ERD), a standard double augmented with a 64-bit exponent, to eliminate the underflow/overflow failures that plague plain doubles (628 of 1000 random instances failed with plain double), and a hybrid scheme mixing floating-point, interval, and rational arithmetic to achieve user-specified precision even when weights mix positive and negative values. The intended consequence is that probabilistic reasoning, quantitative risk assessment, and other weighted-model-counting applications can rely on fast floating-point evaluation with a rigorous precision certificate, instead of either accepting unknown error or paying the high cost of exact rational arithmetic.","feed_headline":"Floating-point counts now carry a precision guarantee","feed_subtitle":"Rounding error in weighted model counting grows only with log n, so doubles give ~8 digits even for 10^7 variables.","key_machinery":"The central object is arithmetic evaluation of a decision-DNNF formula: replace each literal by its weight, conjunctions by multiplication, and disjunctions by addition. The proof's load-bearing device is an induction (Lemma 1) showing that for nonnegative values, a multiplication propagates the sum of the argument error bounds plus two units of rounding error, while an addition propagates the maximum of its arguments' bounds plus one unit. Because decision-DNNF disjunctions have the form (x ∧ φ1) ∨ (¬x ∧ φ2), the addition depth is bounded by n, and because all conjunctions are decomposable, the multiplication error bound is controlled; the product-of-errors term is absorbed by the n ≤ 1/(2√","core_discovery":"The paper's main result is a tight error bound for the arithmetic evaluation of decision-DNNF formulas when all literal weights are nonnegative. Using floating-point arithmetic with a p-bit fraction, the relative error of the computed weighted model count is at most (4n−2)ε for the main evaluation and slightly smaller for the rescaling product, where ε=$2^{{−p}}$ and n is the number of variables; the decimal precision is therefore at least p log10 2 − log10 n − c, with c = log10 7 when rescaling is required and log10 4 otherwise, provided n ≤ 1/(2√ε) (equivalently, log2 n ≤ p/2 − 1). The theorem converts to concrete guarantees: IEEE double or ERD gives at least 8.11 decimal digits for n ≤ $10^{7}$,","pith_inferences":["Because the bound depends only on decision-DNNF structure and the formula's variable count, the same guarantee should transfer to any representation that compiles to smooth decision-DNNF with at most linear size expansion, such as ordered and free binary decision diagrams; this is our inference, not tested by the paper's experiments.","The paper's experiments show that actual precision usually exceeds the worst-case bound by several digits; replacing the all-roundings-same-direction worst case with a stochastic model of rounding could yield tighter typical-case bounds, an extension the author does not pursue.","The worst-case cancellation family τ_n shows that for mixed-sign weights, no finite precision suffices in general; an interesting testable extension would be to characterize which d-DNNF formulas and weight families admit a polynomial-in-n precision bound, capturing whatever property separates the easy Uniform± cases from the hard Limits± cases.","Since the guarantee holds for billions of operations without degrading, the combination of ERD plus Theorem 1 could be used as a drop-in replacement for double-precision code in existing weighted model counters, preserving their speed while turning silent underflow/overflow failures into a quantified precision certificate."],"forward_implications":["For nonnegative weights, floating-point evaluation of decision-DNNF formulas can be trusted without cross-checking: double/ERD guarantees about 8.11 decimal digits on formulas with up to 10^7 variables, no matter how many operations are performed.","To achieve a target precision D, one chooses the MPF fraction size from p ≥ 2(1 + log2 n) and p ≥ D·log2 10 + log2 n + 2.9; for D = 30 and n = 10^7, MPF-128 suffices.","ERD removes the underflow/overflow failures of plain IEEE double at about 7% time overhead, so the range problem in weighted model counting can be solved without abandoning hardware double arithmetic.","For mixed-sign weights, a hybrid strategy—MPF for nonnegative cases, then MPFI-128, MPFI-256, and finally rational arithmetic—achieved the target precision D = 30 on all 2500 test instances in 13.1 hours, compared with 95.2 hours for rational-only evaluation; it also solved 100 instances that rational arithmetic could not complete.","The bound is independent of weight values and of the number of arithmetic operations, so applications such as probabilistic inference over probabilities in [0,1] inherit the guarantee automatically."],"supporting_citations":[{"why":"Wilkinson's 1960 floating-point error analysis supplies the per-operation rounding bounds that the induction chains together.","marker":"[52]"},{"why":"Wilkinson's book-length treatment of rounding errors underpins the relative-error accounting used in Lemmas 1 and 2.","marker":"[53]"},{"why":"Higham's summation accuracy analysis justifies the addition rule (max of argument bounds plus one unit of rounding).","marker":"[26]"},{"why":"The Handbook of Floating-Point Arithmetic provides the ε=2^{-p} rounding model and interval-arithmetic foundations the proofs assume.","marker":"[37]"},{"why":"Darwiche and Marquis's knowledge compilation map defines decomposability and determinism, the structural properties the error bound relies on.","marker":"[14]"},{"why":"Huang and Darwiche define decision-DNNF, the formula class whose bounded addition depth makes the n-dependent bound possible.","marker":"[27]"},{"why":"The D4 compiler generates the decision-DNNF formulas used in all experimental evaluations of the precision guarantee.","marker":"[32]"},{"why":"The MPFI interval library supplies the guaranteed interval arithmetic used for the mixed-weight hybrid strategy.","marker":"[40]"},{"why":"The GNU MP library provides the MPF and MPQ arithmetic used both for high-precision floating-point evaluation and for exact rational ground truth in the experiments.","marker":"[21]"}],"fun_headline_variants":["Weighted model counts now have a precision proof","Floating-point error in counting, tightly bounded","ERD doubles: count larger, trust the result","Precision guarantee for weighted model counting","Model counting without numeric surprises"],"cache_read_input_tokens":2816,"weakest_assumption_plain":"The bound holds only under the paper's Section 3 assumption that every floating-point computation avoids underflow and overflow, and the proof applies only to decision-DNNF formulas, although the abstract's nonnegative-weight claim is stated more broadly; plain IEEE double failed on 628 of 1000 random instances because the assumption was violated.","fun_headline_variants_meta":{"raw":{"variants":["Weighted model counts now have a precision proof","Floating-point error in counting, tightly bounded","ERD doubles: count larger, trust the result","Precision guarantee for weighted model counting","Model counting without numeric surprises"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000445,"raw_usage":{"total_tokens":2130,"prompt_tokens":830,"completion_tokens":1300,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":574,"completion_tokens_details":{"reasoning_tokens":1233}},"tokens_in":574,"tokens_out":1300,"duration_ms":14976,"temperature":1.0,"reasoning_tokens":1233,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T22:52:09.772530+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Evaluate a smooth decision-DNNF formula over n variables (with n ≤ $2^{{p/2−1}}$) using all literal weights equal to a value slightly greater than 1, a p-bit floating-point format, and directed rounding so every operation rounds upward. The theorem predicts the relative error of the computed count versus an exact rational computation is at most (4n−2)·$2^{{−p}}$; any observed relative error exceeding this bound would refute Theorem 1.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Wilkinson's 1960 floating-point error analysis supplies the per-operation rounding bounds that the induction chains together."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Wilkinson's book-length treatment of rounding errors underpins the relative-error accounting used in Lemmas 1 and 2."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Higham's summation accuracy analysis justifies the addition rule (max of argument bounds plus one unit of rounding)."},{"cited_title":"Handbook of Floating-Point Arithmetic, Second Edition","cited_arxiv_id":null,"evidence_quote":"The Handbook of Floating-Point Arithmetic provides the ε=2^{-p} rounding model and interval-arithmetic foundations the proofs assume."},{"cited_title":"A knowledge compilation map","cited_arxiv_id":null,"evidence_quote":"Darwiche and Marquis's knowledge compilation map defines decomposability and determinism, the structural properties the error bound relies on."},{"cited_title":"The language of search","cited_arxiv_id":null,"evidence_quote":"Huang and Darwiche define decision-DNNF, the formula class whose bounded addition depth makes the n-dependent bound possible."},{"cited_title":"An improved decision-DNNF compiler","cited_arxiv_id":null,"evidence_quote":"The D4 compiler generates the decision-DNNF formulas used in all experimental evaluations of the precision guarantee."},{"cited_title":"Motivations for an arbitrary precision interval arithmetic and the MPFI library","cited_arxiv_id":null,"evidence_quote":"The MPFI interval library supplies the guaranteed interval arithmetic used for the mixed-weight hybrid strategy."},{"cited_title":"GNU MP 6.0 Multiple Precision Arithmetic Library","cited_arxiv_id":null,"evidence_quote":"The GNU MP library provides the MPF and MPQ arithmetic used both for high-precision floating-point evaluation and for exact rational ground truth in the experiments."}],"review_version":1}