[talks] C Beck general exam

Wed Apr 20 16:33:20 EDT 2011

Chris Beck will present his research seminar/general exam on Monday April 25 at 11AM in
room 401 (note room).

The members of his committee are:  Sanjeev Arora (advisor), Bernard Chazelle, and Moses
Charikar.  Everyone is 

invited to attend his talk and those faculty wishing to remain for the oral exam following
are welcome to do so.  His 

abstract and reading list follow below.

---------------------------------

Abstract:

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.

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.

Reading List:
Resolution (1):  
Eli Ben-Sasson, Avi Wigderson
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wigderson:Avi.html> : Short
proofs are narrow - resolution made simple. J. ACM 48
<http://www.informatik.uni-trier.de/%7Eley/db/journals/jacm/jacm48.html#Ben-SassonW01>
(2): 149-169 (2001)

Resolution Space (3):
Michael Alekhnovich
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/a/Alekhnovich:Michael.html> ,
Eli Ben-Sasson, Alexander A. Razborov
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/r/Razborov:Alexander_A=.html>
, Avi Wigderson
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wigderson:Avi.html> : Space
Complexity in Propositional Calculus. SIAM J. Comput. 31
<http://www.informatik.uni-trier.de/%7Eley/db/journals/siamcomp/siamcomp31.html#Alekhnovic
hBRW02> (4): 1184-1211 (2002)   
Albert Atserias, Víctor Dalmau
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/d/Dalmau:V=iacute=ctor.html>
: A combinatorial characterization of resolution width. J. Comput. Syst. Sci. 74
<http://www.informatik.uni-trier.de/%7Eley/db/journals/jcss/jcss74.html#AtseriasD08> (3):
323-334 (2008)
Eli Ben-Sasson, Jakob Nordström
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/n/Nordstr=ouml=m:Jakob.html>
: Understanding Space in Resolution: Optimal Lower Bounds and Exponential Trade-offs.
Electronic Colloquium on Computational Complexity (ECCC) 16
<http://www.informatik.uni-trier.de/%7Eley/db/journals/eccc/eccc16.html#Ben-SassonN09a> :
34 (2009)

Polynomial Calculus (4):
 <http://dblp.uni-trier.de/rec/bibtex/conf/focs/Ben-SassonI99.xml> Image removed by
sender. bibliographical record in XMLEli Ben-Sasson, Russell Impagliazzo
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/i/Impagliazzo:Russell.html> :
Random CNF's are Hard for the Polynomial Calculus. FOCS 1999
<http://www.informatik.uni-trier.de/%7Eley/db/conf/focs/focs99.html#Ben-SassonI99> :
415-421 
Samuel R. Buss
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/b/Buss:Samuel_R=.html> , Dima
Grigoriev
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/g/Grigoriev:Dima.html> ,
Russell Impagliazzo, Toniann Pitassi
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/p/Pitassi:Toniann.html> :
Linear Gaps between Degrees for the Polynomial Calculus Modulo Distinct Primes. J. Comput.
Syst. Sci. 62
<http://www.informatik.uni-trier.de/%7Eley/db/journals/jcss/jcss62.html#BussGIP01> (2):
267-289 (2001)
Russell Impagliazzo, Pavel Pudlák
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/p/Pudl=aacute=k:Pavel.html> ,
Jiri Sgall <http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/s/Sgall:Jiri.html>
: Lower Bounds for the Polynomial Calculus and the Gröbner Basis Algorithm. Computational
Complexity 8
<http://www.informatik.uni-trier.de/%7Eley/db/journals/cc/cc8.html#ImpagliazzoPS99> (2):
127-144 (1999)
Matthew Clegg
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/c/Clegg:Matthew.html> , Jeff
Edmonds <http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/e/Edmonds:Jeff.html>
, Russell Impagliazzo: Using the Groebner Basis Algorithm to Find Proofs of
Unsatisfiability. STOC 1996
<http://www.informatik.uni-trier.de/%7Eley/db/conf/stoc/stoc1996.html#CleggEI96> : 174-183

AC^0-Frege (2):
Paul Beame and Søren Riis. More on the relative strength of counting principles
<http://www.cs.washington.edu/homes/beame/papers/riis.ps> . In Paul W. Beame and Samuel R.
Buss, editors, Proof Complexity and Feasible Arithmetics, volume 39 of DIMACS Series in
Discrete Mathematics and Theoretical Computer Science, pages 13-35. American Mathematical
Society, 1998.
Also related:
Paul Beame. A switching lemma primer
<http://www.cs.washington.edu/homes/beame/papers/primer.ps> . Technical Report
UW-CSE-95-07-01, Department of Computer Science and Engineering, University of Washington,
November 1994.

SAT solvers & Model Checking (1):
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

Verification/Model Checking(1):

<http://scholar.google.com/scholar?q=%22Bounded+Model+Checking+Using+Satisfiability+Solvin
g.%22> Image removed by sender. Google scholar
<http://dblp.uni-trier.de/rec/bibtex/journals/fmsd/ClarkeBRZ01> Image removed by sender.
BibTeX <http://dblp.uni-trier.de/rec/bibtex/journals/fmsd/ClarkeBRZ01.xml> Image removed
by sender. bibliographical record in XMLEdmund M. Clarke
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/c/Clarke:Edmund_M=.html> ,
Armin Biere, Richard Raimi
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/r/Raimi:Richard.html> ,
Yunshan Zhu
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/z/Zhu:Yunshan.html> : Bounded
Model Checking Using Satisfiability Solving. Formal Methods in System Design 19
<http://www.informatik.uni-trier.de/%7Eley/db/journals/fmsd/fmsd19.html#ClarkeBRZ01> (1):
7-34 (2001)

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.cs.princeton.edu/pipermail/talks/attachments/20110420/a1a93695/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: image/jpeg
Size: 335 bytes
Desc: not available
URL: <http://lists.cs.princeton.edu/pipermail/talks/attachments/20110420/a1a93695/attachment.jpe>