Jakob Nordström: Understanding conflict-driven SAT solving through the lens of proof complexity

PRACTICALITIES

Lunch is served at 12:00 noon (register at this doodle  at the latest the Saturday before, but preferably earlier). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for 1½-2 hours of more technical discussions.

ABSTRACT

Although determining satisfiability of Boolean formulas is an NP-complete problem, and is hence believed to require exponential time in the worst case, algorithmic developments over the last 15-20 years have led to so-called SAT solvers that successfully handle real-world formulas with millions of variables in a wide range of application areas. It is still quite poorly understood when and how such solvers work, however.

This talk will survey research on analyzing the power and limitations of state-of-the-art conflict-driven clause learning (CDCL) SAT solvers using tools from proof complexity. We will present some of the major results, but will also highlight many of the open problems that remain. Time permitting, we will also discuss how CDCL can be combined with geometric (pseudo-Boolean) techniques and what proof complexity can say about such extensions.