CSB (Count and Sample on Bitvectors) is an exact / approximate model counting and almost-uniform sampling tool aimed at solving constraints of bitvectors. CSB supports projection and weighted model counting.
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.
If you are using Linux, use of the release binaries is strongly encouraged, as CSB requires a specific set of libraries to be installed.
If you want a local build of CSB, or use MacOS please follow the instructions below.
Simply install nix, then build csb:
nix --extra-experimental-features 'nix-command flakes' build github:meelgroup/csb#csb
Then you will have csb binary available at result/bin/csb and ready to use.
If you want to build manually on MacOS or Linux, see the build.md file for detailed instructions.
The input is expected in SMT-LIB2 format. See the section on input format for details on projected or weighted model counting.
Run with an SMT-LIB2 file:
./csb myproblem.smt2
Run with an SMT-LIB2 file:
./csb -a myproblem.smt2
The samples should be uniform in practice. Run with an SMT-LIB2 file:
./csb -s -n 10 myproblem.smt2
The samples are generated with theoretical guarantees on uniformity. But this procedure might be slower than uniform-like sampler.
./csb -u -n 10 myproblem.smt2
Change seed value to get different samples. Refer to this post to know more about uniform, almost-uniform and uniform like samplers.
./csb -c myproblem.smt2
The SMT-LIB2 format is extended to support projection variables and weights. The extensions are described below.
CSB supports projection variables for counting and sampling. Variables can be designated as projection variables using the declare-projvar keyword. Each declare-projvar command can include one or more variables and multiple declare-projvar commands are supported. Projection variables can be declared at any point in the file, provided they are specified after the variable declaration and before the declare-projvar command. Here is an example of extending the SMT-LIB2 format to include projection variables.
(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)
CSB supports weights for variables in the counting process. Weights can be assigned to each variable (and its negation) using the declare-weight keyword in floating point. Weights can be assigned to Boolean variables only. Here is an example of extending the SMT-LIB2 format to include weights. Weights can be used with or without projection variables.
(set-logic QF_BV)
(declare-const p Bool)
(declare-const q Bool)
(declare-const x (_ BitVec 4))
(declare-const y (_ BitVec 4))
(declare-projvar p q)
(declare-weight p 0.8)
(declare-weight -p 1.0)
(declare-weight q 0.3)
(assert (=> p (= (bvadd x y) #xA)))
(assert (=> q (= (bvadd x y) #x5)))
(check-sat)
You can add weights to both literals of a variable. If only one literal is given a weight w, the other literal is assigned a default weight of (1.0-w). If no weights are provided for a projection variable, both literals are assigned a default weight of 0.5.
CSB converts bitvector constraints into SAT using STP, integrating with Ganak, ApproxMC, CMSGen, 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/Ganak/UniGen/ApproxMC/CMSGen for the respective authors.