Width-parameterized SAT: time-space tradeoffs

Title: Width-parameterized SAT: time-space tradeoffs
Speaker: Periklis A. Papakonstantinou (Institute for Theoretical Computer Science, Tsinghua University)
Time: 3:00pm, March 8th (Thursday), 2012.
Venue: Lecture room, 3rd Floor, Building No. 5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Abstract: SAT, short for satisfiability, is probably the most decorated NP-hard problem, and it has attracted a lot of interest both in theory and in real-world practice. Empirical studies show that: first, state-of-the-art SAT-solvers abort due to lack of space; and second, real-world instances often times come with structure. A popular way to quantify such structure is through width parameters, such as treewidth and pathwidth on graphs related to the given formula. We initiate a systematic study of time-space tradeoffs for solving SAT parameterized by pathwidth and treewidth.

Ten years have passed since Alekhnovitch and Razborov [AR02] gave algorithms for parameterized SAT that run in time and in space exponential in tw(phi), for an input formula phi. In their main open question they ask if one can “do anything intelligent in polynomial space to check satisfiability of formulas” with small tree-width. We give positive and negative results regarding this question. If one believes a popular computational complexity assumption then we asymptotically have settled the problem as follows:.

1. We give a simple algorithm that works in time 3^{tw(phi) * logn} and in space poly(n). This does not answer the question of [AR02] due to the multiplicative logn factor in the exponent. Can we get rid of this logn factor without blowing up the space to exponential? We conjecture that this is not possible. Furthermore, we prove that, perhaps surprisingly, this conjecture is equivalent to a popular conjecture is complexity (and its scaled analogs). This follows as a corollary of a systematic complexity theoretic study associating the SAT-parameterized computation with questions in complexity.

2. Our conjecture asserts that it is impossible to improve the exponent assymptotically. So if true, for all practical purposes it makes sense to trade-constants in the exponent. This is the most technical part of our work, where we show that in fact for every epsilon>0 there is an algorithm that runs in time-space (3^{1.441*epsilon*tw(phi)*logn}  ,  2^{2*epislon*tw(phi)} ).

In this talk I shall explain the connections to complexity (that’s not too technical), and I’ll sketch the family of algorithms, including a new algorithmic technique that we devise on the way (and which we also push to its extremes by showing that our results are optimal modulo this technique).

If time permits, I’ll outline some exciting new connections and directions of our work to propositional proof complexity (the first step has already been taken by Beame-Beck-Impagliazzo 2012).

Joint work with: Eric Allender, Shiteng Chen, Bangsheng Tang

Biography:
Periklis research interests are in cryptography, theoretical computer science (at large), and other areas of mathematics (in particular, representations of locally compact groups).  Since March 2010, he is an assistant professor with the Institute for Theoretical Computer Science, Tsinghua University. Right before that he was a graduate student in the University of Toronto where he obtained a PhD in Computer Science under the supervision of Charles Rackoff, simultaneously to this an MSc in Mathematics, and even before that an MSc in Computer Science. Prior to studying at the University of Toronto he obtained an undergraduate degree in Computer Engineering and Science from the University of Patras, Greece, and he’s a licensed Electronics Engineer with the Technical Chamber of Greece. He holds several academic honors, distinctions, and awards.