TB-SPO:
Model-based approaches often come with a substantial time overhead due to their models. In time-bounded sequential parameter optimization (TB-SPO), we reduced this overhead by taking into account both the varying amount of time required for different algorithm runs and the complexity of model building and evaluation. Specifically, TB-SPO avoids the up-front cost of an initial design, introduces a time-bounded intensification mechanism, and shows how to reduce the overhead incurred by constructing and using models. Overall, we showed that TB-SPO represents a new state of the art in model-based optimization of algorithms with continuous parameters on single problem instances, and in that restricted domain also substantially outperforms ParamILS.
SPO+:
We experimentally investigated model-based approaches for optimizing the performance of parameterized randomized algorithms, concluding that sequential parameter optimization (SPO) often yields more robust performance than its competitor, sequential kriging optimization. We then investigated key design decisions within the prominent sequential parameter optimization (SPO) framework, characterizing the performance consequences of each. Based on these findings, we proposed a new version of SPO, dubbed SPO+, which extended SPO with a novel intensification procedure and log-transformed response values. This version led to substantially more robust performance than SPO.
DAVE:
We introduce a new conceptual model for representing and designing Stochastic Local Search (SLS) algorithms for the propositional satisfiability problem (SAT). Our model can be seen as a generalization of existing variable weighting, scoring and selection schemes; it is based upon the concept of Variable Expressions (VEs), which use properties of variables in dynamic scoring functions. Algorithms in our model are constructed from conceptually separated components: variable filters, scoring functions (VEs), variable selection mechanisms and algorithm controllers. To explore the potential of our model we introduce the Design Architecture for Variable Expressions (DAVE), a software framework that allows users to specify arbitrarily complex algorithms at run-time. Using DAVE, we can easily specify rich design spaces of SLS algorithms and subsequently explore these using an automated algorithm configuration tool. We demonstrate that by following this approach, we can achieve significant improvements over previous state-of-the-art SLS-based SAT solvers on software verification benchmark instances from the literature.
ParamILS:
ParamILS is a versatile tool for parameter optimization / algorithm configuration. It has helped us speed up both local search and tree search algorithms by orders of magnitude on certain instance distributions, and we hope you find it useful, too. Ultimately, we hope that ParamILS helps algorithm designers focus on tasks that are more scientifically valuable than parameter tuning.
SATenstein:
Designing high-performance algorithms for computationally hard problems is a difficult and often time-consuming task. In this work, we demonstrate that this task can be automated in the context of stochastic local search (SLS) solvers for the propositional satisfiability problem (SAT). We first introduce a generalized, highly parameterized solver framework, dubbed SATenstein, that includes components gleaned from or inspired by existing high-performance SLS algorithms for SAT. The parameters of SATenstein control the selection of components used in any specific instantiation and the behaviour of these components. SATenstein can be configured to instantiate a broad range of existing high-performance SLS-based SAT solvers, and also billions of novel algorithms. We used an automated algorithm configuration procedure to find instantiations of SATenstein that perform well on several well-known, challenging distributions of SAT instances. Overall, we consistently obtained significant improvements over the previously best-performing SLS algorithms, despite expending minimal manual effort.
