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.... : Short proofs are narrow - resolution made simple. J. ACM 48 http://www.informatik.uni-trier.de/%7Eley/db/journals/jacm/jacm48.html#Ben-S... (2): 149-169 (2001) Resolution Space (3): Michael Alekhnovich http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/a/Alekhnovich:Mi... , Eli Ben-Sasson, Alexander A. Razborov http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/r/Razborov:Alexa... , Avi Wigderson http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wigderson:Avi.... : Space Complexity in Propositional Calculus. SIAM J. Comput. 31 <http://www.informatik.uni-trier.de/%7Eley/db/journals/siamcomp/siamcomp31.ht... hBRW02> (4): 1184-1211 (2002) Albert Atserias, Víctor Dalmau http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/d/Dalmau:V=iacut... : A combinatorial characterization of resolution width. J. Comput. Syst. Sci. 74 http://www.informatik.uni-trier.de/%7Eley/db/journals/jcss/jcss74.html#Atser... (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... : 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-S... : 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:Ru... : Random CNF's are Hard for the Polynomial Calculus. FOCS 1999 http://www.informatik.uni-trier.de/%7Eley/db/conf/focs/focs99.html#Ben-Sasso... : 415-421 Samuel R. Buss http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/b/Buss:Samuel_R=... , Dima Grigoriev http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/g/Grigoriev:Dima... , Russell Impagliazzo, Toniann Pitassi http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/p/Pitassi:Tonian... : 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#BussG... (2): 267-289 (2001) Russell Impagliazzo, Pavel Pudlák http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/p/Pudl=aacute=k:... , Jiri Sgall http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/s/Sgall:Jiri.htm... : 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#Impagliazz... (2): 127-144 (1999) Matthew Clegg http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/c/Clegg:Matthew.... , Jeff Edmonds http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/e/Edmonds:Jeff.h... , 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#CleggEI... : 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+Satisfia... 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_... , Armin Biere, Richard Raimi http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/r/Raimi:Richard.... , Yunshan Zhu http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/z/Zhu:Yunshan.ht... : Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design 19 http://www.informatik.uni-trier.de/%7Eley/db/journals/fmsd/fmsd19.html#Clark... (1): 7-34 (2001)
