<p>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.</p>

<ol>
<li>The notions of tree-decomposition and treewidth can be generalized to arbitrary relational structures. See for instance sections 2 and 3 of 
<a href="https://link.springer.com/chapter/10.1007/3-540-46135-3_21" rel="noreferrer">this paper</a> by Dalmau, Kolaitis and Vardi.</li>
<li>Courcelle's theorem states that MSO logic can be decided in linear time on relational structures of constant treewidth. </li>
<li>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.</li>
<li>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$. </li>
<li>The set of relational structures $\tau$ which encode satisfiable formulas + their incidence graphs is MSO definable. </li>
<li>Therefore, by Bodlander+Courcelle's theorem, one can decide whether a formula of constant treewidth is satisfiable in linear time. </li>
<li>Elberfeld-Jakoby-Tantau-2010 show that "linear time" can be replaced by "logarithmic space" on both Bodlaender and Courcelle's theorem. </li>
<li>Therefore, for each MSO formula $\varphi$, and each relational structure $\tau$, one can determine in logarithmic space whether $\tau$ satisfied $\varphi$. </li>
<li>In particular, SAT can be determined in logspace on graphs of constant treewidth. </li>
</ol>

CC BY-SA 3.0
2017-03-29T00:49:50.850Z
2017-03-29T00:49:50.850Z
Mateus de Oliveira Oliveira
<p><a href="https://dx.doi.org/10.1109/FOCS.2010.21" rel="noreferrer">Elberfeld, Jakoby, and Tantau 2010</a> (<a href="https://eccc.weizmann.ac.il/report/2010/062/" rel="noreferrer">ECCC TR10-062</a>) 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.)</p>

<p>SAT becomes easy when the set of clauses has low width.
Specifically, <a href="https://dx.doi.org/10.1016/j.dam.2006.06.020" rel="noreferrer">Fischer, Makowsky, and Ravve 2008</a> 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$.</p>

<p>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.</p>

<p>This leads me to ask:</p>

<blockquote>
  <p>Is SAT for bounded treewidth formulas known to be in $\mathsf{L}$ or $\mathsf{NL}$?</p>
</blockquote>

CC BY-SA 3.0
2017-03-24T23:17:29.333Z
Doesn't the fact that SAT in L for bounded treewidth instances follow directly from the results in the paper you cited? The set of satisfiable formulas is MSO definable. Therefore, satisfiability can be solved in linear time on graphs of bounded treewidth via Bodlaender + Courcelle theorems. Elberfeld-Jakoby-Tantau-2010, show that MSO properties can be decided in logarithmic space on graphs of bounded treewidth by providing logarithmic space versions of Bodlaender + Courcelle's theorems. Therefore, SAT can be decided in logspace on graphs of bounded treewidth.
Mateus de Oliveira Oliveira
CC BY-SA 3.0
2017-03-27T13:33:09.650Z
@MateusdeOliveiraOliveira, the details don't seem clear to me.  SAT is MSO-definable via a structure with two directed edge relations (Immerman Example 2.18), the union of which leads to the edges of the incidence graph once the direction is forgotten.  However, it is not clear to me that it is possible to use the incidence graph as-is to MSO-define satisfiability (via set cover, for instance), so as to be able to apply Bodlaender/Courcelle/EJT.
András Salamon
CC BY-SA 3.0
2017-03-27T14:18:35.220Z
@AndrásSalomon Courcelle's theorem can be stated for graphs with colored vertices and edges. The treewidth of such colored graphs is the same as the treewidth of the uncolored versions. There are many ways of modeling arbitrary relational structures as colored graphs.
Mateus de Oliveira Oliveira
CC BY-SA 3.0
2017-03-27T14:21:55.350Z
In the case of Formulas you want to define a relational structure that encodes at the same time the formula and the incidence graph. (otherwise, how would you define satisfiability in first place? ) Then by using an appropriate notion of treewidth for such structure, we have that the treewidth of the structure (Formula + Incidence graph) is at most an additive constant bigger than the treewidth of the incidence graph alone. Note that there are many ways of defining such combined relational strucutres, and essentially each author uses the one that is most suitable for his/her context.
Mateus de Oliveira Oliveira
CC BY-SA 3.0
2017-03-28T08:42:51.683Z
@Mateus, thank you!  That is a rather helpful comment; I wasn't aware of the "toolbox" nature of treewidth in descriptive complexity.  Care to turn this into an answer?
András Salamon
CC BY-SA 3.0
2017-03-28T09:14:33.680Z
sorry for the delay in turning the comments into an answer. I'll try to do it today.
Mateus de Oliveira Oliveira
<cc.complexity-theory><sat><treewidth><space-complexity>
Is bounded-width SAT decidable in logspace?
András Salamon
# Is bounded-width SAT decidable in logspace?

(Asked by: username_0 on 2017-03-24)

[Elberfeld, Jakoby, and Tantau 2010](https://dx.doi.org/10.1109/FOCS.2010.21) ([ECCC TR10-062](https://eccc.weizmann.ac.il/report/2010/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](https://dx.doi.org/10.1016/j.dam.2006.06.020) 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}$?

**Tags:** cc.complexity-theory, sat, treewidth, space-complexity

> **Comments:**
> **username_1**: Doesn't the fact that SAT in L for bounded treewidth instances follow directly from the results in the paper you cited? The set of satisfiable formulas is MSO definable. Therefore, satisfiability can be solved in linear time on graphs of bounded treewidth via Bodlaender + Courcelle theorems. Elberfeld-Jakoby-Tantau-2010, show that MSO properties can be decided in logarithmic space on graphs of bounded treewidth by providing logarithmic space versions of Bodlaender + Courcelle's theorems. Therefore, SAT can be decided in logspace on graphs of bounded treewidth.  
> **username_0**: @MateusdeOliveiraOliveira, the details don't seem clear to me.  SAT is MSO-definable via a structure with two directed edge relations (Immerman Example 2.18), the union of which leads to the edges of the incidence graph once the direction is forgotten.  However, it is not clear to me that it is possible to use the incidence graph as-is to MSO-define satisfiability (via set cover, for instance), so as to be able to apply Bodlaender/Courcelle/EJT.  
> **username_1**: @AndrásSalomon Courcelle's theorem can be stated for graphs with colored vertices and edges. The treewidth of such colored graphs is the same as the treewidth of the uncolored versions. There are many ways of modeling arbitrary relational structures as colored graphs.  
> **username_1**: In the case of Formulas you want to define a relational structure that encodes at the same time the formula and the incidence graph. (otherwise, how would you define satisfiability in first place? ) Then by using an appropriate notion of treewidth for such structure, we have that the treewidth of the structure (Formula + Incidence graph) is at most an additive constant bigger than the treewidth of the incidence graph alone. Note that there are many ways of defining such combined relational strucutres, and essentially each author uses the one that is most suitable for his/her context.  
> **username_0**: @Mateus, thank you!  That is a rather helpful comment; I wasn't aware of the "toolbox" nature of treewidth in descriptive complexity.  Care to turn this into an answer?  
> **username_1**: sorry for the delay in turning the comments into an answer. I'll try to do it today.  

---

## 1 answers

### Answer by username_1 on 2017-03-29. Score: 10 | Accepted answer

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](https://link.springer.com/chapter/10.1007/3-540-46135-3_21) 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.


---

