Conflict-driven clause learning (CDCL) has been the de facto standard in modern SAT solving since the early 00s. CDCL triggered the disruption embodied by SAT technology, and enabled the continued practical success of SAT. This talk overviews CDCL SAT solving, it provides a historical perspective on the development of CDCL, and proposes a practical intuition for why CDCL SAT solvers work in practice. The talk then investigates ways to improve CDCL SAT solvers, relating with recent work on the topic. The final part of the talk overviews the use of CDCL SAT solvers as oracles, which finds a growing range of applications, including the recent success in solving QBF, among others.

Bio:

Joao Marques-Silva is Professor of Informatics, Faculty of Science, University of Lisbon (FCUL). Before joining FCUL, he was affiliated with Instituto Superior Tecnico, Portugal; University College Dublin, Ireland; and University of Southampton, United Kingdom. Dr. Marques-Silva current research interests include constraint-based problem solving using different constraint solving paradigms, analysis of over-constrained systems, applied formal methods, applications in software engineering, including model checking, testing, debugging and security, and applications in artificial intelligence, operations research, and bioinformatics. Dr. Marques-Silva is a Fellow of the IEEE and a member of the ACM. Dr. Marques-Silva was a recipient of the 2009 CAV Award for fundamental contributions to the development of high-performance Boolean satisfiability solvers.