Theory of Computing
-------------------
Title : Width-Parametrized SAT: Time--Space Tradeoffs
Authors : Eric Allender, Shiteng Chen, Tiancheng Lou, Periklis A. Papakonstantinou, and Bangsheng Tang
Volume : 10
Number : 12
Pages : 297-339
URL : https://theoryofcomputing.org/articles/v010a012
Abstract
--------
Alekhnovich and Razborov (2002) presented an algorithm that solves SAT
on instances $\phi$ of size $n$ and tree-width $\tw(\phi)$, using time
and space bounded by $2^{O(\tw(\phi))}n^{O(1)}$. Although several
follow-up works appeared over the last decade, the first open question
of Alekhnovich and Razborov remained essentially unresolved: Can one
check satisfiability of formulas with small tree-width in polynomial
space and time as above? We essentially resolve this question, by
(1) giving a polynomial space algorithm with a slightly worse run-time,
(2) providing a complexity-theoretic characterization of bounded
tree-width SAT, which strongly suggests that no polynomial-space
algorithm can run significantly faster, and (3) presenting a spectrum
of algorithms trading off time for space, between our PSPACE algorithm
and the fastest known algorithm.
First, we give a simple algorithm that runs in polynomial space and achieves
run-time $3^{\tw(\phi)\log n}n^{O(1)}$, which approaches the run-time of
Alekhnovich and Razborov (2002), but has an additional $\log n$ factor
in the exponent. Then, we conjecture that this annoying $\log n$ factor
is in general unavoidable.
Our negative results show our conjecture true if one believes a well-known
complexity assumption, which is the SC \neq NC conjecture and its scaled
variants. Technically, we base our result on the following lemma. For
arbitrary $k$, SAT of tree-width $\log^k n$ is complete for the class of
problems computed by circuits of logarithmic depth, semi-unbounded fan-in
and size $2^{O(\log^k n)}$ (SAC^1 when $k=1$).
Problems in this class can be solved simultaneously in
time-space $(2^{O(\log^{k+1}n)}, O(\log^{k+1}n))$,
and also in ($2^{O(\log^k n)}$, $2^{O(\log^k n)}$).
Then, we show that our conjecture (for SAT instances with
poly-log tree-width) is equivalent to the question of whether
the small-space simulation of semi-unbounded circuit classes
can be sped up without incurring a large space penalty. This is
a recasting of the conjecture that SAC^1
(and even its subclass NL) is not contained in SC.
Although we cannot hope for an improvement asymptotically in the
exponent of time and space, we introduce a new algorithmic
technique which trades constants in the exponents:
for each $\epsilon$ with $0 < \epsilon <1$, we give an algorithm
in time-space
(3^{1.441(1-\epsilon)\tw(\phi)\log{|\phi|}}|\phi|^{O(1)},
2^{2\epsilon\tw(\phi)}|\phi|^{O(1)})
We systematically study the limitations of our technique for
trading off time and space, and we show that our bounds are the
best achievable using this technique.