  Width parameterizations of SAT, such as tree-width and path-width, enable the
study of computationally more tractable and practical SAT instances. We give
two simple algorithms. One that runs simultaneously in time-space
$(O^*(2^{2tw(\phi)}), O^*(2^{tw(\phi)}))$ and another that runs in time-space
$(O^*(3^{tw(\phi)\log{|\phi|}}),|\phi|^{O(1)})$, where $tw(\phi)$ is the
tree-width of a formula $\phi$ with $|\phi|$ many clauses and variables. This
partially answers the question of Alekhnovitch and Razborov, who also gave
algorithms exponential both in time and space, and asked whether the space can
be made smaller. We conjecture that every algorithm for this problem that runs
in time $2^{tw(\phi)\mathbf{o(\log{|\phi|})}}$ necessarily blows up the space
to exponential in $tw(\phi)$.
  We introduce a novel way to combine the two simple algorithms that allows us
to trade \emph{constant} factors in the exponents between running time and
space. Our technique gives rise to a family of algorithms controlled by two
parameters. By fixing one parameter we obtain an algorithm that runs in
time-space $(O^*(3^{1.441(1-\epsilon)tw(\phi)\log{|\phi|}}), O^*(2^{2\epsilon
tw(\phi)}))$, for every $0<\epsilon<1$. We systematically study the limitations
of this technique, and show that these algorithmic results are the best
achievable using this technique.
  We also study further the computational complexity of width parameterizations
of SAT. We prove non-sparsification lower bounds for formulas of path-width
$\omega(\log|\phi|)$, and a separation between the complexity of path-width and
tree-width parametrized SAT modulo plausible complexity assumptions.
