Alekhnovich and Razborov 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-ups appeared over the last decade, the first open question of Alekhnovich & Razborov remained essentially unresolved: can one check satisfiability of formulas with small tree-width in polynomial space and time as above? We completely resolve this question, modulo complexity assumptions (the answer is negative), and we discover a threshold phenomenon.

First, we give a simple algorithm that runs in polynomial space and achieves run-time $3^{\tw(\phi)\log n}n^{O(1)}$, nearly matching the run-time of Alekhnovich & Razborov, but the $\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 $\eps$ with $0< \eps <1$, we give an algorithm in time-space $\big( 3^{1.441(1-\eps)\tw(\phi)\log{|\phi|}}|\phi|^{O(1)},\;$ $2^{2\eps\tw(\phi)}|\phi|^{O(1)} \big)$. We systematically study the limitations of our t\
echnique for trading off time and space, and we show that our bounds are the best achievable using this technique.

Improvements in the presentation; clarifying the proofs.

A decade has passed since Alekhnovich and Razborov presented an algorithm that solves SAT on instances $\phi$ of size $n$ having tree-width $TW(\phi)$, using time (and space) bounded by $2^{O(TW(\phi))}n^{O(1)}$. Although there have been several papers over the ensuing years building on the work of Alekhnovich and Razborov there has been no real progress on what they listed as their first open question: Can one ``do anything intelligent in polynomial space to check satisfiability of formulas'' with small tree-width?

We present both positive and negative results on this question; we present a fairly fast polynomial space algorithm, and present complexity-theoretic evidence that no significantly faster algorithm runs in polynomial space.

Our first positive result is a simple algorithm that runs in polynomial space and achieves run-time $3^{TW(\phi)\log{n}}n^{O(1)}$, nearly
matching the run-time of Aleknovich and Razborov, but with an annoying factor of $\log n$ in the exponent.

Our negative results indicate that this annoying factor of $\log n$ is unavoidable. For ease of exposition, let us focus on the case where the tree-width is $\log^k n$. Then, when $k=1$ we show that solving SAT instances of tree-width $\log n$ is complete for LOGCFL = SAC$^1$, and for arbitrary $k$, SAT of tree-width $\log^k n$ is complete for a level of the NSC hierarchy corresponding to log-depth semi-unbounded fan-in circuits of size $2^{O(\log^k n)}$. (NSC is the class of problems solvable in nondeterministic polynomial time and poly-logarithmic space: i.e., the nondeterministic analog of the well-known class SC.) Problems in this class can be solved in space $\log^{k+1}n$ (and hence in time $2^{O(\log^{k+1}n)}$), and also in time $2^{O(\log^k n)}$ (with space bound the same as the time bound).

These results show that our conjecture (that the annoying factor of $\log n$ in the exponent of the running time of our polynomial-space algorithm cannot be eliminated) 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, possibly with different resource bounds depending on $k$, of the long-standing conjecture in complexity theory that SAC$^1$ (and even its subclass NL) is not contained in SC, or even in the Time-Space class TISP$(n^{O(1)},2^{\log^{1-\epsilon} n})$.

The most involved part of this paper is the demonstration that the best-known time-efficient and space-efficient algorithms for small tree-width SAT can be combined using a new technique to obtain, for each $\epsilon$ with $0< \epsilon <1$, an algorithm with time-space complexity $\big( 3^{1.441(1-\epsilon)TW(\phi)\log{|\phi|}}|\phi|^{O(1)},\;$ $2^{2\epsilon TW(\phi)}|\phi|^{O(1)} \big)$. 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.

Corrected title

A decade has passed since Alekhnovich and Razborov presented an algorithm that solves SAT on instances $\phi$ of size $n$ having tree-width $TW(\phi)$, using time (and space) bounded by $2^{O(TW(\phi))}n^{O(1)}$. Although there have been several papers over the ensuing years building on the work of Alekhnovich and Razborov there has been no real progress on what they listed as their first open question: Can one ``do anything intelligent in polynomial space to check satisfiability of formulas'' with small tree-width?

We present both positive and negative results on this question; we present a fairly fast polynomial space algorithm, and present complexity-theoretic evidence that no significantly faster algorithm runs in polynomial space.

Our first positive result is a simple algorithm that runs in polynomial space and achieves run-time $3^{TW(\phi)\log{n}}n^{O(1)}$, nearly
matching the run-time of Aleknovich and Razborov, but with an annoying factor of $\log n$ in the exponent.

Our negative results indicate that this annoying factor of $\log n$ is unavoidable. For ease of exposition, let us focus on the case where the tree-width is $\log^k n$. Then, when $k=1$ we show that solving SAT instances of tree-width $\log n$ is complete for LOGCFL = SAC$^1$, and for arbitrary $k$, SAT of tree-width $\log^k n$ is complete for a level of the NSC hierarchy corresponding to log-depth semi-unbounded fan-in circuits of size $2^{O(\log^k n)}$. (NSC is the class of problems solvable in nondeterministic polynomial time and poly-logarithmic space: i.e., the nondeterministic analog of the well-known class SC.) Problems in this class can be solved in space $\log^{k+1}n$ (and hence in time $2^{O(\log^{k+1}n)}$), and also in time $2^{O(\log^k n)}$ (with space bound the same as the time bound).

These results show that our conjecture (that the annoying factor of $\log n$ in the exponent of the running time of our polynomial-space algorithm cannot be eliminated) 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, possibly with different resource bounds depending on $k$, of the long-standing conjecture in complexity theory that SAC$^1$ (and even its subclass NL) is not contained in SC, or even in the Time-Space class TISP$(n^{O(1)},2^{\log^{1-\epsilon} n})$.

The most involved part of this paper is the demonstration that the best-known time-efficient and space-efficient algorithms for small tree-width SAT can be combined using a new technique to obtain, for each $\epsilon$ with $0< \epsilon <1$, an algorithm with time-space complexity $\big( 3^{1.441(1-\epsilon)TW(\phi)\log{|\phi|}}|\phi|^{O(1)},\;$ $2^{2\epsilon TW(\phi)}|\phi|^{O(1)} \big)$. 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.