Efficient Sampling of SAT Solutions for Testing
Please check out our most recent work SMTSampler. SMTSampler brings some important improvements over QuickSampler and also allows sampling from SMT formulas with bit-vectors and arrays.
Install dependencies
sudo apt install git g++ make python-minimal
Clone repos
git clone https://github.com/RafaelTupynamba/quicksampler.git
git clone https://github.com/Z3Prover/z3.git
Build z3 (with a patch to check samples generated by QuickSampler)
cd z3
git checkout 9635ddd8fceb6bdde7dc7725e696e6c123af22f4
cp ../quicksampler/check/sat_params.pyg src/sat/sat_params.pyg
cp ../quicksampler/check/dimacs.cpp src/sat/dimacs.cpp
cp ../quicksampler/check/dimacs_frontend.cpp src/shell/dimacs_frontend.cpp
python scripts/mk_make.py
cd build
make
sudo make install
cd ../..
Build QuickSampler
cd quicksampler
make
Simply run with
./quicksampler -n 10000000 -t 7200.0 formula.cnf
QuickSampler will create a file formula.cnf.samples with the samples generated and print statistics to standard output. The file formula.cnf.samples has one line for each produced sample. The first number represents the number of atomic mutations which were used to generate this sample. Then, the sample is displayed in a compact format, with characters '0' and '1' indicating the assignments to each of the variables in the independent support.
The option -n can be used to specify the maximum number of samples produced and the option -t can be used to specify the maximum time allowed for sampling.
To check the validity of the samples generated, run z3 with the option sat.quicksampler_check=true
z3 sat.quicksampler_check=true sat.quicksampler_check.timeout=3600.0 formula.cnf
The option sat.quicksampler_check.timeout can be used to establish a timeout for the checking of all samples produced. If the time required to check all samples is larger than this timeout, we will uniformly choose a subset of the samples to check. A timeout of 0.0 disables the timeout.
Running z3 with the option sat.quicksampler_check=true will read samples from formula.cnf.samples, check if they satisfy the formula formula.cnf and create a file formula.cnf.samples.valid with the valid samples. This final output file formula.cnf.samples.valid will have one line for each unique valid solution, displaying the solution in DIMACS format, followed by number of times this solution was sampled.
The benchmarks used are included under the Benchmarks directory. Like UniGen2, QuickSampler expects formulas in DIMACS CNF format, with the independent support specified.
For convenience, we provide the patch STS/STS.patch that we applied over the SearchTreeSampler source code STS/STS.zip for it to use the independent support for sampling.
For comparison with UniGen2, the source code can be obtained from https://bitbucket.org/kuldeepmeel/unigen.
Efficient Sampling of SAT Solutions for Testing
Rafael Dutra, Kevin Laeufer, Jonathan Bachrach, Koushik Sen