Abstract: Over the last two decades, software engineering has witnessed a silent revolution in the form of Boolean SAT solvers. These solvers are now integral to many analysis, synthesis, verification, and testing approaches. This is largely due to a dramatic improvement in the scalability of these solvers vis-a-vis large real-world formulas. What is surprising is that the Boolean satisfiability problem is NP-complete, believed to be intractable in general, and yet these solvers easily solve 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 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 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 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 now widely used in industry and academia.
