It applies both to our work on ParamILS and to our work on the empirical analysis of algorithm configuration (algorithm design) scenarios.

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.

According to a manual count in the CPLEX user manual, there are 159 user-specifiable parameters. However, many of these parameters deal with various configuration options that are independent of the search strategy. We identified 81 parameters that affect the search (note that we are not intimately familiar with CPLEX, and might have missed some parameters, or have chosen to modify parameters that do not matter -- the fact that we are still able to improve over its default parameters merely demonstrates the great promise that lies in automated parameter tuning). We did take special care to not include parameters that would change the problem, for example by modifying the required precision of the solution.

A large number of CPLEX' parameters deal with MIP strategy heuristics (such as variable and branching heuristics, probing, dive type and subalgorithms) and with the amount and type of preprocessing to be performed. There are also nine parameters governing how frequently a different type of cut should be used (there are four magnitude values and the value “choose automatically”; note that this last value prevents the parameters from being ordinal). A considerable number of other parameters deal with simplex and barrier optimization, and with various other algorithm components. For numerical parameters with an automatic option, we chose that option instead of hypothesizing numerical values that might work well. We also identified a number of numerical parameters that dealt primarily

with numerical issues, and fixed those to their default values. For other numerical parameters, we chose up to five possible values that seemed sensible, including the default. For the many categorical parameters with an automatic option, we included the automatic option as a choice for the parameter, but also included all the manual options. Finally, we ended up with 63 configurable parameters, leading to 1.78 * 10^38 possible configurations. Exploiting the fact that seven of the CPLEX parameters were only relevant conditional on other parameters taking certain values, we reduced this to 1.38 * 10^37 distinct configurations. As the starting configuration for our configuration procedures, we used the default settings, which have been obtained by careful manual configuration on a broad range of MIP instances.

For a list of all parameters we selected for tuning, as well as the values we considered, see the file cplex-params.txt, which is in the format described in the ParamILS quickstart guide. There is also another copy of that parameter file, where we categorize each parameter into the three categories integer (I), categorical (C), and continuous numerical (N), and also determine the size of configuration space with and without exploiting conditional parameters.

Please send any questions, concerns or comments to Frank Hutter