SAT Industrial Day

Talk at the SAT Industrial Day 2016


Solvers are usually parameterized, and different settings can lead to quite different behavior in practice. As such, a tedious task for the user is to optimize the settings of the solver for his particular needs (input). Experts (aka solvers designers) have usually enough knowledge about the solvers internals to provide settings good enough for a class of problems they are familiar with. This task is much more challenging for simple users of the solvers or experts on arbitrary problems. Fortunately, there exists now software to help the latter in that task. Marius Lindauer will introduce the Sequential Model-based Algorithm Configuration (SMAC) tool, a state-of-the-art algorithm configuration optimizer.


  • Algorithm Configuration motivation and problem statement
  • Introduction into algorithm configuration procedures (focus: SMAC)
  • Overview on parameter importance
  • Automatic construction of parallel portfolios
  • Per-Instance algorithm configuration
  • Robust benchmark sets


Tool Links


Marius Lindauer