The Sad, Happy-Ending Story of Logic and Abstraction
3Once upon a time in mathematics, there was a quest to understand truth, proof, and calculation. This quest led to the discovery of mathematical logic and the theory of computation, two great, intellectual triumphs of the twentieth century. These developments revealed that even the simple logical problem of Boolean satisfiability is computationally intractable. Defying theoretical pessimism, modern SAT solvers scale to problem instances with hundreds of thousands of variables. Two pressing questions are: Why do solvers work so well? and, Can we replicate this success on other problems? In this talk, I will characterize SAT solvers as lattice-theoretic approximation algorithms. This characterization provides a new understanding of SAT algorithms. In practice, we obtain a systematic recipe for lifting SAT algorithms to new problems. This talk is self-contained. I will begin with a historical overview of mathematical logic and then introduce abstract interpretation, the unsung hero of the story. Through the eyes of abstract interpretation, we will follow a trail from George Boole's original conception of logic to modern, high-performance solvers.