**Time-space tradeoffs for width-parameterized SAT**
Periklis A. Papakonstantinou

*29 June 2012, 14h30 - 29 June 2012, 15h30*
Salle/Bat : 445/PCRI-N

Contact :

**Activités de recherche : **
**Résumé :**
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 scalled analogs).

That is, ignoring constants in the exponent,

if you pay a logn in the exponent then

you can bring the space down to polynomial, but other than this

there is nothing else you can do.

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).

*Pour en savoir plus : *