SAT and Satisfiability Modulo Theories (SMT) solvers have many important applications in PL, including verification, testing, type checking and inference, and program analysis – but they are often a mysterious black box to their users, even when those users are PL researchers with lots of solver experience! This talk will be partly a tutorial introduction to the inner workings of SAT and SMT solvers, and partly an extended analogy to navigating life as a researcher: making decisions when you have only incomplete information to go on, learning from decisions that turned out to be bad, and determining when to give up and when to try again. I’ll also highlight a variety of papers in this year’s POPL program that make use of SAT and SMT solving, and discuss why I think it’s worthwhile to learn about solver internals.
- Introduction
- Self-intro
- My research: "language-based approaches to building parallel and distributed software systems that are correct and efficient"
- three examples, one unifying principle: not only do high-level abstractions not have to compromise performance, they can actually enable it
- the performance/productivity/generality trilemma
- lead-in to talking about SAT/SMT solving
- The so-called "SMT revolution"
- List a bunch of PL and PL-adjacent papers in the last 15 years that use SAT/SMT
- Heule and Kullman describe SAT and SMT as a "disruptive" technology
- A lot of PL researchers use SAT and SMT solvers as a black box
- I decided around 2017 that I wanted to open the box and know more about how SAT and SMT solvers work
- (Strangely enough, I decided to do this as a side effect of the so-called deep learning revolution. Leave it to a PL person to react to deep learning by saying "I must learn about SAT solvers"...)
- I discovered that the SAT solving process is strangely analogous to life as a researcher
- "You have to get into your bunker and prepare for the onslaught of failure." -- Matt Might
- Making decisions when you have only incomplete information to go on
- Learning from decisions that turned out to be bad
- Determining when to give up and when to try again
- Overview of this talk
- Part tutorial intro to the inner workings of SAT/SMT solvers, partly extended analogy to life as a researcher
- Will talk about SAT, but all this is relevant to SMT as well because SMT solvers are built on top of an underlying SAT solver
- Highlighting some papers in this year's POPL program that use SAT or SMT solving
- Why I think it's worthwhile for us PL folk to learn about solver internals
- What is the SAT problem?
- Definition of the boolean satisfiability problem
- Famously NP-complete
- Example problem from chapter 2 of Kroening and Strichman -- radio station frequency allocation -- and how to encode it as a SAT problem
- Overview of solving
- Three phases: simplify, decide, and learn
- Simplification: BCP
- Implementation of an "elementary-school" SAT solver (no guessing)
- Grown-up SAT solving -- all that stuff I talked about before:
- Making decisions when you have only incomplete information to go on: decision heuristics
- Learning from decisions that turned out to be bad: clause learning
- Determining when to give up and when to try again
- What we glossed over: internals of decision heuristics, creation of conflict clauses
- Quick example of creation of conflict clauses
- What lessons can we take away for research and life?
- Part of being a grown-up (and a researcher) is figuring out what to do when you don't have all the information (and be ready to do something else later if it doesn't work!)
- Don't be paralyzed -- try something. Maybe it won't work, but you will have learned something from the experience
- But, use heuristics (advice from experts and friends) to guide the search
- It's useful to periodically take stock of what you've learned and summarize that information (e.g., add a conflict clause to your formula) for easy understandability.
- You have to do this anyway to give talks and write paper introductions
- Part of being a grown-up (and a researcher) is figuring out what to do when you don't have all the information (and be ready to do something else later if it doesn't work!)
- Why do I think it's worthwhile to learn about solver internals?
- It's fun and useful to know how your tools work
- That trilemma thing -- PL people can learn from what solver people already know
- Once we understand how solvers are developed today, can we use PL principles to democratize solver development? I sure hope so. Come do research in the LSD lab at UCSC and help us find out!