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: Short proofs are narrow - resolution made simple. J. ACM 48(2): 149-169 (2001)

Resolution Space (3):
Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, Avi Wigderson: Space Complexity in Propositional Calculus. SIAM J. Comput. 31(4): 1184-1211 (2002)  
Albert Atserias, Víctor Dalmau: A combinatorial characterization of resolution width. J. Comput. Syst. Sci. 74(3): 323-334 (2008)
Eli Ben-Sasson, Jakob Nordström: Understanding Space in Resolution: Optimal Lower Bounds and Exponential Trade-offs. Electronic Colloquium on Computational Complexity (ECCC) 16: 34 (2009)

Polynomial Calculus (4):
Image removed by sender. bibliographical record in XMLEli Ben-Sasson, Russell Impagliazzo: Random CNF's are Hard for the Polynomial Calculus. FOCS 1999: 415-421
Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo, Toniann Pitassi: Linear Gaps between Degrees for the Polynomial Calculus Modulo Distinct Primes. J. Comput. Syst. Sci. 62(2): 267-289 (2001)
Russell Impagliazzo, Pavel Pudlák, Jiri Sgall: Lower Bounds for the Polynomial Calculus and the Gröbner Basis Algorithm. Computational Complexity 8(2): 127-144 (1999)
Matthew Clegg, Jeff Edmonds, Russell Impagliazzo: Using the Groebner Basis Algorithm to Find Proofs of Unsatisfiability. STOC 1996: 174-183

AC^0-Frege (2):
Paul Beame and Søren Riis. More on the relative strength of counting principles. 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. 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):
Image removed by sender. Google scholarImage removed by sender. BibTeXImage removed by sender. bibliographical record in XMLEdmund M. Clarke, Armin Biere, Richard Raimi, Yunshan Zhu: Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design 19(1): 7-34 (2001)