CSB (Count and Sample on Bitvectors) is an approximate model counting and almost-uniform sampling tool aimed at solving constraints of bitvectors.
To learn more about CSB, please have a look at our SMT Workshop '24 paper.
CSB uses STP as its frontend and is built on top of that. For counting it uses ApproxMC (with Arjun). For sampling, it uses UniGen.
For a quick install:
sudo apt install git cmake bison flex libboost-all-dev python3 perl build-essential python3-distutils-extra
sudo apt install zlib1g-dev libboost-program-options-dev libboost-serialization-dev libgmp-dev libmpfr-dev
git clone https://github.com/meelgroup/csb
cd csb
git submodule init && git submodule update
./scripts/deps/setup-gtest.sh
./scripts/deps/setup-outputcheck.sh
./scripts/deps/setup-cms.sh
./scripts/deps/setup-minisat.sh
./scripts/deps/setup-unisamp.sh
mkdir build
cd build
cmake ..
cmake --build .
sudo cmake --install .
The SMT-LIB2 format is the recommended file format, because it is parsed by all modern bitvector solvers. Only quantifier-free bitvectors and arrays are implemented from the SMT-LIB2 format.
The samples should be uniform in practice. Run with an SMT-LIB2 file:
./csb -s --ns 10 --seed 6 myproblem.smt2
The samples are generated with theoretical guarantees on uniformity. But this procedure might be slower than uniform-like sampler.
./csb -u --ns 10 --seed 6 myproblem.smt2
Change seed value to get different samples. Refer to this post to know more about uniform, almost-uniform and uniform like samplers.
Run with an SMT-LIB2 file:
./csb -c myproblem.smt2
CSB converts bitvector constraints into SAT using STP, integrating with ApproxMC or UniGen based on specific needs of counting or sampling. The benchmarks used for evaluating CSB in the SMT workshop paper are available here.
Please refer to STP/UniGen/ApproxMC for the respective authors.