Algorithms we configured & parameter values considered
This page lists algorithms we have configured in the past, and the parameters we considered for configuration.
It applies both to our work on ParamILS and to our work on the
empirical analysis of algorithm configuration (algorithm design)
scenarios.
SAPS
SAPS is a high-performance dynamic local search algorithm for SAT solving developed by Frank Hutter, Dave Tompkins and Holger Hoos. We used a UBCSAT implementation (developed by Dave Tompkins),
specifically UBCSAT version 1.1.0ll. When introduced in 2002, SAPS was
a state-of-the-art solver, and it still performs competitively on many
instances. We chose to study this algorithm because it is well known,
it has relatively few parameters, and we are intimately familiar with
it. The original defaults for SAPS’s four continuous parameters
were set through manual configuration based on experiments with
prominent benchmark instances. These four continuous parameters control
the scaling and smoothing of clause weights, as well as the probability
of random walk steps. Having subsequently gained more experience with
SAPS’s parameters for more general problem classes (our CP-06
paper on per-instance approaches), we chose promising intervals for
each parameter, including, but not centered at, the original default.
We then picked seven possible values for each parameter spread
uniformly across its respective interval, resulting in 2401 possible
parameter configurations (these are exactly the same values as used in
our AAAI-07 paper). As the starting configuration for ParamILS, we used
the center point of each parameter’s domain.
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
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
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.
CPLEX
CPLEX is a commercial solver for mixed integer programs, developed by ILOG. We used CPLEX version 10.1.1, along with a Ruby wrapper script to start CPLEX and pass parameters to it. This wrapper scripts requires the file param_reader.rb
to assign the passed values to the right parameters. Note that this
Ruby Script simply starts the CPLEX Interactive Optimizer, reads
in the problem, sets parameters including a timeout, and
then starts the optimization.
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