A Survey of Proof Complexity from a SAT Solving Perspective
Jakob Nordström, KTH
Date and Time
Wednesday, November 11th, 2015 at 13:15.
Polacksbacken, room 1145
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. It is still quite poorly understood when and how such solvers work, however.
Proof complexity studies formal methods for reasoning about Boolean formulas, and provides one of the few tools available for theoretical analysis of SAT solver performance. This talk is intended as a selective survey of proof complexity, focusing on proof systems that are of particular interest in the context of SAT solving. We will review resolution, polynomial calculus, and cutting planes (related to conflict-driven clause learning, Gröbner basis computations, and pseudo-Boolean solvers, respectively) and some proof complexity measures that have been studied for these proof systems. This will then allow us to discuss if and how these complexity measures could provide insights into the potential and limitations of current state-of-the-art SAT solvers.