Con ict-driven clause-learning (CDCL) SAT solvers have deeply in uenced software 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 e ciently 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 e cient 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 In uential 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 rst Heidelberg Laureate Forum in 2013, a gathering where young researchers from around the world were selected to meet with Turing, Fields and Abel Laureates.