CSB: A Counting and Sampling tool for Bit-vectors

• URL: http://arxiv.org/abs/2607.04142v1
• Date: Sun, 05 Jul 2026 07:02:03 GMT
• Title: CSB: A Counting and Sampling tool for Bit-vectors
• Abstract summary: Satisfiability modulo theory (SMT) solvers have significantly advanced automated reasoning.<n>Can we rely on modern CNF model counters and CNF samplers to extend modern SMT solvers to handle the problems of counting and sampling over bit-vectors?
• Score: 29.586350637820846
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Satisfiability modulo theory (SMT) solvers have significantly advanced automated reasoning due to their effectiveness in solving problems across various fields. With the advancement in SMT solvers, there is growing interest in exploring capabilities beyond mere satisfiability, similar to the progression observed in Boolean satisfiability solvers that expanded into counting and sampling. In this study, we investigate the following question: Can we rely on modern CNF model counters and CNF samplers to extend modern SMT solvers to handle the problems of counting and sampling over bit-vectors? The main contribution of this work is the development of an efficient and user-friendly tool, csb, that solves a bunch of problems around model counting and sampling on the theory of bit-vectors, namely exact and approximate projected and non-projected model counting, along with the almost-uniform and uniform-like sampling. In the case of exact counting, projected counting, and uniform sampling. Our tool csb converts the bit-vector formula into a CNF formula using bit-blasting techniques before applying CNF model counters or samplers to perform counting or sampling. Our experiments demonstrate significant performance improvements over existing methods.

Related papers

• Fast Gibbs Sampling on Bayesian Hidden Markov Model with Missing Observations [0.30586855806896046]
  The Hidden Markov Model (MM) is a widely-used statistical model for handling sequential data.<n>missing observations in real-world datasets often show up in numerical simulations and real data.<n>We propose an algorithm that estimates both the number of missing entries and the time complexity of a lot.<n>The proposed algorithm produces a larger Effective Sample Size (ESS) per summary, which can be justified theoretically and theoretically.
  arXiv  Detail & Related papers  (2026-01-04T09:10:43Z)
• Reasoning with Sampling: Your Base Model is Smarter Than You Think [52.639108524651846]
  We propose a simple iterative sampling algorithm leveraging the base models' own likelihoods.<n>We show that our algorithm offers substantial boosts in reasoning that nearly match and even outperform those from RL.<n>Our method does not require training, curated datasets, or a verifier.
  arXiv  Detail & Related papers  (2025-10-16T17:18:11Z)
• Text Generation Beyond Discrete Token Sampling [74.06071135207635]
  Mixture of Inputs (MoI) is a training-free method for autoregressive generation.<n>MoI consistently improves performance across multiple models including QwQ-32B, Nemotron-Super-49B, Gemma-3-27B, and DAPO-Qwen-32B.
  arXiv  Detail & Related papers  (2025-05-20T18:41:46Z)
• Parallel Simulation for Log-concave Sampling and Score-based Diffusion Models [55.07411490538404]
  We propose a novel parallel sampling method that improves adaptive complexity dependence on dimension $d$.<n>Our approach builds on parallel simulation techniques from scientific computing.
  arXiv  Detail & Related papers  (2024-12-10T11:50:46Z)
• Quasi-random Multi-Sample Inference for Large Language Models [1.647759094903376]
  Large language models (LLMs) are often equipped with multi-sample decoding strategies.<n>Traditional text generation methods, such as beam search and sampling-based techniques, have notable limitations.<n>This study explores the potential of arithmetic sampling, contrasting it with ancestral sampling.
  arXiv  Detail & Related papers  (2024-11-09T18:55:04Z)
• Unveiling the Statistical Foundations of Chain-of-Thought Prompting Methods [59.779795063072655]
  Chain-of-Thought (CoT) prompting and its variants have gained popularity as effective methods for solving multi-step reasoning problems. We analyze CoT prompting from a statistical estimation perspective, providing a comprehensive characterization of its sample complexity.
  arXiv  Detail & Related papers  (2024-08-25T04:07:18Z)
• Learning to sample fibers for goodness-of-fit testing [0.0]
  We consider the problem of constructing exact goodness-of-fit tests for discrete exponential family models.<n>We translate the problem into a Markov decision process and demonstrate a reinforcement learning approach for learning good moves' for sampling.<n>Our algorithm is based on an actor-critic sampling scheme, with provable convergence.
  arXiv  Detail & Related papers  (2024-05-22T19:33:58Z)
• Amortizing intractable inference in large language models [56.92471123778389]
  We use amortized Bayesian inference to sample from intractable posterior distributions. We empirically demonstrate that this distribution-matching paradigm of LLM fine-tuning can serve as an effective alternative to maximum-likelihood training. As an important application, we interpret chain-of-thought reasoning as a latent variable modeling problem.
  arXiv  Detail & Related papers  (2023-10-06T16:36:08Z)
• Fast Bayesian Inference with Batch Bayesian Quadrature via Kernel Recombination [23.6031259333814]
  We propose a parallelised (batch) Bayesian quadrature (BQ) method that possesses a provably-exponential convergence rate. We find that our approach significantly outperforms the sampling efficiency of both state-of-the-art BQ techniques and Nested Sampling in various real-world datasets.
  arXiv  Detail & Related papers  (2022-06-09T19:14:52Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  We introduce the CoCoMoT (Computing Conformance Modulo Theories) framework. First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case. Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering.
  arXiv  Detail & Related papers  (2021-03-18T20:22:50Z)

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.