=Paper=
{{Paper
|id=Vol-1639/paper-01
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-1639/paper-01.pdf
|volume=Vol-1639
}}
==None==
<pdf width="1500px">https://ceur-ws.org/Vol-1639/paper-01.pdf</pdf>
<pre>
          An Empirical Understanding of Conflict-Driven
                 Clause-Learning SAT Solvers
                                         Vijay Ganesh
                                 University of Waterloo, Canada
                                  vijay.ganesh@uwaterloo.ca
                              https://ece.uwaterloo.ca/~vganesh

Abstract. Conflict-driven clause-learning (CDCL) SAT solvers have deeply influenced soft-
ware engineering and security research over the last two decades, thanks largely to the fact that
these solvers can easily solve real-world constraints with millions of variables and clauses in
them. This phenomenon has puzzled theoreticians and practitioners alike. It is widely believed
that industrial instances solved efficiently by SAT solvers are highly structured. However, until
recently there was little understanding of the structure of industrial instances or the way solvers
go about exploiting the said structure.

In this talk, I will introduce CDCL SAT solvers, and the most important heuristics that power
them. In addition, I will give an answer to the question of why SAT solvers are efficient on
industrial instances. My answer is based on empirical discoveries my collaborators, students,
and I have made via a rigorous and systematic experimental study of CDCL SAT solvers and
industrial instances. I will conclude with a mathematical model that incorporates our empirical
discoveries.

Biography. Dr. Vijay Ganesh is an assistant professor at the University of Waterloo. Prior
to that he was a research scientist at MIT, 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 reasoning 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, the Z3 string solver, MapleSAT,
and MathCheck. He has also proved several decidability and complexity results in the context
of theories over string equations and integers. For his research, he won the Early Researcher
Award (ERA) in 2016, an IBM Research Faculty Award in 2015, Google Research Faculty
Awards in 2013 and 2011, and 7 best paper awards/honors at conferences like ISSTA, SAT,
CAV, CADE, SPLC, IJCAI, and DATE (including a Ten-Year Most Influential Award). His
solvers STP and MapleSAT have won numerous awards at the highly competitive international
SMT and SAT solver competitions. Recently he was invited to the first Heidelberg Laureate
Forum in 2013, a gathering where young researchers from around the world were selected to
meet with Turing, Fields and Abel Laureates.

</pre>