Samuel R. Buss.
"Mini-tutorial on Proof Complexity"
Workshop on Theoretical Foundations of Applied SAT Solving.
BIRS, Banff, Canada.
January 20, 2014.
Download talk slides: PDF.
Abstract: This talk will survey propositional proof complexity. It will cover proof systems such as resolution, Frege systems, extended Frege systems, cutting planes, nullstellensatz and the polynomial calculus, with an emphasis on how they apply to SAT solvers or may possibly point the way to new algorithms for satisfiability. The talk will also discuss upper and lower bounds. It will discuss Craig interpolation, which has proved to be important both for lower bounds on propositional proofs and for applied SMT solvers. It will also discuss automatizability, i.e., the complexity of proof search.
Back to Sam Buss's publications page.