Raymond Hettinger - Modern solvers: Problems well-defined are problems solved - PyCon 2019

Raymond Hettinger demonstrates how to use tree search and SAT solvers in Python to solve complex logic puzzles.

Speaker: Raymond Hettinger Every programmer should learn to use solvers, tools that reason directly from a description of a problem to its solution. Tools like AlphaZero can formulate winning strategies for games given only a description of the rules of the game. For certain classes of problems, we really can just let the computer do the work. In this talk, we learn principles, techniques, and multiple examples for three solvers available in Python. The first tool is a generic puzzle-solving framework that employs tree search strategies. We apply it to a simple sequencing problem and then to a harder sliding-block puzzle. Next, we'll look at the solver code to learn how it works. I'll also show an essential optimization technique and how to humanize the output. We demonstrate our skills by solving another famous puzzle. The second tool is called a SAT solver. It is one of the miracles of the 21st century. From first principles, I'll show you what problems it solves and the way problems need to be described for modules like *PycoSAT*. I'll provide helper functions to humanize our interactions with this great tool. Then, we'll demonstrate our skills by creating a Sudoku solver and a readable logic problem solver. The third tool is the ""multi-armed bandit"". It is a generic reinforcement learning algorithm that is easy to learn, powerful, and applicable to a broad class of problems. We apply it to winning rock-paper-scissors using pattern recognition. Lastly, I'll summarize DeepMind's paper on AlphaZero which was published in the December 2018 edition of *Science*. This gives us hints at the full potential of these techniques. Pure Python source code and examples are provided for all of the tools. Slides can be found at: rhettinger.github.io