CSB: A Counting and Sampling Tool for Bit-vectors

This arXiv paper presents csb, a tool for model counting and sampling over bit-vector formulas. It bit-blasts formulas into CNF and then invokes modern CNF model counters or samplers. The supported tasks include exact and approximate counting, projected and non-projected counting, almost-uniform sampling, and uniform-like sampling. The authors report substantial performance improvements over existing methods, but the supplied abstract does not provide benchmark sizes, runtimes, solver configurations, or quantified gains. The work is relevant to SMT-based verification and probabilistic analysis where satisfiability alone is insufficient.