[Colloquium] Theory Seminar at Computer Science

[Donna Brooms]

    ~REMINDER~

COMPUTER SCIENCE

The University of Chicago

THEORY SEMINAR

_______________________

Date:	Tuesday, November 29, 2011

Time:	3 p.m.

Place:	Ryerson 251

________________________

Speaker:	Christopher Beck

From:	Princeton University

Title:	Time-Space Tradeoffs in Resolution: Superpolynomial Lower Bounds for
Superlinear Space

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. Much recent research in proof complexity
has focused on understanding this memory bottleneck -- is it inherent
to the Resolution based approach, or is it an artifact of the search
heuristics used in practice? The most direct approach to this question
would be to try to prove unconditional space lower bounds for proofs
of some particular formula, but this approach is limited by the
observation that every formula has a trivial proof which may be
carried out in space no larger than the size of the formula. The catch
is that this proof is exponentially large in general, so a natural
next step is to try to show that for some formula, such a penalty must
be incurred when the space is thus constrained. This is formalized by
a tradeoff result -- in high space, there is a short proof, but with
constrained space only much longer proofs exist.

We obtain strong time space tradeoff lower bounds for a simple and
explicit collection of formulas -- in particular for any k, we give a
sequence of formulas of length n such that with n^k space there is a
proof of length polynomial in n, but for which every proof is
superpolynomial when the space is constrained to n^{k/2}. Thus, on
these instances, if you want to run in polynomial time, you need a
large polynomial amount of space. Previous research has only been able
to obtain tradeoffs when the space is sublinear. This is the first
result that has allowed us to distinguish the efficiency of e.g.
Resolution with linear space versus quadratic space.

_____________________________________________________
*Refreshments will be served prior to the talk at 2:30 in Ryerson 255*
Persons who need assistance should call 773-702-6614


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20111129/563f338d/attachment.htm