A new open-source tool called CSB lets SMT solvers count and sample solutions over bit-vector formulas, not just check whether a solution exists.
Satisfiability modulo theory (SMT) solvers are the workhorses of formal verification, bug-finding, and program analysis — they answer whether a set of logical constraints can be satisfied. CSB extends that by tackling two harder problems: counting how many solutions exist, and drawing samples from that set. It does this by converting bit-vector formulas into conjunctive normal form (CNF) using a technique called bit-blasting, then handing the result to existing CNF model counters and samplers. The tool supports exact and approximate counting, projected and non-projected variants, and both almost-uniform and uniform-like sampling. The researchers report significant performance gains over prior methods.
The progression mirrors what happened in Boolean satisfiability research, where solvers that once only returned true or false eventually grew into full counting and sampling ecosystems. Bringing that same capability to the richer theory of bit-vectors matters for security analysis and software verification, where knowing the distribution of valid inputs — not just one — can expose hard-to-find vulnerabilities or quantify information leakage.
The bit-blasting approach is well-trodden, which means CSB is more an efficient assembly of existing machinery than a theoretical leap — but in tooling, that kind of engineering work is often what actually gets used.