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