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.