=Paper=
{{Paper
|id=Vol-3273/keynote1
|storemode=property
|title=Logic Solvers and Machine Learning: The Next Frontier (keynote abstract)
|pdfUrl=https://ceur-ws.org/Vol-3273/keynote1.pdf
|volume=Vol-3273
|authors=Vijay Ganesh
|dblpUrl=https://dblp.org/rec/conf/scsquare/Ganesh21
}}
==Logic Solvers and Machine Learning: The Next Frontier (keynote abstract)==
<pdf width="1500px">https://ceur-ws.org/Vol-3273/keynote1.pdf</pdf>
<pre>
Logic Solvers and Machine Learning: The Next
Frontier
Vijay Ganesh
University of Waterloo, Waterloo, Canada


                                      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 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, 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 so efficient 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 solver proofs in an optimal way.

                                      Keywords
                                      SAT solvers, SMT solvers, Machine learning




SC2 2021: 6th International Workshop on Satisfiability Checking and Symbolic Computation, August 19–20, 2021
$ vganesh@uwaterloo.ca (V. Ganesh)
€ https://ece.uwaterloo.ca/~vganesh/ (V. Ganesh)
 0000-0002-6029-2047 (V. Ganesh)
                                    © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
 CEUR
 Workshop
 Proceedings
               http://ceur-ws.org
               ISSN 1613-0073
                                    CEUR Workshop Proceedings (CEUR-WS.org)

</pre>