Sticky is a parallel SAT solver originally based on Glucose-Syrup 4.0. Sticky uses physical clause sharing, whereby all clauses are represented only once in memory. This is an early stage prototype and is in this version not under development any more.

cd sticky
mkdir build
cd build
cmake ..
make -j

Running standard sticky with 4 threads, maximal 1 hour (3600s) runtime and 4 GB (4000MB) memory:

./sticky -nthreads=4 -maxmemory=4000 -maxtime=3600 ~/path/to/sat_problem.cnf

Running sticky with export vivification and a max LBD of 4 for vivification clauses:

./sticky -nthreads=4 -useExportVivi -maxVifiLBD=4 ~/path/to/sat_problem.cnf

For more useful flags use one of the following two lines:

./sticky --help # shows available flags
./sticky --help-verb # shows flags and short describtions

Sticky was developed at Zuse Institute Berlin. Employees were funded by BMBF under grand 01IH15006C. We thank the Glucose-Syrup team and the Minisat team for providing the baseline source codes and insides into SAT solving.

For questions contact hartung(ät)zib(dot)de