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 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 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.


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