Lecture at the SAT Summer School 2016
Abstract
Manual optimization of algorithm parameters (e.g., of SAT solvers) is a tedious, time-consuming and error-prone task; but nevertheless it is an important task since default parameter configurations often do not achieve peak performance. A recent example is the Configurable SAT Solver Challenge (CSSC), where the parameters of SAT solvers were optimized for each individual instance set and thereby the performance was often significantly improved by one or two orders of magnitude. To automate this process of parameter optimization, algorithm configurators (such as ParamILS and SMAC) have impressively shown how cutting-edge optimization and machine learning techniques can be combined to effectively solve the problem of parameter optimization. In the lecture, we will discuss how these algorithm configurators work and how they can be effectively applied to SAT solvers.