Is bounded-width SAT decidable in logspace?

Question

Elberfeld, Jakoby, and Tantau 2010 (ECCC TR10-062) proved a space-efficient version of Bodlaender's theorem. They showed that for graphs with treewidth at most $k$, a tree decomposition of width $k$ can be found using logarithmic space. The constant factor in the space bound depends on $k$. (Bodlaender's theorem shows a linear time bound, with an exponential dependence on $k$ in the constant factor.)

SAT becomes easy when the set of clauses has low width. Specifically, Fischer, Makowsky, and Ravve 2008 showed that satisfiability of CNF formulas with treewidth of the incidence graph bounded by $k$ can be decided with at most $2^{O(k)} n$ arithmetic operations when the tree decomposition is given. By Bodlaender's theorem, computing the tree decomposition of the incidence graph for fixed $k$ can be done in linear time, and therefore SAT can be decided for bounded treewidth formulas in time that is a low-degree polynomial in the number of variables $n$.

One might then expect that SAT should actually be decidable using logarithmic space, for formulas with bounded treewidth of the incidence graph. It is not clear how to modify the Fischer et al. approach for deciding SAT into something space-efficient. The algorithm works by computing an expression for the number of solutions, via inclusion-exclusion, and recursively evaluating the number of solutions of smaller formulas. Although the bounded treewidth does help, the subformulas seem to be too large to compute in logarithmic space.

This leads me to ask:

Is SAT for bounded treewidth formulas known to be in $\mathsf{L}$ or $\mathsf{NL}$?

Answer 1

Indeed, using the resultss in Elberfeld-Jakoby-Tantau-2010 one can show that SAT can be decided in logspace on formulas whose incidence graph has bounded treewidth. Here is a sketch of how the main steps of the proof of this claim go.

1. The notions of tree-decomposition and treewidth can be generalized to arbitrary relational structures. See for instance sections 2 and 3 of this paper by Dalmau, Kolaitis and Vardi.
2. Courcelle's theorem states that MSO logic can be decided in linear time on relational structures of constant treewidth.
3. A theorem of Bodlaender implies that if a relational structure has treewidth $t$, then a tree-decomposition of such structure can be found in time $f(t)\cdot n$. In other words, such a decomposition can be found in linear time on graphs of constant treewidth.
4. One can define suitable relational structure $\tau$ which can be used to encode a formula $F$ together with its incidence graph $I$. The treewidth of $\tau$ is at most a constant plus the treewidth of $I$.
5. The set of relational structures $\tau$ which encode satisfiable formulas + their incidence graphs is MSO definable.
6. Therefore, by Bodlander+Courcelle's theorem, one can decide whether a formula of constant treewidth is satisfiable in linear time.
7. Elberfeld-Jakoby-Tantau-2010 show that "linear time" can be replaced by "logarithmic space" on both Bodlaender and Courcelle's theorem.
8. Therefore, for each MSO formula $\varphi$, and each relational structure $\tau$, one can determine in logarithmic space whether $\tau$ satisfied $\varphi$.
9. In particular, SAT can be determined in logspace on graphs of constant treewidth.