Numerical Considerations in Weighted Model Counting

• URL: http://arxiv.org/abs/2508.06264v1
• Date: Fri, 08 Aug 2025 12:28:49 GMT
• Title: Numerical Considerations in Weighted Model Counting
• Abstract summary: We show how to combine multiple numeric representations to efficiently compute weighted model counts that are guaranteed to achieve a user-specified precision.<n>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.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• DEL: Digit Entropy Loss for Numerical Learning of Large Language Models [63.37357414497361]
  Number prediction is a fundamental capability of large language models (LLMs) in mathematical problem-solving and code generation.<n>We present Digit Entropy Loss (DEL) for auto-regressive numerical learning.<n>Our formulation can incorporate integers, decimals, and decimal points, expanding the learning objective from a single digit to the floating-point number domain.
  arXiv  Detail & Related papers  (2026-05-19T18:18:59Z)
• Multiplication in Multimodal LLMs: Computation with Text, Image, and Audio Inputs [0.8129517423858409]
  Multimodal LLMs can accurately perceive numerical content across modalities yet fail to perform exact multi-digit multiplication.<n>We introduce a controlled multimodal multiplication benchmark that factorially varies digit length, digit sparsity, representation.<n>We also define arithmetic load, C, as the product of the total and non-zero digit count.
  arXiv  Detail & Related papers  (2026-04-20T12:52:07Z)
• Evaluating Numerical Accuracy in Mixed-Precision Computing by Dual-Delta Testing [0.7106986689736828]
  When implementing custom mixed-precision functions, it is critical to verify their numerical accuracy.<n>Traditional approaches typically compare the custom implementation against a reference using a single error metric.<n>This paper introduces textitDual-Delta Testing, a systematic methodology that evaluates two error distributions against a high-precision oracle.
  arXiv  Detail & Related papers  (2026-02-11T07:54:04Z)
• Fisher Random Walk: Automatic Debiasing Contextual Preference Inference for Large Language Model Evaluation [46.643610591694376]
  We develop a semiparametric efficient estimator that automates the debiased estimation.<n>We show that the efficiency is achieved when the weights are derived from a novel strategy called Fisher random walk.
  arXiv  Detail & Related papers  (2025-09-06T22:29:17Z)
• Semiparametric conformal prediction [79.6147286161434]
  We construct a conformal prediction set accounting for the joint correlation structure of the vector-valued non-conformity scores.<n>We flexibly estimate the joint cumulative distribution function (CDF) of the scores.<n>Our method yields desired coverage and competitive efficiency on a range of real-world regression problems.
  arXiv  Detail & Related papers  (2024-11-04T14:29:02Z)
• How Numerical Precision Affects Arithmetical Reasoning Capabilities of LLMs [69.55103380185612]
  We identify numerical precision as a key factor that influences Transformer-based large language models' arithmetic performances.<n>Our results show that Transformers operating with low numerical precision fail to address arithmetic tasks, such as iterated addition and integer multiplication.<n>In contrast, Transformers with standard numerical precision can efficiently handle these tasks with significantly smaller model sizes.
  arXiv  Detail & Related papers  (2024-10-17T17:59:35Z)
• A Fourier Approach to the Parameter Estimation Problem for One-dimensional Gaussian Mixture Models [21.436254507839738]
  We propose a novel algorithm for estimating parameters in one-dimensional Gaussian mixture models. We show that our algorithm achieves better scores in likelihood, AIC, and BIC when compared to the EM algorithm.
  arXiv  Detail & Related papers  (2024-04-19T03:53:50Z)
• Fast Shapley Value Estimation: A Unified Approach [71.92014859992263]
  We propose a straightforward and efficient Shapley estimator, SimSHAP, by eliminating redundant techniques. In our analysis of existing approaches, we observe that estimators can be unified as a linear transformation of randomly summed values from feature subsets. Our experiments validate the effectiveness of our SimSHAP, which significantly accelerates the computation of accurate Shapley values.
  arXiv  Detail & Related papers  (2023-11-02T06:09:24Z)
• Efficient Computation of Counterfactual Bounds [44.4263314637532]
  We compute exact counterfactual bounds via algorithms for credal nets on a subclass of structural causal models. We evaluate their accuracy by providing credible intervals on the quality of the approximation.
  arXiv  Detail & Related papers  (2023-07-17T07:59:47Z)
• Learning Unnormalized Statistical Models via Compositional Optimization [73.30514599338407]
  Noise-contrastive estimation(NCE) has been proposed by formulating the objective as the logistic loss of the real data and the artificial noise. In this paper, we study it a direct approach for optimizing the negative log-likelihood of unnormalized models.
  arXiv  Detail & Related papers  (2023-06-13T01:18:16Z)
• An Efficient Summation Algorithm for the Accuracy, Convergence and Reproducibility of Parallel Numerical Methods [0.0]
  We have introduced a new parallel algorithm for summing a sequence of floating-point numbers. This algorithm which scales up easily with the number of processors, adds numbers of the same exponents first. In this article, our main contribution is an extensive analysis of its efficiency with respect to several properties.
  arXiv  Detail & Related papers  (2022-05-11T08:31:48Z)
• Fixed-point iterations for several dissimilarity measure barycenters in the Gaussian case [69.9674326582747]
  In target tracking and sensor fusion contexts it is not unusual to deal with a large number of Gaussian densities. Fixed-Point Iterations (FPI) are presented for the computation of barycenters according to several dissimilarity measures.
  arXiv  Detail & Related papers  (2022-05-10T11:12:12Z)
• Integer-arithmetic-only Certified Robustness for Quantized Neural Networks [14.737638416823772]
  A line of work on tackling adversarial examples is certified robustness via randomized smoothing. Such a mechanism usually uses floating-point arithmetic for calculations in inference. We show our approach can obtain a comparable accuracy and 4x5x speedup over floating-point arithmetic certified robust methods.
  arXiv  Detail & Related papers  (2021-08-21T01:15:19Z)
• Berrut Approximated Coded Computing: Straggler Resistance Beyond Polynomial Computing [34.69732430310801]
  We propose Berrut Approximated Coded Computing (BACC) as an alternative approach to deal with stragglers effect. BACC is proven to be numerically stable with low computational complexity. In particular, BACC is used to train a deep neural network on a cluster of servers.
  arXiv  Detail & Related papers  (2020-09-17T14:23:38Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.