Tutorial Speaker
João Marques-Silva holds a PhD degree from the University of Michigan, Ann Arbor, USA, in 1995, and the Habiliation degree in Computer Science from Universidade Técnica de Lisboa, Portugal, in 2004. Currently, he is Professor of Computer Science, Faculdade de Ciências da Universidade de Lisboa, Portugal. He has also been affiliated with University College Dublin, Ireland, University of Southampton, United Kingdom, and Instituto Superior Técnico, Lisbon, Portugal. His research interests include decision and function procedures, analysis of over-constrained systems, and applications in artificial intelligence, formal methods and software engineering. He received the 2009 CAV award for fundamental contributions to SAT solvers.
Abstract
Propositional SAT solvers are one of the success stories of Computer Science. An academic curiosity until the early 90s, SAT solvers now find an ever increasing range of applications. This tutorial is organized into the following main parts. The first part describes the organization of modern Conflict-Driven Clause Learning (CDCL) SAT solvers. The second part details standard techniques for encoding constraints into propositional logic. The third part highlights the use of SAT oracles for solving computationally more challenging problems. The fourth part delves into practical applications of SAT solvers, and highlights representative examples. The final part summarizes recent research trends in computing with SAT oracles.