Logic Solvers and Machine Learning: The Next Frontier

Abstract: Over the last two decades, software engineering has witnessed a silent revolution thanks in large part due to Boolean SAT and SMT solvers. These solvers are now integral to many analysis, synthesis, verification, and testing approaches. This is largely because of dramatic improvements in the scalability of these solvers. What is surprising is that the Boolean satisfiability and related first-order problems are NP-complete or worse, believed to be intractable in general, and yet these solvers manage to easily solve real-world 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 so efficient through the lens of machine learning as well as ideas from (parameterized) proof complexity. I will argue that SAT solvers are best viewed as proof systems, composed of both proof construction and prediction engines that optimize some metric correlated with solver running time. These prediction engines can be built using machine learning (ML) techniques, whose aim is to structure solver proofs in an optimal way. Thus, two major paradigms of AI, namely machine learning and logical deduction, are brought together in a principled way with the aim of designing efficient SAT solvers. A result of my research is the MapleSAT solver, that has medaled at several recent international SAT competitions, and is now widely used in industry and academia. I will also discuss some new ideas in applying solvers to ML with the goal of improving their robustness, data efficiency, and security.

Bio: Dr. Vijay Ganesh is an associate professor at the University of Waterloo, Canada. Prior to joining Waterloo in 2012, he was a research scientist at MIT (2007-2012) and completed his PhD in computer science from Stanford University in 2007. Vijay’s primary area of research is the theory and practice of automated mathematical reasoning algorithms (aka solvers) aimed at software engineering, formal methods, security, and mathematics. In this context he has led the development of many SAT/SMT solvers, most notably, STP, Z3str3, HAMPI, MapleSAT, and MathCheck. He has also proved several decidability and complexity results in the context of first-order theories. Vijay has won over 25 awards, honors, and medals to-date for his research, including an ACM Impact Award at ISSTA 2019, ACM Test of Time Award at CCS 2016, several best paper awards, two Google Faculty Research Awards in 2011 and 2013, and a Ten-Year Most Influential Paper citation at DATE 2008.