Talk slides.
Samuel R. Buss.
"Proof Complexity and the Complexity of SAT Solvers"
First International SAT/SMT Solver Workshop.
MIT, Boston.
June 17, 2011.
Download talk slides: PDF.
Abstract: This talk discusses the performance of a SAT solvers from the perpective of computational complexity and proof complexity. The first half of the talk discussed the "bad news" from the point of view of the hardness of nondeterministic polynomial time (NP) and complexity aspects of the hardness of proof search. The second half addresses the "good news" that DPLL solvers with clause learning are very efficient for many practical problems. We discuss the performance of the SatDiego solver on the pigeonhole principles. We discuss characterizations of DPLL with clause learning in terms of proof systems. We discuss the effectiveness of restarts.