<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:x="urn:schemas-microsoft-com:office:excel" xmlns:p="urn:schemas-microsoft-com:office:powerpoint" xmlns:a="urn:schemas-microsoft-com:office:access" xmlns:dt="uuid:C2F41010-65B3-11d1-A29F-00AA00C14882" xmlns:s="uuid:BDC6E3F0-6DA3-11d1-A2A3-00AA00C14882" xmlns:rs="urn:schemas-microsoft-com:rowset" xmlns:z="#RowsetSchema" xmlns:b="urn:schemas-microsoft-com:office:publisher" xmlns:ss="urn:schemas-microsoft-com:office:spreadsheet" xmlns:c="urn:schemas-microsoft-com:office:component:spreadsheet" xmlns:odc="urn:schemas-microsoft-com:office:odc" xmlns:oa="urn:schemas-microsoft-com:office:activation" xmlns:html="http://www.w3.org/TR/REC-html40" xmlns:q="http://schemas.xmlsoap.org/soap/envelope/" xmlns:rtc="http://microsoft.com/officenet/conferencing" xmlns:D="DAV:" xmlns:Repl="http://schemas.microsoft.com/repl/" xmlns:mt="http://schemas.microsoft.com/sharepoint/soap/meetings/" xmlns:x2="http://schemas.microsoft.com/office/excel/2003/xml" xmlns:ppda="http://www.passport.com/NameSpace.xsd" xmlns:ois="http://schemas.microsoft.com/sharepoint/soap/ois/" xmlns:dir="http://schemas.microsoft.com/sharepoint/soap/directory/" xmlns:ds="http://www.w3.org/2000/09/xmldsig#" xmlns:dsp="http://schemas.microsoft.com/sharepoint/dsp" xmlns:udc="http://schemas.microsoft.com/data/udc" xmlns:xsd="http://www.w3.org/2001/XMLSchema" xmlns:sub="http://schemas.microsoft.com/sharepoint/soap/2002/1/alerts/" xmlns:ec="http://www.w3.org/2001/04/xmlenc#" xmlns:sp="http://schemas.microsoft.com/sharepoint/" xmlns:sps="http://schemas.microsoft.com/sharepoint/soap/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:udcs="http://schemas.microsoft.com/data/udc/soap" xmlns:udcxf="http://schemas.microsoft.com/data/udc/xmlfile" xmlns:udcp2p="http://schemas.microsoft.com/data/udc/parttopart" xmlns:wf="http://schemas.microsoft.com/sharepoint/soap/workflow/" xmlns:dsss="http://schemas.microsoft.com/office/2006/digsig-setup" xmlns:dssi="http://schemas.microsoft.com/office/2006/digsig" xmlns:mdssi="http://schemas.openxmlformats.org/package/2006/digital-signature" xmlns:mver="http://schemas.openxmlformats.org/markup-compatibility/2006" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns:mrels="http://schemas.openxmlformats.org/package/2006/relationships" xmlns:spwp="http://microsoft.com/sharepoint/webpartpages" xmlns:ex12t="http://schemas.microsoft.com/exchange/services/2006/types" xmlns:ex12m="http://schemas.microsoft.com/exchange/services/2006/messages" xmlns:pptsl="http://schemas.microsoft.com/sharepoint/soap/SlideLibrary/" xmlns:spsl="http://microsoft.com/webservices/SharePointPortalServer/PublishedLinksService" xmlns:Z="urn:schemas-microsoft-com:" xmlns:st="" xmlns="http://www.w3.org/TR/REC-html40"><head><meta http-equiv=Content-Type content="text/html; charset=iso-8859-1"><meta name=Generator content="Microsoft Word 12 (filtered medium)"><!--[if !mso]><style>v\:* {behavior:url(#default#VML);}
o\:* {behavior:url(#default#VML);}
w\:* {behavior:url(#default#VML);}
.shape {behavior:url(#default#VML);}
</style><![endif]--><style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Times New Roman","serif";}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
p.MsoPlainText, li.MsoPlainText, div.MsoPlainText
{mso-style-priority:99;
mso-style-link:"Plain Text Char";
margin:0in;
margin-bottom:.0001pt;
font-size:9.0pt;
font-family:"Arial","sans-serif";}
span.EmailStyle18
{mso-style-type:personal-reply;
font-family:"Arial","sans-serif";
color:blue;
font-weight:normal;
font-style:normal;
text-decoration:none none;}
span.PlainTextChar
{mso-style-name:"Plain Text Char";
mso-style-priority:99;
mso-style-link:"Plain Text";
font-family:"Arial","sans-serif";}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]--></head><body lang=EN-US link=blue vlink=purple><div class=WordSection1><p class=MsoNormal><span style='font-size:9.0pt;font-family:"Arial","sans-serif";color:blue'>Chris Beck will present his research seminar/general exam on Monday April 25 at 11AM in room 401 (note room).<o:p></o:p></span></p><p class=MsoNormal><span style='font-size:9.0pt;font-family:"Arial","sans-serif";color:blue'>The members of his committee are: Sanjeev Arora (advisor), Bernard Chazelle, and Moses Charikar. Everyone is <o:p></o:p></span></p><p class=MsoNormal><span style='font-size:9.0pt;font-family:"Arial","sans-serif";color:blue'>invited to attend his talk and those faculty wishing to remain for the oral exam following are welcome to do so. His <o:p></o:p></span></p><p class=MsoNormal><span style='font-size:9.0pt;font-family:"Arial","sans-serif";color:blue'>abstract and reading list follow below.<o:p></o:p></span></p><p class=MsoNormal><span style='font-size:9.0pt;font-family:"Arial","sans-serif";color:blue'>---------------------------------<o:p></o:p></span></p><p class=MsoPlainText>Abstract:<o:p></o:p></p><p class=MsoPlainText><o:p> </o:p></p><p class=MsoPlainText>For modern SAT solvers based on DPLL with clause learning, the two major bottlenecks are the time and memory used by the algorithm. There is a well known correspondence between these algorithms and the Resolution proof system, in which these resources correspond to the length and space of proofs. Lately there has been great theoretical interest in understanding the interplay of these two resources, and in obtaining Time Space Tradeoff results. In 2010, Eli Ben-Sasson and Jakob Nordström demonstrated formulae which have linear sized proofs using linear space, but which require exponentially large proofs when the space is constrained to be n / log n. It remains a major open question to obtain similar lower bounds against time but with a more mild space assumption, since in practice SAT solvers generally are not used on instances so large that they exceed the available memory.<o:p></o:p></p><p class=MsoPlainText><o:p> </o:p></p><p class=MsoPlainText>We obtain strong tradeoff results for Regular Resolution, a restricted form of General Resolution. For each k, we can find formulae of length n which may be proved in time n^(k+1) with space n^k, but such that with space at most n^(k - epsilon), superpolynomial time is necessary in any proof. Our analysis relies on a random adversary related to those used in Prover Adversary games, normally thought to be relevant only to very weak proof systems. This innovation permits a comparatively simple lower bound argument, avoiding completely the use of random restrictions.<o:p></o:p></p><p class=MsoNormal><span style='font-size:9.0pt;font-family:"Arial","sans-serif";color:blue'><o:p> </o:p></span></p><p class=MsoNormal style='margin-bottom:12.0pt'><span style='font-size:9.0pt;font-family:"Arial","sans-serif";color:blue'>Reading List:</span><span style='font-size:9.0pt;font-family:"Arial","sans-serif"'><br>Resolution (1): <br>Eli Ben-Sasson, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wigderson:Avi.html" target="_blank">Avi Wigderson</a>: Short proofs are narrow - resolution made simple. <a href="http://www.informatik.uni-trier.de/%7Eley/db/journals/jacm/jacm48.html#Ben-SassonW01" target="_blank">J. ACM 48</a>(2): 149-169 (2001)<br><br>Resolution Space (3):<br><a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/a/Alekhnovich:Michael.html" target="_blank">Michael Alekhnovich</a>, Eli Ben-Sasson, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/r/Razborov:Alexander_A=.html" target="_blank">Alexander A. Razborov</a>, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wigderson:Avi.html" target="_blank">Avi Wigderson</a>: Space Complexity in Propositional Calculus. <a href="http://www.informatik.uni-trier.de/%7Eley/db/journals/siamcomp/siamcomp31.html#AlekhnovichBRW02" target="_blank">SIAM J. Comput. 31</a>(4): 1184-1211 (2002) <br>Albert Atserias, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/d/Dalmau:V=iacute=ctor.html" target="_blank">Víctor Dalmau</a>: A combinatorial characterization of resolution width. <a href="http://www.informatik.uni-trier.de/%7Eley/db/journals/jcss/jcss74.html#AtseriasD08" target="_blank">J. Comput. Syst. Sci. 74</a>(3): 323-334 (2008)<br>Eli Ben-Sasson, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/n/Nordstr=ouml=m:Jakob.html" target="_blank">Jakob Nordström</a>: Understanding Space in Resolution: Optimal Lower Bounds and Exponential Trade-offs. <a href="http://www.informatik.uni-trier.de/%7Eley/db/journals/eccc/eccc16.html#Ben-SassonN09a" target="_blank">Electronic Colloquium on Computational Complexity (ECCC) 16</a>: 34 (2009)<br><br>Polynomial Calculus (4):<br><a href="http://dblp.uni-trier.de/rec/bibtex/conf/focs/Ben-SassonI99.xml" target="_blank"><span style='border:solid windowtext 1.0pt;padding:0in;text-decoration:none'><img border=0 width=16 height=16 id="_x0000_i1025" src="cid:image001.jpg@01CBFF78.A3034510" alt="Image removed by sender. bibliographical record in XML"></span></a>Eli Ben-Sasson, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/i/Impagliazzo:Russell.html" target="_blank">Russell Impagliazzo</a>: Random CNF's are Hard for the Polynomial Calculus. <a href="http://www.informatik.uni-trier.de/%7Eley/db/conf/focs/focs99.html#Ben-SassonI99" target="_blank">FOCS 1999</a>: 415-421 <br><a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/b/Buss:Samuel_R=.html" target="_blank">Samuel R. Buss</a>, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/g/Grigoriev:Dima.html" target="_blank">Dima Grigoriev</a>, Russell Impagliazzo, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/p/Pitassi:Toniann.html" target="_blank">Toniann Pitassi</a>: Linear Gaps between Degrees for the Polynomial Calculus Modulo Distinct Primes. <a href="http://www.informatik.uni-trier.de/%7Eley/db/journals/jcss/jcss62.html#BussGIP01" target="_blank">J. Comput. Syst. Sci. 62</a>(2): 267-289 (2001)<br>Russell Impagliazzo, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/p/Pudl=aacute=k:Pavel.html" target="_blank">Pavel Pudlák</a>, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/s/Sgall:Jiri.html" target="_blank">Jiri Sgall</a>: Lower Bounds for the Polynomial Calculus and the Gröbner Basis Algorithm. <a href="http://www.informatik.uni-trier.de/%7Eley/db/journals/cc/cc8.html#ImpagliazzoPS99" target="_blank">Computational Complexity 8</a>(2): 127-144 (1999)<br><a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/c/Clegg:Matthew.html" target="_blank">Matthew Clegg</a>, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/e/Edmonds:Jeff.html" target="_blank">Jeff Edmonds</a>, Russell Impagliazzo: Using the Groebner Basis Algorithm to Find Proofs of Unsatisfiability. <a href="http://www.informatik.uni-trier.de/%7Eley/db/conf/stoc/stoc1996.html#CleggEI96" target="_blank">STOC 1996</a>: 174-183<br><br>AC^0-Frege (2):<br>Paul Beame and Søren Riis. <a href="http://www.cs.washington.edu/homes/beame/papers/riis.ps" target="_blank">More on the relative strength of counting principles</a>. In Paul W. Beame and Samuel R. Buss, editors, <cite><span style='font-family:"Arial","sans-serif"'>Proof Complexity and Feasible Arithmetics</span></cite>, volume 39 of <cite><span style='font-family:"Arial","sans-serif"'>DIMACS Series in Discrete Mathematics and Theoretical Computer Science</span></cite>, pages 13-35. American Mathematical Society, 1998.<br>Also related:<br>Paul Beame. <a href="http://www.cs.washington.edu/homes/beame/papers/primer.ps" target="_blank">A switching lemma primer</a>. Technical Report UW-CSE-95-07-01, Department of Computer Science and Engineering, University of Washington, November 1994.<br><br>SAT solvers & Model Checking (1):<br>Lintao Zhang, Conor F. Madigan, Matthew H. Moskewicz, Sharad Malik, "Efficient Conflict Driven Learning in a Boolean Satisfiability Solver," iccad, pp.279, 2001 International Conference on Computer-Aided Design (ICCAD '01), 2001<br><br>Verification/Model Checking(1):<br><a href="http://scholar.google.com/scholar?q=%22Bounded+Model+Checking+Using+Satisfiability+Solving.%22" target="_blank"><span style='border:solid windowtext 1.0pt;padding:0in;text-decoration:none'><img border=0 width=16 height=16 id="_x0000_i1026" src="cid:image001.jpg@01CBFF78.A3034510" alt="Image removed by sender. Google scholar"></span></a><a href="http://dblp.uni-trier.de/rec/bibtex/journals/fmsd/ClarkeBRZ01" target="_blank"><span style='border:solid windowtext 1.0pt;padding:0in;text-decoration:none'><img border=0 width=16 height=16 id="_x0000_i1027" src="cid:image001.jpg@01CBFF78.A3034510" alt="Image removed by sender. BibTeX"></span></a><a href="http://dblp.uni-trier.de/rec/bibtex/journals/fmsd/ClarkeBRZ01.xml" target="_blank"><span style='border:solid windowtext 1.0pt;padding:0in;text-decoration:none'><img border=0 width=16 height=16 id="_x0000_i1028" src="cid:image001.jpg@01CBFF78.A3034510" alt="Image removed by sender. bibliographical record in XML"></span></a><a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/c/Clarke:Edmund_M=.html" target="_blank">Edmund M. Clarke</a>, Armin Biere, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/r/Raimi:Richard.html" target="_blank">Richard Raimi</a>, <a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/z/Zhu:Yunshan.html" target="_blank">Yunshan Zhu</a>: Bounded Model Checking Using Satisfiability Solving. <a href="http://www.informatik.uni-trier.de/%7Eley/db/journals/fmsd/fmsd19.html#ClarkeBRZ01" target="_blank">Formal Methods in System Design 19</a>(1): 7-34 (2001)<br><br><br><o:p></o:p></span></p><p class=MsoNormal><o:p> </o:p></p></div></body></html>