Talk by Periklis Papakonstantinou, Tsinghua University

Host:  Anne Condon

Contact:  Kerry Neil, Secretary to the Head (headsec@cs.ubc.ca)

Title:  Time-space tradeoffs for width-parameterized SAT

Abstract:

SAT, short for satisfiability, is probably the most decorated and applicable NP-hard problem. Empirical studies show that: (i) state-of-the-art SAT solvers abort mainly due to lack of memory, and (ii) real-life SAT instances come with structure. We systematically study time-space tradeoffs for solving SAT, parameterized by path-width & tree-width; two popular ways to quantify how much structured is the input instance.

In particular, we (conditionally) resolve the main open question of Alekhnovitch and Razborov (2002) which has as follows:

"Is it possible to solve SAT of treewidth w(n) simultaneously in time-space(poly(n) 2^O(w), poly(n))?"

We show that in the incidence graph there is a simple algorithm running in time-space (poly(n) 2^O(w*logn), poly(n)). We furthermore, show that removing this logn factor from the time exponent incurs an exponential blow up in the space unless NC \subseteq SC (or its scaled analogs). That is, if one cares about asymptotic improvements in the exponent of the running time and space, then (i) by paying an additional logn factor in the exponent of the 2^w running time then you can bring the space down to polynomial, but (ii) other than this there is nothing else you can do to achieve polynomial space.

Finally, we devise algorithms showing that it is possible to trade constants in the exponent between time and space.

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

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