Pith. sign in

REVIEW 2 major objections 4 minor 55 references

Numerical Considerations in Weighted Model Counting

T0 review · 2 major / 4 minor · reviewed 2026-08-05 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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}

desk verdict Real precision bound for WMC with honest experiments; abstract oversells scope but core math holds. read the letter →

arxiv 2508.06264 v1 pith:HCRUAMNB submitted 2025-08-08 math.NA cs.AIcs.LOcs.NA

Randal E. Bryant This is my paper · ORCID
classification math.NAcs.AIcs.LOcs.NA MSC 65G5065G30
keywords weightedmodelcountingfloating-pointarithmeticroundingerrordecision-DNNFintervalextended-rangedoublerationalprecisionguarantee
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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√

What would settle it

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.

Watch

Extended reading notes

Core claim

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}$,

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

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.

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 (2)
  1. [§4.4] 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.
  2. [§3, §7, Table 1] 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
minor comments (4)
  1. [Abstract] 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.
  2. [§4.3] 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.
  3. [Typos] 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.
  4. [§4.3, Table 1] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

Theorem 1 is proved from first principles; no fitted parameter or self-citation is used as the derivation's input.

full rationale

The central derivation chain is self-contained. Theorem 1 (Eq. 8) is obtained from Lemmas 1–2, whose induction proofs start from the definition of floating-point rounding (δ[Rnd(v),v] ≤ ε) and from the structure of decision-DNNF formulas: decomposable conjunctions bound multiplication error, and decision disjunctions bound addition depth. No constant in (4n−2)ε or (3n−2)ε is fitted to data, and no step assumes the theorem's conclusion. The precision bounds in Table 1 are algebraically derived from p and n. Experimental validation uses external MC2024 benchmarks and exact MPQ ground truth, so it tests the theorem rather than supplying an ingredient of it. The only self-citation, [7] (Bryant 1986), is background for OBDDs and is not load-bearing for any theorem. The paper's explicit caveat—'We assume for the remainder of this paper that all floating-point computations can be performed without underflow or overflow'—limits the theorem's practical scope: plain IEEE Double fails on 628/1000 random and 45/100 original instances in the paper's own data, and ERD's range extension is described operationally rather than given its own rounding-error theorem. These are scope/correctness limitations, not circularity: they do not make any conclusion equivalent to its input. Similarly, the abstract's nonnegative-weight statement omits the decision-DNNF restriction, an overstatement of scope but not a circular step. No pattern from the list is present: no self-definitional ratio, no fitted input renamed as prediction, no load-bearing self-citation, no imported uniqueness, no ansatz smuggled via citation, and no renaming of a known result as new organization. The derivation is therefore not circular.

Assumptions & free parameters 0 free parameters · 5 assumptions · 1 invented entities

The ledger is light: Theorem 1 is a parameter-free derivation under standard rounding and range assumptions. ERD is the only new construct, and it is an engineering representation rather than a physical entity.

assumptions (5)
  • domain assumption Arithmetic evaluation of a d-DNNF formula computes the weighted model count when weights satisfy the sum-to-one, smoothness, or rescaling conditions stated in Section 2.
    Section 2 lists the three evaluation methods; this is prior knowledge-compilation theory the paper builds on.
  • standard math Each floating-point operation is correctly rounded with relative error at most epsilon = 2^-p, and no underflow or overflow occurs.
    Section 3 and Lemmas 1-2 rely on this model; the no-overflow/no-underflow clause is explicitly assumed for the rest of the paper.
  • domain assumption GMP MPQ/MPF and MPFI libraries are correctly implemented, so rational arithmetic is exact and interval arithmetic returns intervals guaranteed to contain the true values.
    Sections 4.5, 5.2, and 6 use these libraries for ground truth and certified intervals; correctness of the hybrid depends on them.
  • domain assumption The formula class is decision-DNNF, or has a computable structural error bound e(psi) as in Section 4.4.
    Theorem 1 is proved only for decision-DNNF; Section 4.4 extends to other circuits via a structural bound that is asserted, not proved in detail.
  • domain assumption D4 compiles the MC2024 benchmarks to decision-DNNF within the stated limits, making the experimental collection valid for testing the bound.
    Section 4.5; experimental conclusions are scoped to the 100 formulas successfully compiled.
invented entities (1)
  • Extended-Range Double (ERD)
    purpose: Extend IEEE double with a 64-bit signed exponent to avoid underflow and overflow in weighted model counting.
    Introduced in Section 7 as a software representation; no external falsifiable prediction, only claimed performance within the paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Numerical Considerations in Weighted Model Counting." pith.science (2026). https://pith.science/paper/HCRUAMNB

@misc{pith2026250806264,
  author       = {Pith},
  title        = {Pith review of: Numerical Considerations in Weighted Model Counting},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HCRUAMNB}},
  note         = {Machine review of arXiv:2508.06264}
}
read the original abstract

Weighted model counting computes the sum of the rational-valued weights associated with the satisfying assignments for a Boolean formula, where the weight of an assignment is given by the product of the weights assigned to the positive and negated variables comprising the assignment. Weighted model counting finds applications across a variety of domains including probabilistic reasoning and quantitative risk assessment. Most weighted model counting programs operate by (explicitly or implicitly) converting the input formula into a form that enables arithmetic evaluation, using multiplication for conjunctions and addition for disjunctions. Performing this evaluation using floating-point arithmetic can yield inaccurate results, and it cannot quantify the level of precision achieved. Computing with rational arithmetic gives exact results, but it is costly in both time and space. This paper describes how to combine multiple numeric representations to efficiently compute weighted model counts that are guaranteed to achieve a user-specified precision. When all weights are nonnegative, we prove that the precision loss of arithmetic evaluation using floating-point arithmetic can be tightly bounded. We show that supplementing a standard IEEE double-precision representation with a separate 64-bit exponent, a format we call extended-range double (ERD), avoids the underflow and overflow issues commonly encountered in weighted model counting. For problems with mixed negative and positive weights, we show that a combination of interval floating-point arithmetic and rational arithmetic can achieve the twin goals of efficiency and guaranteed precision. For our evaluations, we have devised especially challenging formulas and weight assignments, demonstrating the robustness of our approach.

Figures

Figures reproduced from arXiv: 2508.06264 by the authors.

Figure 1
Figure 1. Decimal Precision Achieved by MPF-128 for Benchmarks with Nonnegative Weights. [PITH_FULL_IMAGE:figures/full_fig_p011_1.png] view at source ↗
Figure 2
Figure 2. Percent of instances (top) and average evaluation time (bottom) to achieve target [PITH_FULL_IMAGE:figures/full_fig_p013_2.png] view at source ↗
Figure 3
Figure 3. Decimal Precision Achieved by MPF-128 for Benchmarks with Mixed Weights. There [PITH_FULL_IMAGE:figures/full_fig_p015_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Predictive Accuracy of MPFI-128 Interval Arithmetic. MPFI never has a higher [PITH_FULL_IMAGE:figures/full_fig_p016_4.png]
Figure 5
Figure 5. Figure 5: Percent of instances (top) and average evaluation time (bottom) to achieve target [PITH_FULL_IMAGE:figures/full_fig_p018_5.png]
Figure 6
Figure 6. Figure 6: Runtime for hybrid method vs. for MPQ, categorized by the solution method. Success [PITH_FULL_IMAGE:figures/full_fig_p020_6.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

55 extracted references · 55 canonical work pages

  1. [1]

    Interactive cost configuration over decision diagrmas

    Henrik Reif Andersen, Tarik Hadzic, and David Pisinger. Interactive cost configuration over decision diagrmas. Journal of Artificial Intelligence Research , 37:99–139, 2010

    work page 2010

  2. [2]

    Andrews and Sarah J

    John D. Andrews and Sarah J. Dunnett. Event-tree analysis using binary decision diagrams. IEEE Transactions on Reliability Analysis , 49(2):230–238, June 2000

    work page 2000

  3. [3]

    Lower bounds for exact model counting and applications in probabilistic databases

    Paul Beame, Jerry Li, Sudeepa Roy, and Dan Suciu. Lower bounds for exact model counting and applications in probabilistic databases. In Uncertainty in Artificial Intelligence , 2013

    work page 2013

  4. [4]

    A verified certificate checker for finite-precision error bounds in Coq and HOL4

    Heiko Becker et al. A verified certificate checker for finite-precision error bounds in Coq and HOL4. In Formal Methods in Computer-Aided Design (FMCAD) , 2016

    work page 2016

  5. [5]

    Automated analysis of feature models 20 years later: A literature review

    David Benavides, Sergio Segura, and Antonio Ruiz-Cort´ es. Automated analysis of feature models 20 years later: A literature review. Information Systems , 35:615–636, 2010

    work page 2010

  6. [6]

    Cire, Willem-Jan van Hoeve, and John Hooker

    David Bergman, Andre A. Cire, Willem-Jan van Hoeve, and John Hooker. Decision Diagrams for Optimization. Springer, 2016

    work page 2016

  7. [7]

    Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Trans. Computers, 35(8):677–691, 1986

    work page 1986

  8. [8]

    On probabilistic inference by weighted model counting

    Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artificial Intelligence, 172:772–799, 2008

    work page 2008

Show all 55 references
  1. [9]

    Decomposable negation normal form

    Adnan Darwiche. Decomposable negation normal form. Journal of the ACM , 48(4):608–647, 2001

    2001

  2. [10]

    On the tractable counting of theory models and its application to truth main- tenance and belief revision

    Adnan Darwiche. On the tractable counting of theory models and its application to truth main- tenance and belief revision. Journal of Applications of Non Classical Logics , 11(1-2):11–34, 2001

    2001

  3. [11]

    A compiler for deterministic, decomposable negation normal form

    Adnan Darwiche. A compiler for deterministic, decomposable negation normal form. InAssociation for the Advancement of Artificial Intelligence , 2002

    2002

  4. [12]

    New advances in compiling CNF to decomposable negation normal form

    Adnan Darwiche. New advances in compiling CNF to decomposable negation normal form. In European Conference on Artificial Intelligence , pages 328–332, 2004

    2004

  5. [13]

    SDD: A new canonical representation of propositional knowledge bases

    Adnan Darwiche. SDD: A new canonical representation of propositional knowledge bases. In International Joint Conference on Artificial Intelligence (IJCAI) , pages 819–826, 2011

    2011

  6. [14]

    A knowledge compilation map

    Adnan Darwiche and Pierre Marquis. A knowledge compilation map. Journal of Artificial Intel- ligence Research, 17, 2002

    2002

  7. [15]

    Probabilistic planning via heuristic forward search and weighted model counting

    Carmel Domshlak and J¨ org Hoffman. Probabilistic planning via heuristic forward search and weighted model counting. Journal of Artificial Intelligence Research , 30:565–620, 2007

    2007

  8. [16]

    Anytime weighted model counting with approximation guarantees for probabilistic inference

    Alexandre Dubray, Pierre Schaus, and Siegfried Nijssen. Anytime weighted model counting with approximation guarantees for probabilistic inference. In Principles and Practice of Constraint Programming (CP), 2024

    2024

  9. [17]

    Dudek, Vu H

    Jeffrey M. Dudek, Vu H. N. Phan, and Moshe Y. Vardi. ADDMC: Weighted model counting with algebraic decision diagrams. In AAAI Conference on Artificial Intelligence , pages 1468–1475, 2020

    2020

  10. [18]

    Dudek, Vu H

    Jeffrey M. Dudek, Vu H. N. Phan, and Moshe Y. Vardi. ProCount: Weighted projected model counting with graded project-join trees. In Theory and Applications of Satisfiability Testing (SAT), volume 12831 of LNCS, pages 152–170, 2021

    2021

  11. [19]

    Fichte, Markus Hecher, and Florim Hamiti

    Johannes K. Fichte, Markus Hecher, and Florim Hamiti. The model counting competition 2020. Journal of Experimental Algorithmics , 26(1), 2021

    2020

  12. [20]

    Gomes, Ashish Sabharwal, and Bart Selman

    Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Model counting. In Handbook of Satisfia- bility, pages 633–654. IOS Press, 2009

    2009

  13. [21]

    GNU MP 6.0 Multiple Precision Arithmetic Library

    Torbjrn Granlund. GNU MP 6.0 Multiple Precision Arithmetic Library . Samurai Media, Ltd, 2015

    2015

  14. [22]

    Groen, Carol Smidts, and Ali Mosleh

    Frank J. Groen, Carol Smidts, and Ali Mosleh. QRAS—the quantitative risk assessment system. Reliability Engineering and System Safety , 91(3):292–304, March 2006

    2006

  15. [23]

    K-terminal network reliablity measures with 23 Numerical Considerations in Weighted Model Counting R

    Gary Hardy, Corinne Lucet, and Nikolaos Limnios. K-terminal network reliablity measures with 23 Numerical Considerations in Weighted Model Counting R. E. Bryant binary decision diagrams. IEEE Transactions on Reliability , 56(3):506–515, 2007

    2007

  16. [24]

    The results of the model counting competition, 2024

    Markus Hecher, Johannes Fichte, and Arijit Shaw. The results of the model counting competition, 2024

    2024

  17. [25]

    Hickey, Qun Ju, and Maarten H

    Timothy J. Hickey, Qun Ju, and Maarten H. van Emden. Interval arithmetic: From principles to implementation. J.ACM, 48(5):1038–1068, 2001

    2001

  18. [26]

    Nicholas J. Higham. The accuracy of floating-point summation. SIAM Journal on Scientific Computing, 14(4), 1993

    1993

  19. [27]

    The language of search

    Jinbo Huang and Adnan Darwiche. The language of search. Journal of Artificial Intelligence Research, 22:191–219, 2007

    2007

  20. [28]

    R. S. Jones. The C Programmer’s Companion ANSI C Library Functions . Silicon Press, 1991

    1991

  21. [29]

    Donald E. Knuth. The Art of Computer Programming, Volume 2: Seminumerical Algorithms, Second Edition, chapter 4.5 Rational Arithmetic. Addison-Wesley, 1981

    1981

  22. [30]

    Donald E. Knuth. The Art of Computer Programming, Volume 2: Seminumerical Algorithms, Second Edition, chapter 4.2 Floating-Point Arithmetic. Addison-Wesley, 1981

    1981

  23. [31]

    Donald E. Knuth. The Art of Computer Programming, Volume 4A: Combinatorial Algorithms, Part I , chapter 7.1.4 Binary Decision Diagrams. Pearson, 2011

    2011

  24. [32]

    An improved decision-DNNF compiler

    Jean-Marie Lagniez and Pierre Marquis. An improved decision-DNNF compiler. In International Joint Conference on Artificial Intelligence (IJCAI) , pages 667–673, 2017

    2017

  25. [33]

    Certified roundoff error bounds using semidefinite programming

    Victor Magron, George Constantinides, and Alastair Donaldson. Certified roundoff error bounds using semidefinite programming. ACM Transactions on Mathematical Software, 43(4):1–31, 2017

    2017

  26. [34]

    Zero-suppressed BDDs and their applications

    Shin-ichi Minato. Zero-suppressed BDDs and their applications. Software Tools for Technology Transfer, 3:156–170, 2001

    2001

  27. [35]

    Compiling Bayesian networks by symbolic proba- bility calculation based on zero-suppressed BDDs

    Shin-ichi Minato, Ken Satoh, and Taisuke Sato. Compiling Bayesian networks by symbolic proba- bility calculation based on zero-suppressed BDDs. In International Joint Conference on Artificial Intelligence (IJCAI) , 2007

    2007

  28. [36]

    McIlraith, J

    Christian Muise, Sheila A. McIlraith, J. Christopher Beck, and Eric Hsu. DSHARP: Fast d-DNNF compilation with sharpSAT. In Canadian Conference on Artificial Intelligence , volume 7310 of LNCS, pages 356–361, 2012

    2012

  29. [37]

    Handbook of Floating-Point Arithmetic, Second Edition

    Jean-Michel Muller et al. Handbook of Floating-Point Arithmetic, Second Edition . Birkh¨ auser, 2018

    2018

  30. [38]

    Michael L. Overton. Numerical Computing with IEEE Floating Point Arithmetic . SIAM, 2001

    2001

  31. [39]

    On compiling CNF into decision-DNNF

    Umut Oztok and Adnan Darwiche. On compiling CNF into decision-DNNF. In Constraint Pro- gramming (CP), volume 8656 of LNCS, pages 42–57, 2014

    2014

  32. [40]

    Motivations for an arbitrary precision interval arithmetic and the MPFI library

    Nathali Revol and Fabrice Rouillier. Motivations for an arbitrary precision interval arithmetic and the MPFI library. Reliable Computing, 11(4):275–290, 2005

    2005

  33. [41]

    Rump, Florian B¨ unger, and Claude-Pierre Jeannerod

    Siegfried M. Rump, Florian B¨ unger, and Claude-Pierre Jeannerod. Improved error bounds for floating-point products and Horner’s scheme. BIT Numerical Mathematics , 56:293–307, 2015

    2015

  34. [42]

    Performing Bayesian inference by weighted model counting

    Tian Sang, Paul Beame, and Henry Kautz. Performing Bayesian inference by weighted model counting. In AAAI Conference on Artificial Intelligence , pages 475–482, 2005

    2005

  35. [43]

    Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. GANAK: A scalable proba- bilistic exact model counter. In International Joint Conference on Artificial Intelligence (IJCAI) , pages 1169–1176, 2019

    2019

  36. [44]

    Arjit Shaw and Kuldeep S. Meel. Model counting in the wild. In Principles of Knowledge Repre- sentation and Reasoning , 2024

    2024

  37. [45]

    Smoothing structured decomposable circuits

    Andy Shih, Guy Van den Broeck, Paul Beame, and Antoine Amarilli. Smoothing structured decomposable circuits. In Neural Information Processing Systems (NeurIPS) , 2019

    2019

  38. [46]

    Baranowski, Ian Briggs, Charles Jacobsen, Zvonimir Rakamari´ c, and Ganesh Gopalakrishnan

    Alexey Solovyev, Marek S. Baranowski, Ian Briggs, Charles Jacobsen, Zvonimir Rakamari´ c, and Ganesh Gopalakrishnan. Rigorous estimation of floating-point round-off errors with symbolic 24 Numerical Considerations in Weighted Model Counting R. E. Bryant Taylor expansion. ACM T...

    2018

  39. [47]

    Ham, Sharad Malik, and Robert K

    Arvind Srinivasan, T. Ham, Sharad Malik, and Robert K. Brayton. Algorithms for discrete function manipulation. In International Conference on Computer-Aided Design (ICCAD) , pages 92–95, 1990

    1990

  40. [48]

    Young, Thomas Th¨ um, and Ina Schaefer

    Chico Sundermann, Tobias Heß, Michael Nieke, Paul Maximilian Bittner, Jeffrey M. Young, Thomas Th¨ um, and Ina Schaefer. Evaluating state-of-the-art #SAT solvers on industrial con- figuration spaces. Empirical Software Engineering, 28, January 2023

    2023

  41. [49]

    Reusing d-DNNFs for efficient feature-model counting

    Chico Sundermann, Heiko Raab, Tobias Heß, Thomas Th¨ um, and Ina Schaefer. Reusing d-DNNFs for efficient feature-model counting. ACM Transactions on Software Engineering and Methodology, 33(8), 2024

    2024

  42. [50]

    Leslie G. Valiant. The complexity of enumeration and reliability problems. SIAM Journal of Computing, 8(3):410–421, 1979

    1979

  43. [51]

    Branching Programs and Binary Decision Diagrams: Theory and Applications

    Ingo Wegener. Branching Programs and Binary Decision Diagrams: Theory and Applications . SIAM, 2000

    2000

  44. [52]

    James. H. Wilkinson. Error analysis of floating-point computation. Numerische Mathematik , 2:319–340, 1960

    1960

  45. [53]

    James. H. Wilkinson. Rounding Errors in Algebraic Processes. Prentice Hall, 1964

    1964

  46. [54]

    A review of decision diagrams in system reliability modeling and analysis

    Liudong Xing. A review of decision diagrams in system reliability modeling and analysis. Applied Mathematical Modeling, 2025

    2025

  47. [55]

    Liudong Xing and Suprasad V. Amari. Binary Decision Diagrams and Extensions for System Reliability Analysis. Wiley, 2015. 25

    2015

Pith tools

Reviewed August 5, 2026 · model on record in the stance chip above.