Paper deep dive

CSB: A Counting and Sampling tool for Bit-vectors

Arijit Shaw, Kuldeep S. Meel

Year: 2026Venue: arXiv preprintArea: cs.LOType: PreprintEmbeddings: 45

Intelligence

Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%

Last extracted: 7/7/2026, 11:51:32 AM

Summary

This paper introduces CSB, a high-performance tool for model counting and sampling over quantifier-free bit-vectors (QFBV). CSB extends the STP SMT solver by integrating CNF-based model counters (ApproxMC, Ganak) and samplers (UniGen, CMSGen) via a bit-blasting pipeline that converts bit-vector formulas to CNF. It supports exact, approximate, and projected model counting, as well as almost-uniform and uniform-like sampling, demonstrating significant performance improvements over existing methods.

Entities (10)

csb · software-tool · 98%ApproxMC · model-counter · 95%Bit-blasting · technique · 95%CMSGen · sampler · 95%Ganak · model-counter · 95%STP · smt-solver · 95%UniGen · sampler · 95%Arjun · preprocessor · 90%CNF · data-format · 90%QFBV · logic-theory · 90%

Relation Signals (13)

csb → extends → STP

confidence 95% · We built our tool on top of SMT solver STP

csb → integrates → ApproxMC

confidence 95% · integrating approximate model counter ApproxMC

csb → integrates → Ganak

confidence 95% · exact model counter Ganak

csb → integrates → UniGen

confidence 95% · almost-uniform sampler UniGen

csb → integrates → CMSGen

confidence 95% · uniform-like sampler CMSGen

csb → solves → Projected Model Counting

confidence 95% · addresses six key challenges... exact and approximate projected model counting

csb → solves → Approximate Counting

confidence 95% · exact and approximate model counting

csb → solves → Almost-uniform Sampling

confidence 95% · almost-uniform sampling

csb → solves → Uniform-like Sampling

confidence 95% · uniform-like sampling

csb → solves → Exact Counting

confidence 95% · exact and approximate model counting

Bit-blasting → converts → QFBV

confidence 90% · converts the bit-vector formula into a CNF formula using bit-blasting techniques

csb → integrates → Arjun

confidence 90% · utilize Arjun as a preprocessor

Bit-blasting → produces → CNF

confidence 90% · converts the bit-vector formula into a CNF formula

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

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.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

44,119 characters extracted from source content.

Expand or collapse full text

CSB: A Counting and Sampling tool for Bit-vectors ∗ Arijit Shaw Chennai Mathematical Institute IAI, TCG-CREST, Kolkata Kuldeep S. Meel Georgia Institute of Technology University of Toronto 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,csbis the first tool to solve the problem — although all these problems have a lot of applications. Our toolcsbconverts the bit-vector formula into a CNF formula using bit-blasting techniques before applying CNF model counters or samplers to perform counting or sampling. It keeps track of the variable mapping between the bitvector and CNF formula and passes that information to the CNF counter. We built our tool on top of SMT solverSTPby integrating approximate model counterApproxMC, exact model counterGanak, almost-uniform sampler UniGen, and uniform-like samplerCMSGenin it. Our experiments demonstrate significant performance improvements over existing methods. 1 Introduction The paradigm of Satisfiability Modulo Theory (SMT) solving has been central to advances in hardware and software verification over the past two decades. Over time, the community has developed several scalable state-of-the-art SMT solvers [B + 22,BSST21,B09,CGSS13, NP23]. For many problem instances, satisfiability alone does not suffice, and one is often interested in computations over the solution set. Two such problems are computing an estimate of the cardinality of the solution set and uniformly sampling a solution from the entire solution set. As a starting point, we focus on the case when the underlying formula is expressed inQFBV, or quantifier-free bit-vector arithmetic (referred to as bit-vectors hereafter). Our choice ofQFBV stems from its being one of the first theories to be investigated in the context of SMT solving, as well as recent empirical studies showing the importance of counting problems over bit-vector formulas in domains such as cryptography [BZG20] and software verification [GFB21,TW21]. In many of the problems like [TW21], the underlying problem becomes a projected model counting problem, where we want the count projected on a subset of variables. ∗ This is the authors’ version of the article published in Acta Informatica [SM26]. The corresponding toolcsb is available at https://github.com/meelgroup/csb. 1 arXiv:2607.04142v1 [cs.LO] 5 Jul 2026 The problem of counting and sampling over bit-vectors can be addressed through two methods: (i) reasoning directly over bit-vectors, or (i) reducing the problem to a Boolean formula in conjunctive normal form (CNF). While the former approach has been studied in recent years using lifting techniques for word-level constraints [CDM15,CMMV16,DBS18,DBS19], the latter has not been thoroughly assessed. In this paper, we focus on whether a modern SMT solver can be extended with CNF-based model counters and CNF samplers to efficiently address the problems of counting and sampling over bit-vectors. Our investigation into the design of a counting tool for bit-vector formulas relies on bit-blasting, followed by the use of CNF-based samplers and counters, leveraging the latter’s scalability. Our toolcsb 1 addresses six key challenges in the theory of bitvectors: exact and approximate model counting, exact and approximate projected model counting, uniform-like sampling, and almost-uniform sampling. Prior tocsb, no existing tool supported this full spectrum of func- tionality beyond approximate model counting. To evaluate scalability, we assembled a suite of 661 benchmarks drawn from diverse application domains—such as cryptography and software verification—each encoded as a bit-vector model counting instance. The primary contribution of this paper iscsb, a high-performance bit-vector model counter that extends the SMT solverSTPby integrating off-the-shelf CNF counters. On our 661 benchmarks,csbcomputes exact counts for 640 instances, outperforming the state-of-the-art counterSMTApproxMC, which solves only 111 cases. We further enhancecsbto support both exact and projected model counting, and incorporate CNF-based sampling engines to enable efficient uniform-like and almost-uniform sampling. Experimental results show thatcsbgenerates 500 uniform-like samples in an average of 6.6 s and produces 500 almost-uniform samples in 283.7 s. Organization. The rest of the paper is organized as follows: We introduce the preliminaries and related work in Section 2. In Section 3, we present an overview of our framework,csb. We describe our experimental methodology and results in Section 4. Finally, we conclude in Section 5. 2 Background SMT and bitvectors. A bit-vector is a vector of bits of a given fixed width. LetXbe the set of bit-vector variables, and letFbe a formula in the theory of quantifier-free bit-vectors. Suppose Fhas variablesx 1 ,x 2 ,...,x n , each associated with a fixed widthw 1 ,w 2 ,...,w n . Consequently, each variablex i ranges over a finite domain of cardinality 2 w i . A model (or solution) ofFis an assignment of bit-vector constants to the variables inXsuch thatFevaluates to true. The set of all models ofFis denoted bySol(F). Throughout this paper, we abuse notation by usingF to denote both Boolean and bit-vector formulas interchangeably. Model Counting. The model counting problem is determining|Sol(F)|, where|S|denotes the cardinality of a setS. An exact model counter takes in formulaF, and returns|Sol(F)|. An approximate model counter takes in a formulaF, tolerance parameterε, confidence parameterδ and returnscsuch thatPr |Sol(F )| 1 + ε ≤ c≤ (1 + ε)|Sol(F )| ≥1− δ, wherePr[E] denotes the probability of event E. Projected Model Counting. LetFbe a formula over variablesVars(F), and letα∈0,1 Vars(F) 1 Open source tool available at: https://github.com/meelgroup/csb/ 2 be an assignment. For any projection setS ⊆ Vars(F), we define a projected assignmentαon S α ↓S = (α(x) ) x∈S ∈0,1 S i.e. the projection of the full assignmentαonto the coordinates indexed byS. LetSol(F) ↓S denote the set of projected assignments satisfying the given formula Fand a projection setS. The problem of projected model counting is to compute|Sol(F) ↓S |. An exact projected model counter takes in formulaF, and returns|Sol(F) ↓S |. An approximate projected model counter takes in a formulaF, projection setS, parametersε, andδ, and returns csuch thatPr |Sol(F ) ↓S | 1 + ε ≤ c≤ (1 + ε)|Sol(F ) ↓S | ≥ 1− δ. To differentiate between model counting and projected model counting, we use the term non-projected model counting to refer to model counting without projection. Sampling. An almost uniform samplerGtakes a tolerance parameterεalong withF, and guarantees∀y ∈ Sol(F), 1 (1 + ε)|Sol(F )| ≤ Pr[G(F,ε) =y]≤ (1 + ε) |Sol(F )| . An uniform-like sampler also takes in a Boolean formulaFand returnsσ ∈ Sol(F), and is designed to behave like a uniform sampler, but without theoretical guarantees. Its design is inspired by the distribution- testing tool Barbarik [CM19,GSCM21]. Empirical evaluation on a large benchmark suite shows that distribution-testing tools cannot distinguish its output from that of an almost-uniform sampler, indicating that the uniform-like sampler produces samples from a distribution closely approximating the ideal almost-uniform distribution. Independent Support. For a given assignmentσoverXand a subset of variablesS ⊆ X, letσ ↓S represent the assignment of variables restricted toS. Given a Boolean formulaF over the set of variablesXand a projection setS ⊆ X, a subset of variablesIsuch that I ⊆ Sis called independent support ofSif∀σ 1 ,σ 2 ∈ Sol(F),σ 1↓I =σ 2↓I =⇒ σ 1↓S =σ 2↓S . Several preprocessing techniques for model counting have been proposed, which compute a small independent support for the input formula and simplify the formula based on that support [LLM16, SM19]. Related Work. The success of propositional model counters, especially approximate ones, led to the adaptation of these techniques for word-level constraints.[CDM15] extended hashing-based model counting from the approximate CNF model counterApproxMC[CMV13] to word-level benchmarks using bit-blasting.[CMMV16] developedSMTApproxMC, which lifts hash functions to handle word-level constraints. Kim et al. [KM18,KM20] introduced a system for statistical estimation to continuously refine the probabilistic estimate of model counts, although it lacks (ε,δ)-guarantees [KM18]. In the sampling domain, the need for uniform samplers and those achieving high coverage is well-established. There have been considerable efforts to sample from SMT formulas with high coverage [DBS18,DBS19,PRI23], yet uniform sampling from these formulas remains largely unexplored, representing a significant challenge. The technique of lifting hash functions, as used in [CMMV16], is ineffective for uniform sampling due to the need for 3-wise independence, whereas the lifted hash functions in [CMV16] only ensure 2-wise independence. In the context of CNF counting, there has been a significant improvement in the last two decades. Different model counters have their respective strengths and weaknesses, as seen in recent studies [SM24a] and the model counting competition [FHH21]. 3 3 Approach We developcsb, a model counting and sampling tool for the quantifier-free fragment of the theory of bit-vectors. To achieve this,csbfirst bit-blasts the formula to a Boolean CNF formula, then applies an off-the-shelf CNF model counter or CNF sampler to solve the problems of model counting and sampling, respectively. By reducing the problem to CNF, our toolcsbleverages ongoing improvements in propositional model counting and sampling. Bit-blasting 1. UniGen (Almost-uniform Sampl.) 2. CMSGen (Uniform-like Sampl.) Tools used in each Component CNF Sample Bitvector Sample CNF Sampling CNF Bitvector Formula Model Construction Sampling Framework Bit-blasting CNF Bitvector Formula (F) Counting Framework Tools used in each Component TechMap (STP) 1. ApproxMC (Approximate Counting) 2. Ganak (Exact Counting) Model Count (F) (ω) (F ) bit (F ) bit (ω ) bit (c) TechMap (STP) STP Model Counting Figure 1: The architecture for counting and sampling in csb. 3.1 Model Counting As shown in Figure 1, the model counting part ofcsbcomprises two primary components: (i) a tool for bit-blasting SMT2 formulas into CNFs and (i) an off-the-shelf model counter. Phase 1: Bit-blasting The bit-blasting component takes an input bit-vector formulaFand outputs a CNF formulaF bit such that the elements ofSol(F bit ) has one-to-one correspondence with elements ofSol(F). The most commonly used method for converting a bit-vector formula into a propositional Boolean formula involves representing the formula as an And-Inverter Graph (AIG) circuit,F aig , which is subsequently converted into CNF,F bit .F aig is built with primary input over individual bits of the bitvector formula,bitsF. For conversion to AIG, each bit-vector operator is lowered to a dedicated Boolean gate network over the individual bits. For example, aw-bit adder is implemented as a ripple-carry chain of full adders. Aw-bit multiplier generates w 2 partial products and then sums them using a cascade of adder networks. The AIGF aig is built by composing these per-operator sub-circuits over one another, following the structure of F. The result in every case is a directed acyclic graph of and, or, not, xor or ite gates, which are later converted to just and, or gates resulting in the AIGF aig . The AIG is converted to CNF F bit using technology mapping based conversion [EMS07]. All the auxiliary variables introduced inF bit are defined by bi-implications, therefore,Sol(F aig ) =Sol(F bit ) ↓bits(F) , andSol(F aig ) has one-one correspondence to elements in Sol(F bit ). A subset of bits inF bit directly corresponds to the actual bits of the formulaF, while the rest are auxiliary variables required for encoding constraints. The encoding ensures that the count 4 is not increased by the introduction of the auxiliary variables. These auxiliary variables are not part of the independent support ofF bit . Approximate model counters and samplers achieve better performance when provided with smaller independent support. During bit-blasting,csb identifies and tracks the variables belonging to the independent support versus auxiliary variables, relaying this information to the model counter. Phase 2: Propositional Model Counting The second phase ofcsbinvolves a proposi- tional model counter that takes the CNF formulaF bit and returnsc, the value of|Sol(F bit )|, or an approximation of that. We investigated various approaches to model counting, including both compilation-based counters and hashing-based approximate counters. In recent years, there has been a proliferation of model counters, and the annual model counting competi- tions have demonstrated that different model counters have distinct strengths and weaknesses for various problem types. In the context of this research, we examine the applicability of five model counters within the framework ofcsb: four compilation-based exact counters SharpSAT-TD[KJ21],Ganak[SRSM19],D4[LM17], andGPMC; and a hashing-based approxi- mate counterApproxMC[SM19]. Upon comparing the performances of different CNF counters, we chose the best CNF counters for exact and approximate counting. In the exact model counting mode ofcsb, we use the latest version ofGanakas used in model counting competition 2024 [FHS24a], while in the approximate model counting mode, we use ApproxMC. 3.2 Projected Model Counting The second class of problemscsbsolves is projected model counting. The architecture is the same as that of non-projected counting, but there are a few key differences. Phase 1: Bit-blasting The bit-blasting component in the projected model counting mode ofcsbis similar to the non-projected model counting mode. We useTechMapfor bit-blasting. In addition to that, it keeps track of which variables to keep projections on. On the blasted CNF, the variables are marked as projection variables. The CNF counting problem, therefore, represents a projected model counting problem. Given a bitvector formulaF, and a projection setP ⊂ Vars(F),csbdetectsP bit ⊂ Vars(F bit ) from the bitblasted formulaF bit , such that |Sol(F bit ) ↓P bit |=|Sol(F) ↓P |. The resultant problem becomes a projected CNF counting problem of formula F bit , projected on P bit . Phase 2: Propositional Projected Model Counting The CNFF bit along with the projection variablesP bit generated in the previous phase are passed to the projected model counter. In this context, we experimented with four projected model countersGanak[SRSM19], D4[LM17],GPMC, andApproxMC[SM19]. Upon comparing the performances of different CNF counters, we chose the best CNF counters for exact and approximate projected CNF counting. Similar to non-projected counting, in the exact model counting mode ofcsb, we use the latest version of Ganak, while in the approximate model counting mode, we use ApproxMC. 3.3 Uniform Sampling As shown in Figure 1, the sampling mode ofcsbcomprises three primary components: (i) a tool for bit-blasting SMT2 formulas into CNFs, (i) a CNF sampler to sample solutions (almost) uniformly from the solution space, and (i) constructing the bit-vector model from the sampled CNF solution. In the following part of this section, we briefly describe the task and available tools for each component. 5 (set-logic QF_BV) (declare-const a (_ BitVec 6)) (declare-const b (_ BitVec 6)) (declare-const c (_ BitVec 6)) (declare-const d (_ BitVec 6)) (declare-projvar a b) (declare-projvar d) (assert (bvult a #b001010)) (assert (bvult b #b011110)) (assert (= (bvadd c d) #b001000)) (check-sat) Figure 2: Example SMT formula with projection variables Phase 1: Bit-blasting The bit-blasting component generates a propositional formulaF bit from the input bit-vector formulaF, such that there is a one-to-one correspondence between Sol(F) andSol(F bit ). The techniques used in this part are the same as those in the bit-blasting component of the model counting mode. At this stage, the underlying SMT solver maintains the mapping between variables of F and F bit , allowing it to map an element of Sol(F bit ) to the corresponding element of Sol(F ). Phase 2: CNF Sampling The bit-blasted formulaF bit is passed to a CNF sampler to generate a sampleω bit , a randomly selected element fromSol(F bit ).UniGen[CFM + 15] uses hashing- based techniques to achieve almost-uniform sampling. On the other hand,CMSGen[GSCM21] incorporates randomization at various stages of an SAT solver’s process, effectively making the solver’s output mimic that of a uniform sampler. This approach resembles uniform sampling and meets distribution tests [MPC20], validating its utility. In practical scenarios, uniform- like samplers often exhibit superior performance, although some applications necessitate strict uniformity guarantees. Depending on the specific sampling requirements, we employ different CNF samplers: for almost-uniform sampling, we utilizeUniGen; for uniform-like sampling, we select CMSGen. Phase 3: Model Construction Once the CNF sampler returns a solutionω bit , it is passed to the SMT solver, which generates the corresponding bit-vector solutionS. The SMT solver uses the variable mapping from phase 1 to perform this operation. 3.4 Preprocessing In model counting and sampling, preprocessors attempt to simplify the original problem instance. In practical scenarios, the problem instances are typically rooted in circuits within a specific domain. These circuits are comprised of gates, and the variables correspond to either input or output variables, with the output variables being determined by the input variables. Preprocessing techniques have been developed to effectively handle the input-output bipartition property, as discussed in several studies [LLM16,LLM20,SM22]. Incsb, we utilizeArjun[SM22] as a preprocessor, since it consistently outperforms alternative preprocessors [SM24b]. 6 3.5 Implementation A simple approach to build the tool is to use a standalone shell script that interfaces with an SMT solver to generate a CNF file, followed by processing with a model counter or sampler. However, using shell scripts could lead to performance bottlenecks due to the overhead of file read-writes, complicate error handling, and create challenges in deployment and portability by requiring specific environmental setups and external binaries. Therefore, we chose a tightly integrated approach, embedding the counter and samplers directly within the SMT solver as a library. This integration yields a single binary that efficiently produces both model counts and samples. We implementcsbusingSTPas the underlying SMT solver. The bit-blasting procdure at STP had the following pre-/in-processing steps. We have disabled all of them, as they might have impacted the model-preserving property: (i)Bitvector-level simplifications and rewrites: BV-level solving, removal of unconstrained variables, interval analysis, rewrites underite, equality detection, splitting ofextract, share-aware rewrites. (i)Bit-level simplifications: constant-bit propagation, pure-literal elimination, propagation of top-level assertions, flattening of and/or, merging of similar ors, equivalence detection. (i)With these passes disabled, BV→CNF reduces to the two logically count-preserving stages above. One other possible source that might have broken the model preservation property is variable substitution. However, disabling simplification inSTPalso disables variable substitution. InSTP, substitutions are recorded in a substitution map that is populated by (i) constant-bit propagation, (i) pure-literal elimination, and (i) elimination of unconstrained variables. With these passes disabled, the substitution map remains empty, and variable substitution does not occur. We integrateApproxMCto implement the approximate model counter,Ganakto integrate the exact model counter, andUniGenandCMSGento implement the samplers. We also integrate Arjunas a preprocessor. When used alongsideArjun,TseitinEncandTechMapexhibit comparable performance; accordingly, we retainTechMap, the default inSTP. The default parameters for the approximate model counting mode areε= 0.8 andδ= 0.2, adhering to the standard values used in the model counting community. Our implementation is designed to be easily extensible to any (projected) model counter or sampler, requiring only minimal integration effort. However, csbleverages standard APIs for interfacing with counters and samplers; therefore, compatibility requires the availability of an API in the counters or samplers. Input format Since projection is irrelevant in the context of satisfiability, SMT-Lib [BST + 10] does not incorporate the concept of projection. To address this, we propose an extended format for problem input. Variables can be designated as projection variables using thedeclare-projvar keyword. Eachdeclare-projvarcommand can include one or more variables and multiple declare-projvarcommands are supported. Projection variables can be declared at any point in the file, provided they are specified after the variable declaration and before thecheck-sat command. This format is analogous to the one used in propositional model counting [FHS24b]. An example bitvector formula with projection variables is presented in Figure 2. 3.6 Ensuring Correctness Given the two-phase structure ofcsb, correctness of the end-to-end pipeline requires that each phase satisfy its specification. The expected property from the second phase (CNF 7 counting/sampling) is: given a Boolean formula, count (or sample uniformly) from its satisfying assignments. The model counters and samplers we use have been extensively validated in the literature [SM25,CFM + 15,CM19] and in the Model Counting Competition [HFS25]; we therefore treat CNF counting/sampling correctness as a trusted component. Thus, our primary concern is the correctness of the BV→CNF bit-blasting pipeline. We establish that this pipeline is model preserving, i.e., the satisfying assignments of the input BV formulaFare in one-to-one correspondence with the satisfying assignments of the resulting CNFF bit . We now review the toolchain to justify this property. Recall that the BV→CNF pipeline comprises two stages: (i) BV→AIG and (i) AIG→CNF. For the two steps, we rely on the following model-preservation properties. (1) BV→AIG: Recall that bit-blasting is compositional: each operator node in the AST ofF is replaced by a dedicated combinational sub-circuit over individual bits, and these sub-circuits are composed along the AST to produceF aig . We establish in two steps thatFandF aig are in one-to-one model correspondence over the primary inputs. 1. Step 1: Per-operator equivalence. For each BV operator, we manually inspect its correspond- ing AIG circuit. These are standard textbook circuits. Kroening and Strichman [KS16, Ch. 6] establish correctness for many of these circuits by expressing each bit-blasting transformation as a bi-implication between the circuit’s output bits and the BV operator’s semantics, and proving the resulting iff. We verify that each sub-circuit in our implemen- tation follows this pattern, and is therefore model-preserving. As an empirical safeguard, we further confirm this with 3-bit-width truth-table unit tests, all of which pass. 2.Step 2: Composition preserves the bijection. Given Step 1, we lift per-operator equivalence to whole-formula equivalence. Take any satisfying BV assignmentσofF. Traversing the AST bottom-up,σinduces a unique assignmentσ ′ to the wires ofF aig , and thisσ ′ satisfies F aig . Each sub-circuit’s output is functionally determined by its inputs, so no spurious models are introduced. Conversely, take any satisfying assignmentσ ′ ofF aig . Its restriction to the primary inputs is a BV assignment that satisfiesF, since each sub-circuit’s output equals the BV image of its inputs. Henceσ ↔ σ ′ is a bijection betweenSol(F) and Sol(F aig ). Our testing-based approach to correctness mirrors that of mainstream BV solvers [GD07, B09]. A fully mechanized argument, in the spirit of recent theorem proving-based efforts for bit-vector reasoning [SFL + 21], is left to future work. (2) AIG→CNF: Our toolchain uses technology-mapping-based CNF generation [EMS07]: it applies function-preserving rewrites to the AIGF aig , and then emits a CNFF bit whose auxiliary variables are constrained by bi-implications. Consequently, every satisfying input assignment ofF aig has a unique extension to a satisfying assignment ofF bit ; equivalently,Sol(F aig ) is in bijection with the projection of Sol(F bit ) onto the input variables. Emperical assurance. We assess the correctness in terms of counting accuracy by comparing counts produced bycsbagainst those generated bySMTApproxMC, the current state-of-the- art bit-vector model counter. AsSMTApproxMCis an approximate model counter, direct correctness validation by comparison alone is insufficient. However, if the actual count is e, andSMTApproxMCreturns a counts, we know the actual countslies within the range (e/(1 +ε),(1 +ε)e) with probability (1− δ). Across all benchmark instances where both csb-exactandSMTApproxMCprovided counts, we observed that the results are close enough: max e s , s e − 1<0.8, thereby increasing our confidence in the correctness and reliability ofcsb. 8 4 Experimental Evaluation The evaluation procedure was conducted using the following setup. We conducted all our experiments on a high-performance computer cluster, with each node consisting of Intel Xeon Gold 6248 CPUs. We set the memory limit to 16 GB for all configurations and ran each solver instance on a single core. To adhere to the standard timeout used in model counting competitions, we set the timeout for all experiments to 3600 seconds for both counting and sampling. 2 Baseline For the problem of model counting, we compare our performance with the prior state-of-the-art bit-vector model counter, SMTApproxMC. As noted in the related works, there are no available projected model counters or uniform samplers for bit-vectors, so we evaluate the relative performance of both of them based on the total number of benchmarks. Benchmarks We collected a substantial set of benchmarks that pertain to the problem of model counting and naturally encode them into bit-vector formulas. The benchmarks were produced using several software tools for various purposes. These includeCounterSharp[TW21], which is a quantitative software reliability estimation tool; an algorithm designed for testing robust reachability [GFB21];Delphinium, which is a cryptographic tool for automating chosen ciphertext attacks [BZG20]; andSMC, previous work on bit-vector counting [KM18]. The total number of benchmarks used in our evaluation amounts to 661. Across the suite, files contain on average 22 bit-vector variables, 205 constraints and with an overall mean width of 27 bits. The most variables in any one file is 1008, the highest constraint count in a file is 2009, and the single widest bit-vector declared spans 156 bits. For projected model counting, we used the same set of benchmarks with the addition of projection variables. In the case ofCounterSharp benchmarks, the projection variables were predefined within the benchmarks. For the remaining benchmarks, we randomly selected 30% of all variables as projection variables. With this setup, in this work, we sought to answer the following questions: RQ1.How doescsb’s performance compare with the existing state-of-the-art in different problems? RQ2. How do the various components ofcsb, such as model counting, sampling, and bit-blasting, impact its overall performance? Summary of Results In model counting mode,csbsolves nearly six times as many instances asSMTApproxMC. Out of a total of 661 instances,csb-approxcan count 640,csb-exactcan count 418; whereasSMTApproxMCis able to count 111. In projected counting mode,csb-exactsolves 643 instances, andcsb-approxsolves 659 instances. In sampling mode,csbgenerated samples from almost all the problem formulas with a median time of 1.17s and 78.4s, respectively, in the uniform-like and almost-uniform sampling mode. The uniform-like sampling mode showed better efficiency in generating samples. RQ1. Comparison with Prior State-of-the-Art Ascsbsolves three completely different problems, we compare the performance in the following three subsections. 2 Benchmarks and logfiles available at: https://doi.org/10.5281/zenodo.20637680 9 Problem 1: Model Counting CounterInstances Counted Average Runtime (s) SMTApproxMC1115973.6 csb-exact4182795.9 csb-approx640368.3 Table 1: Performance comparison on 661 non-projected instances. We experimented with configurations forcsband compared its performance withSMTApproxMC, the current state-of-the-art approximate bit-vector model counter. Table 1 shows the improve- ment in performance demonstrated bycsb. In approximate mode,csbcounted 640 instances out of 661, which is six times the number of instances counted bySMTApproxMC, which could count 111 instances. Even in exact mode,csbperforms better thanSMTApproxMC, which is an approximate counter. The average Runtime 3 of csb is also great. In the cactus plot in Figure 3, we compare the performance. Thex-axis represents the number of instances, while they-axis shows the time taken. A point (i,j) in the plot indicates that a counter countedjbenchmarks out of the total benchmarks in a set in less than or equal toiseconds. The cactus plot reveals that whileSMTApproxMCstruggles to solve more than 111 instance, csb solves more than 600 instances, each with less than 500s. 0100200300400500600700 Benchmarks 0 500 1000 1500 2000 2500 3000 3500 Runtime(s) csb-approx csb-exact SMTApproxMC Figure 3: Performance of csb with SMTApproxMC on non-projected counting. Problem 2: Projected Model Counting As there is no existing uniform bit-vector sampling tool, we do not have a baseline for comparing csbagainst. We count the number of instances solved by the approximate and exact mode of csbout of 661 instances. As Table 2 indicates, in approximate modecsbsolves 659 instances - almost all of the benchmark set consisting of 661 instances. The performance in exact mode is also quite close, wherecsbsolves 643 instances. Moreover, the cactus plot in Figure 4 indicates that in both modes, csb solves 607 instances in a minute. 3 We use the PAR-2 score as a proxy for average runtime. PAR-2 score (penalized average runtime) assigns a runtime of two times the time limit for each benchmark not solved by a counter. 10 CounterInstances Counted Average Runtime (s) csb-exact643301.4 csb-approx659140.2 Table 2: Performance comparison on 661 projected instances. 0100200300400500600700 Benchmarks 0 500 1000 1500 2000 2500 3000 3500 Runtime(s) csb-approx csb-exact Figure 4: Performance comparison of two modes of csb on projected counting. Problem 3: Uniform Sampling As there is no existing uniform bit-vector sampling tool, we do not have a baseline for comparing csbagainst. We testedcsbon our benchmarks in both sampling modes by asking it to generate 500 samples for each input formula. In Table 3, we compare the performance in terms of the number of instances solved and average runtime. Out of 661 instances, in almost-uniform sampling modecsbgenerated samples for 641 instances, while in uniform-like sampling mode, it solved 660 instances. Sampling Mode in csbInstances Sampled Avg. Time (s) Median Time (s) Almost-uniform sampling641283.778.4 Uniform-like sampling6606.61.17 Table 3: Performance comparison on sampling on 661 instances. RQ2. Impact of Different Components As shown in Section 3, there are multiple components forcsb, and there are multiple tools/algo- rithms available for each component. To determine which tools to use for each component, we performed experiments. Below, we summarize the impact of each component. Impact of CNF Counters in non-projected counting To find the best counters to use in csb, we selected solvers from the 2024 Model Counting Competition [FHS24a] for comparison. By combining each model counter with its best possible preprocessing settings, we observed that 11 ApproxMCdelivered the best performance, solving 640 out of 661 benchmarks. The second-best performance was achieved byGanak, which solved 418 benchmarks. The other exact counters —SharpSAT-TD,D4, andGPMC— performed similarly toGanak, solving 414, 359, and 342 instances, respectively. As shown in the cactus plot in Figure 3,ApproxMCoutperforms all other counters significantly, while the exact counters exhibit comparable performance. 0100200300400500600700 Benchmarks 0 500 1000 1500 2000 2500 3000 3500 Runtime(s) ApproxMC Ganak SharpSAT-TD D4 GPMC Figure 5: Performance comparison of model counters on non-projected instances. Impact of CNF Counters in projected counting Similar to the non-projected case, we evaluate projected CNF counters on the projected CNF counting instances generated bycsb. The counterSharpSAT-TDwas excluded from this evaluation as it does not support projected model counting.ApproxMCachieved the best performance, solving 659 instances. Among the exact counters,Ganakperformed the best, solving 643 instances. The other counters showed similar performance:D4solved 602 instances, andGPMCsolved 573 instances. The cactus plot in Figure 6 shows that, unlike the non-projected case, the performance gap betweenApproxMC and the exact counters is minimal, with all counters performing comparably. 0100200300400500600700 Benchmarks 0 500 1000 1500 2000 2500 3000 3500 Runtime(s) ApproxMC Ganak D4 GPMC Figure 6: Performance comparison of model counters on projected instances. 12 Impact of CNF Samplers Both CNF samplers demonstrate strong performance, solving over 94% of instances. The average runtime is significantly improved whenCMSGenis used as the sampler. In Table 3, we compare the performance metrics. UsingCMSGenas the sampler, csb solves 21 more instances and reduces the average runtime to 3% of that with UniGen. Impact of bitblasting method There are multiple techniques available for converting an AIG to CNF, with the two most commonly used being: (i)TseitinEnc: the standard Tseitin encoding [Tse83] and (i)TechMap: technology mapping-based logic synthesis [EMS07]. The TseitinEncmethod uses auxiliary variables for sub-circuits of AIG, whereas theTechMapmethod performs various optimizations on the circuit to produce a minimized CNF. From the perspective of satisfiability, studies have revealed that the performance of the encoding scheme is reliant on the benchmark set being investigated, withTseitinEncexhibiting superior results in some benchmark sets andTechMapbeing more effective in others [JLS09]. In the context ofcsb, TseitinEncandTechMapshowed similar performance, and we useTechMapfor bit-blasting, which is default inSTP. The performance ofcsbremains relatively unchanged when the bit-blasting technique is switched betweenTseitinEncandTechMapincsb. However, ifArjunis not employed as a preprocessing technique, usingTseitinEncas a bit-blasting technique instead ofTechMap can improve the performance of csb. This improvement is observed across all CNF-counters. Impact of Preprocessing The preprocessors had a minimal positive impact on the perfor- mance of exact model counting tools, and in a few cases, they even showed a slight negative effect. For the approximate model counting toolApproxMC,Arjundemonstrated a positive impact, enabling the solving of 643 instances, which is 473 more than without preprocessing. 5 Conclusion This work introducedcsb, an extension of the SMT solverSTPthat utilizes CNF counters and samplers to efficiently address counting and sampling challenges over bit-vector formulas efficiently, demonstrating strong performance on a large application benchmark set.csbsupports exact and approximate projected and non-projected model counting, as well as almost-uniform and uniform-like sampling, marking the first solution for exact counting, projected counting, and uniform sampling on bit-vector formulas. We hope that the availability of an efficient tool will inspire researchers from diverse domains to solve their problems using bit-vector counting and sampling, fostering further exploration and innovation in this area. Acknowledgements. We are thankful to anonymous reviewers for their constructive feedback. This work was supported in part by the Natural Sciences and Engineering Research Council of Canada (NSERC) [RGPIN-2024-05956]. The work was done when Arijit Shaw was a visiting graduate student at the University of Toronto. Computations were performed on the Niagara supercomputer at the SciNet HPC Consortium. SciNet is funded by Innovation, Science and Economic Development Canada; the Digital Research Alliance of Canada; the Ontario Research Fund: Research Excellence; and the University of Toronto. 13 References [B09] Robert Brummayer and Armin Biere. Boolector: An efficient SMT solver for bit-vectors and arrays. In Proc. of TACAS, 2009. [B + 22]Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres N ̈otzli, et al. cvc5: A versatile and industrial-strength smt solver. In Proc. of TACAS, 2022. [BSST21]Clark Barrett, Roberto Sebastiani, Sanjit A Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Handbook of satisfiability. 2021. [BST + 10]Clark Barrett, Aaron Stump, Cesare Tinelli, et al. The smt-lib standard: Version 2.0. In Proc. of SMT Workshop, 2010. [BZG20]Gabrielle Beck, Maximilian Zinkus, and Matthew Green. Automating the develop- ment of chosen ciphertext attacks. In Proc. of USENIX Security, 2020. [CDM15] Dmitry Chistikov, Rayna Dimitrova, and Rupak Majumdar. Approximate counting in SMT and value estimation for probabilistic programs. In Proc. of TACAS, 2015. [CFM + 15]Supratik Chakraborty, Daniel J Fremont, Kuldeep S Meel, Sanjit A Seshia, and Moshe Y Vardi. On parallel scalable uniform sat witness generation. In Proc. of TACAS, 2015. [CGSS13] Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. The mathsat5 SMT solver. In Proc. of TACAS, 2013. [CM19]Sourav Chakraborty and Kuldeep S Meel. On testing of uniform samplers. In Proc. of AAAI, 2019. [CMMV16] Supratik Chakraborty, Kuldeep Meel, Rakesh Mistry, and Moshe Vardi. Approximate probabilistic inference via word-level counting. In Proc. of AAAI, 2016. [CMV13]Supratik Chakraborty, Kuldeep S Meel, and Moshe Y Vardi. A scalable approximate model counter. In Proc. of CP, 2013. [CMV16]Supratik Chakraborty, Kuldeep S Meel, and Moshe Y Vardi. Algorithmic Im- provements in Approximate Counting for Probabilistic Inference: From Linear to Logarithmic SAT Calls. In Proc. of IJCAI, 2016. [DBS18]Rafael Dutra, Jonathan Bachrach, and Koushik Sen. Smtsampler: Efficient stimulus generation from complex smt constraints. In Proc. of ICCAD, 2018. [DBS19]Rafael Dutra, Jonathan Bachrach, and Koushik Sen. Guidedsampler: coverage- guided sampling of smt solutions. In Proc. of FMCAD, 2019. [EMS07]Niklas E ́en, Alan Mishchenko, and Niklas S ̈orensson. Applying logic synthesis for speeding up SAT. In Proc. of SAT, 2007. [FHH21]Johannes K Fichte, Markus Hecher, and Florim Hamiti. The model counting competition 2020. Journal of Experimental Algorithmics (JEA), 2021. [FHS24a]Johannes Fichte, Markus Hecher, and Arijit Shaw. Model counting competition 2024: Submitted solvers, 2024. 14 [FHS24b]Johannes Fichte, Markus Hecher, and Arijit Shaw. Model counting competition data format (version 1.1). 2024. [GD07]Vijay Ganesh and David L Dill. A decision procedure for bit-vectors and arrays. In International conference on computer aided verification. Springer, 2007. [GFB21]Guillaume Girol, Benjamin Farinier, and S ́ebastien Bardin. Not all bugs are created equal, but robust reachability can tell the difference. In Proc. of CAV, 2021. [GSCM21]Priyanka Golia, Mate Soos, Sourav Chakraborty, and Kuldeep S Meel. Designing samplers is easy: The boon of testers. In Proc. of FMCAD, 2021. [HFS25]Markus Hecher, Johannes K. Fichte, and Arijit Shaw. Model counting competition 2025: Description, 2025. [JLS09] Susmit Jha, Rhishikesh Limaye, and Sanjit A Seshia. Beaver: Engineering an efficient smt solver for bit-vector arithmetic. In Proc. of CAV, 2009. [KJ21]Tuukka Korhonen and Matti J ̈arvisalo. Integrating tree decompositions into decision heuristics of propositional model counters. In Proc. of CP, 2021. [KM18] Seonmo Kim and Stephen McCamant. Bit-vector model counting using statistical estimation. In Proc. of TACAS, 2018. [KM20]Seonmo Kim and Stephen McCamant. Structural bit-vector model counting. In SMT, 2020. [KS16] Daniel Kroening and Ofer Strichman. Decision procedures. 2016. [LLM16] Jean-Marie Lagniez, Emmanuel Lonca, and Pierre Marquis. Improving model counting by leveraging definability. In Proc. of IJCAI, 2016. [LLM20] Jean-Marie Lagniez, Emmanuel Lonca, and Pierre Marquis. Definability for model counting. Artificial Intel ligence, 2020. [LM17] Jean-Marie Lagniez and Pierre Marquis. An improved decision-dnnf compiler. In Proc. of IJCAI, 2017. [MPC20]Kuldeep S Meel, Yash Pralhad Pote, and Sourav Chakraborty. On testing of samplers. Proc. of NeurIPS, 2020. [NP23] Aina Niemetz and Mathias Preiner. Bitwuzla. In Proc. of CAV, 2023. [PRI23]Matan I Peled, Bat-Chen Rothenberg, and Shachar Itzhaky. Smt sampling via model-guided approximation. In Proc. of FM, 2023. [SFL + 21]Xiaomu Shi, Yu-Fu Fu, Jiaxiang Liu, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo- Yin Yang. Coqqfbv: a scalable certified smt quantifier-free bit-vector solver. In International Conference on Computer Aided Verification, pages 149–171. Springer, 2021. [SM19] Mate Soos and Kuldeep S Meel. BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In Proc. of AAAI, 2019. 15 [SM22]Mate Soos and Kuldeep S. Meel. Arjun: An efficient independent support computa- tion technique and its applications to counting and sampling. In Proc. of ICCAD, 2022. [SM24a]Arijit Shaw and Kuldeep S Meel. Model counting in the wild. In Proc. of KR, 2024. [SM24b]Mate Soos and Kuldeep S Meel. Engineering an efficient preprocessor for model counting. In Proceedings of the 61st ACM/IEEE Design Automation Conference, pages 1–6, 2024. [SM25]Mate Soos and Kuldeep S Meel. Engineering an efficient probabilistic exact model counter. In International Conference on Computer Aided Verification, pages 72–91. Springer, 2025. [SM26] Arijit Shaw and Kuldeep S Meel. CSB: A Counting and Sampling tool for Bit-vectors.Acta Informatica, 63(3):23, 2026.https://doi.org/10.1007/ s00236-026-00535-0. [SRSM19] Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S Meel. Ganak: A scalable probabilistic exact model counter. In Proc. of IJCAI, 2019. [Tse83]Grigori S Tseitin. On the complexity of derivation in propositional calculus. In Automation of reasoning. Berlin, Heidelberg, 1983. [TW21] Samuel Teuber and Alexander Weigl. Quantifying software reliability via model- counting. In Proc. of Quantitative Evaluation of Systems, 2021. 16

Instant research discovery