Proof Complexity and Complexity of SAT Solvers

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.

Sam Buss, University of California, San Diego, USA

Sam Buss is a professor of mathematics and computer science at the University of California, San Diego. He earned his Ph.D. in Mathematics in
1985 from Princeton, was the Mathematical Sciences Research Institute for 1985-1986, and the Department of Mathematics at UC Berkeley during
1986-1988. He has been at UC San Diego since 1988. His research concerns mathematical logic and theoretical computer science, especially proof
theory, bounded arithmetic, computational complexity and proof complexity. He is the author of a book on bounded arithmetic and a book on computer
graphics, and the editor of the handbook in proof theory. His current research also includes work on a SAT solver, SatDiego.