We used UBCSAT with a Ruby wrapper script to select the SAPS algorithm and pass parameters to it. This wrapper scripts requires the file param_reader.rb to assign the passed values to the right parameters. All parameters are given in the file saps-params.txt, which is in the format described in the ParamILS quickstart guide. SAPS is in some sense the least interesting of our algorithms and we thus did not include it in our empirical analysis of algorithm design scenarios. However, we have performed experiments with it and they are qualitatively very similar to the ones for SATenstein.
SPEAR is a recent tree search algorithm for solving SAT problems,
developed by Domagoj Babic.
SPEAR is a state-of-the-art SAT solver for industrial instances, and
with appropriate parameter settings it is the best available solver for
certain types of hardware and software verification instances (see our
FMCAD-07 paper). Furthermore, configured with ParamILS, SPEAR won the
quantifier-free bit-vector arithmetic category of the 2007
Satisfiability Modulo Theories Competition. SPEAR has 26 parameters,
including ten categorical, four integer, and twelve continuous
parameters, and their default values were hand tuned by its developer.
The categorical parameters mainly control heuristics for variable and
value selection, clause sorting, resolution ordering, and enable or
disable
optimizations, such as the pure literal rule. The continuous and
integer parameters mainly deal with activity, decay, and elimination of
variables and clauses, as well as with the interval of randomized
restarts and percentage of random choices. We discretized the integer
and continuous parameters by choosing lower and upper bounds at
reasonable values and allowing between three and eight discrete values
spread relatively uniformly across the resulting interval, including
the default, which served as the starting configuration for ParamILS.
The number of discrete values was chosen according to our intuition
about the importance of each parameter. After this discretization,
there were 3.7 * 10^18 possible parameter configurations. However,
exploiting the fact that nine of the parameters are conditional (i.e.,
only relevant when other parameters take certain values) we reduced the
total to 8.34 * 10^17 configurations.
We used the 32-bit version 1.2.1 of SPEAR along with a Ruby wrapper script. This wrapper scripts requires the file param_reader.rb to assign the passed values to the right parameters. All parameters are detailed in the file spear-params.txt, which is in the format described in the ParamILS quickstart guide.
SATenstein is a framework for local search solvers for SAT, developed by Ashiqur KhudaBukhsh. We used version 1.0, along with a Ruby wrapper script. This wrapper scripts requires the file param_reader.rb to assign the passed values to the right parameters.
There are 41 parameters; for an explanation of them, see the SATenstein quickstart guide. Parameter configuration space is split into two disjoint subspaces, one space for dynamic local search (DLS) methods and one for non-DLS methods. The two parameter files are given in satenstein-dls-params.txt and satenstein-params.txt (non-DLS); the format of these files is described in the ParamILS quickstart guide. For our empirical analysis paper, we randomly sampled 500 configurations from each subspace.
Please send any questions, concerns or comments to Frank Hutter