Date
Thursday, 21 Jan 2016 7:30 PM
Hi C++ Freaks und Frohes Neues! – Time for January’s get-together. This time we have Rüdiger Ehlers on Using Modern Solvers.
Many computationally difficult problems can be framed as queries to so-called solvers. Examples are the solution of Sudokus (or their automatic preparation), scheduling problems, planning in general, verification/test generation problems, and package dependency problems in Linux package managers. By describing the requirements on the solutions that are to be obtained as constraints to a solver and applying the solver as a black box library, the developer saves the work to implement branch-and-bound algorithms or related concepts to search for solutions. In this way, the results of years of sophisticated solver engineering can be used without knowing their details.
The talk gives a high-level overview on the motivation and application of modern solvers. Small example programs that employ the C++ interface of the SMT-solver Z3 by Microsoft Research show how solvers can be used in practice.
