TITLE:  On The Unreasonable Effectiveness of SAT Solvers

ABSTRACT: 

Over the last two decades, software engineering (broadly construed to include testing, analysis, synthesis, verification, and security) has witnessed a silent revolution in the form of Boolean SAT and SMT solvers. These solvers are now integral to many testing, analysis, synthesis, and verification approaches. This is largely due to adramatic improvement in the scalability of these solvers vis-a-vis large real-world formulas. What is surprising is that the Booleansatisfiability problem is NP-complete, believed to be intractable, and yet these solvers easily solve industrial instances containing millions of variables and clauses in them. How can that be?

In my talk, I will address this question of why SAT solvers are soefficient through the lens of machine learning (ML) as well as ideas from (parameterized) proof complexity. While the focus of my talk is almost entirely empirical, I will show how can we leverage theoretical ideas to not only deepen our understanding but also to build better SAT solvers. I will argue that SAT solvers are best viewed as proof systems, composed of two kinds of sub-routines, ones that implement proof rules and others that are prediction engines that optimize some metric correlated with solver running time. These prediction engines can be built using ML techniques, whose aim is to structure solverproofs in an optimal way. Thus, two major paradigms of AI, namely ML and logical deduction, are brought together in a principled way in order to design efficient SAT solvers. A result of my research is the MapleSAT solver, that has been the winner of several recent international SAT competitions and is widely used inindustry and academia.

BIO:

Dr. Vijay Ganesh is an associate professor at the University of Waterloo. Prior to joining Waterloo in 2012, he was a research scientist at MIT (2007-2012) and completed his Ph.D. in computer science from Stanford in 2007. Ganesh’s primary area of research is the theory and practice of automated mathematical reasoning algorithms aimed at software engineering, security, and mathematics. In this context he has led the development of many SAT/SMT solvers, most notably, STP, Z3 string, MapleSAT, and MathCheck. He has also proved several decidability and complexity results in the context of first-order theories. He has won over 25 awards, honors, and medals to date for his research, including an ACM Impact Paper Award at ISSTA 2019, ACM Test of Time Award at CCS 2016, and a Ten-Year Most Influential Paper citation in 2008. He is the editor-in-chief of the Springer book series Progress in Computer Science and Applied Logic (PCSAL) and has co-chaired many conferences, workshops, and seminars including a Simons Institute semester on Boolean Satisfiability in 2021.