Scalable and Provable Distributed SAT Solving

Abstract

SAT and SMT solvers are the "engines of proof" that underly many of our automated reasoning tools.  At Amazon, we make billions of calls to SAT and SMT solvers each day.    Recent progress in distributed SAT solving has led to solvers that can solve problems 30-50 times faster on average (up to one hundred times faster) than sequential SAT solvers by sharing derived information among multiple sequential solvers working on the same problem.  We believe that these techniques can be adapted for SMT solvers for similar scalability gains.

Unlike sequential solvers, however, distributed solvers have not been able to produce proofs of unsatisfiability in a scalable manner, which has limited their use in critical applications. This talk will present a recently published method to produce unsatisfiability proofs for distributed SAT solvers by combining the partial proofs produced by each sequential solver into a single, linear proof.  I describe how proof support is implemented in the state-of-the-art open-source distributed solver Mallob, and demonstrate how proofs can be efficiently assembled even from large scale distributed SAT solvers (100 machines, 1600 cores in total).  This combination of scalability and rigor with distributed solvers unlocks the use of SAT solvers problems that were previously impractical to solve, involving domains such as optimization and program verification.

Author

Dr. Michael Whalen is a Principal Applied Scientist at Amazon Web Services and the former Director of the University of Minnesota Software Engineering Center.  Dr. Whalen is interested in formal analysis, language translation, testing, and requirements engineering.  He has led development of simulation, translation, testing, and formal analysis tools for C, Rust, and Model-Based Development languages including Simulink, Stateflow, SCADE, and RSML-e, and has published 90 peer-reviewed articles on these topics.  Dr. Whalen has led successful formal verification projects on foundational Amazon C libraries and large industrial avionics models, including secure autonomous vehicles (DARPA HACMS project), pilots’ displays (Rockwell-Collins ADGS-2100 Window Manager), redundancy management and control allocation (AFRL CerTA FCS program) and autoland (AFRL CerTA CPD program).  He is currently working on formal verification at “cloud scale”, looking at how to create proof engines that can cost-effectively scale to larger and more complex problems than are handled by current tools.  He is also involved with outreach, helping developers and business customers apply verification tools to improve their team’s quality, velocity, and innovation.

View Slides (You must register and request HCSS Community Membership to download the slides.)