Title: Applying Practice to Theory: Time-Space Lower Bounds for SAT
Speaker: Ryan Williams, IAS
Date: Wednesday, November 5, 2008 11:00-12:00pm
Location: DIMACS Center, CoRE Bldg, Room 431, Rutgers University, Busch Campus, Piscataway, NJ
A fertile area of recent research has demonstrated concrete polynomial time lower bounds for solving natural hard problems on restricted computational models. Among these problems are Satisfiability, Vertex Cover, Hamilton Path, MOD6-SAT, Majority-of-Majority-SAT, and Tautologies, to name a few. These lower bound proofs all follow a certain diagonalization-based proof-by-contradiction strategy. A pressing open problem has been to determine how powerful such proofs can possibly be.
I will survey some of my work in this area. After a brief overview of the proof techniques used, I will propose an automated search strategy for studying the limits of these proof techniques. In particular, the search for better lower bounds can often be turned into a problem of solving a large series of linear programming instances. This work suggests a new methodology for proving time lower bounds, where prospective lower-bounders can formulate their proof rules, write programs to generate optimal short proofs, then study the empirical results and extrapolate new proofs on paper.