### DIMACS Theoretical Computer Science Seminar

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

Abstract:

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.