The Sad, Happy-Ending Story of Logic and Abstraction

Once 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.

Speaker Details

You may not be the kind of person who routinely wonders who the speaker is and where they came from. But here is this Vijay D’Silva, knocking on your mailbox, claiming to have a story. He is visiting you from U. C. Berkeley, where he just began a postdoc, having recently defended his D. Phil. at the University of Oxford. He was supervised by the mighty Daniel Kroening whom he met in 2006 when he (Vijay) was a Masters student in Zurich. You may now rightly ask: What kind of person writes a biography in second person? Come to the talk and see.

Series:
Microsoft Research Talks
Date:
Speakers:
Vijay D'Silva
Affiliation:
University of California Berkeley

Series: Microsoft Research Talks