Solving Puzzles with Constraint Solvers (glt22)


Manage episode 326472735 series 1910928
CCC media team tarafından hazırlanmış olup, Player FM ve topluluğumuz tarafından keşfedilmiştir. Telif hakkı Player FM'e değil, yayıncıya ait olup; yayın direkt olarak onların sunucularından gelmektedir. Abone Ol'a basarak Player FM'den takip edebilir ya da URL'yi diğer podcast uygulamalarına kopyalarak devam edebilirsiniz.
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. about this event:

11730 bölüm