Title: SAT Solvers & Proof Complexity

Speaker: Marco Carmosino, Hampshire College

Abstract:

A summary of recent work in proof complexity, with special attention
paid to the implications of that work for SAT solvers. We will
characterize familiar complexity classes in terms of proof complexity
and examine a series of different proof systems and how they relate to
each other. We will explain how proof complexity could be used to
seperate NP from coNP. Finally, we will see how modern techniques for
solving SAT fit into this landscape, and use proof complexity to
explain why CDCL (conflict driven clause learning) solvers have been
so successful.