Benedikt Maderbacher

Constraint solvers are powerful tools that can be used to solve various problems. We will look at the open source solver Z3 and see how to use it for logic puzzles and other applications.

In the first part of the talk you will learn about Z3 and how to model classic puzzles such as Sudoku. If you are programmer you might want to implement a back tracking algorithm to solve this specific problem. However, you would have to write a new program for each puzzle from scratch. Would it not be nice if we could simply state the rules of each game and the computer does everything from there? That is exactly what a constraint or SMT solver provides. We merely give Z3 the rules and the concrete instance of each puzzle and it will tell us the answer. After covering the fundamentals and logic puzzles the second part will move away from recreational puzzles and discuss other applications. Such as: resolving complex dependencies in a package manager, or finding inputs that might crash a program.