Skip to content

RafaelTupynamba/quicksampler

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

10 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

QuickSampler

Efficient Sampling of SAT Solutions for Testing

Paper

Update

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.

Building

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

Running

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.

Benchmarks

The benchmarks used are included under the Benchmarks directory. Like UniGen2, QuickSampler expects formulas in DIMACS CNF format, with the independent support specified.

Comparison with SearchTreeSampler

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.

Comparison with UniGen2

For comparison with UniGen2, the source code can be obtained from https://bitbucket.org/kuldeepmeel/unigen.

Paper

ICSE 2018 paper

Efficient Sampling of SAT Solutions for Testing

Rafael Dutra, Kevin Laeufer, Jonathan Bachrach, Koushik Sen

About

Efficient Sampling of SAT Solutions for Testing

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published