Matti Järvisalo: Modern SAT Solving: CDCL and Inprocessing

Boolean satisfiability (SAT) has become an attractive approach to solving hard decision and optimization problems arising from artificial intelligence, knowledge representation, and various industrially relevant domains. The success of the SAT-based approach relies heavily on the development of increasingly robust and efficient SAT solvers. This talk gives a two-part overview of the current state-of-the-art SAT solver technology based on the conflict-driven clause learning (CDCL) paradigm.
In the first part, I will provide a basic overview of the most important components of CDCL SAT solvers today. The second part of the talk concentrates on the important aspect of practical preprocessing for SAT and the inprocessing SAT solving paradigm in which more extensive reasoning is interleaved with the core satisfiability search (not only before search). I will review some of the most successful SAT preprocessing techniques, and give an overview of our recent work (joint work with Armin Biere and Marijn
Heule) on developing new reasoning techniques for pre- and inprocessing.

The seminar will be 2*45 minutes with a 15 minute break.