A Survey of Lower Bounds for the Resolution Proof System

Computer Science/Discrete Mathematics Seminar II
Topic:A Survey of Lower Bounds for the Resolution Proof System
Speaker:Avi Wigderson
Affiliation:Herbert H. Maass Professor, School of Mathematics
Date:Tuesday, January 31
Time/Room:10:30am - 12:30pm/S-101

The Resolution proof system is among the most basic and popular for proving propositional tautologies, and underlies many of the automated theorem proving systems in use today. I'll start by defining the Resolution system, and its place in the proof-complexity picture. A large body of work, starting in the 1960s, aimed to prove that some tautologies (represented as a disjunctive normal form formulae on n Boolean variables) require exp(n) size Resolution proofs. I will describe two different methods to prove such lower bounds and illustrate how to use them to get such exponential lower bounds on natural tautologies, such as the Pigeonhole Principle and the fact that no k-colorable graph can have a (k+1) clique. No special background will be assumed.