<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:st1="urn:schemas-microsoft-com:office:smarttags" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv=Content-Type content="text/html; charset=us-ascii">
<meta name=Generator content="Microsoft Word 11 (filtered medium)">
<o:SmartTagType namespaceuri="urn:schemas-microsoft-com:office:smarttags"
name="PlaceName"/>
<o:SmartTagType namespaceuri="urn:schemas-microsoft-com:office:smarttags"
name="PlaceType"/>
<o:SmartTagType namespaceuri="urn:schemas-microsoft-com:office:smarttags"
name="place"/>
<!--[if !mso]>
<style>
st1\:*{behavior:url(#default#ieooui) }
</style>
<![endif]-->
<style>
<!--
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Times New Roman";}
a:link, span.MsoHyperlink
{color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{color:purple;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal;
font-family:Arial;
color:windowtext;}
span.EmailStyle18
{mso-style-type:personal-reply;
font-family:Arial;
color:navy;}
@page Section1
{size:8.5in 11.0in;
margin:1.0in 1.25in 1.0in 1.25in;}
div.Section1
{page:Section1;}
-->
</style>
</head>
<body lang=EN-US link=blue vlink=purple>
<div class=Section1>
<p class=MsoNormal><font size=3 face=Arial><span style='font-size:12.0pt;
font-family:Arial'>When:
Tue, Mar 11,
2008 @ 2:00 <font color=navy><span style='color:navy'>p</span></font>m<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=3 face=Arial><span style='font-size:12.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=3 face=Arial><span style='font-size:12.0pt;
font-family:Arial'>Where:
TTI-C Conference Room<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=3 face=Arial><span style='font-size:12.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=3 face=Arial><span style='font-size:12.0pt;
font-family:Arial'>Who:
Ryan
Williams, <st1:place w:st="on"><st1:PlaceName w:st="on">Carnegie</st1:PlaceName>
<st1:PlaceName w:st="on">Mellon</st1:PlaceName> <st1:PlaceType w:st="on">University</st1:PlaceType></st1:place>
<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=3 face=Arial><span style='font-size:12.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal style='text-autospace:none'><font size=3 face=Arial><span
style='font-size:12.0pt;font-family:Arial'>Topic:
Applying
Practice to Theory: Time Lower Bounds for Fundamental Problems<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=3 face=Arial><span style='font-size:12.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal style='text-autospace:none'><font size=3 face=Arial><span
style='font-size:12.0pt;font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal style='text-autospace:none'><font size=3 face=Arial><span
style='font-size:12.0pt;font-family:Arial'>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.<o:p></o:p></span></font></p>
<p class=MsoNormal style='text-autospace:none'><font size=3 face=Arial><span
style='font-size:12.0pt;font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal style='text-autospace:none'><font size=3 face=Arial><span
style='font-size:12.0pt;font-family:Arial'>I will survey some of my work in
this area, with an emphasis on simplicity. 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, I will demonstrate how the
search for better lower bounds can often be turned into a problem of solving a
large series of linear programming instances. This mathematical work has in
turn led to a new methodology for proving time lower bounds, where prospective
lower-bounders formulate their proof rules, write programs to generate optimal
short proofs, then study the empirical results and extrapolate new proofs on
paper.<o:p></o:p></span></font></p>
<p class=MsoNormal style='text-autospace:none'><font size=3 face=Arial><span
style='font-size:12.0pt;font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal style='text-autospace:none'><font size=3 face=Arial><span
style='font-size:12.0pt;font-family:Arial'>In some settings, our programs
provide strong evidence that the best known lower bound proofs are already
optimal for the current framework, contradicting the consensus intuition; in
other settings, we are guided to improved lower bounds where no further
progress had been made for some time.<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=3 color=navy face=Arial><span style='font-size:
12.0pt;font-family:Arial;color:navy'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=3 face=Arial><span style='font-size:12.0pt;
font-family:Arial'>Contact:
Lance Fortnow fortnow@eecs.northwestern.edu
834-9873<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=3 color=navy face=Arial><span style='font-size:
12.0pt;font-family:Arial;color:navy'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
</div>
</body>
</html>