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}$?

  • 5
    $\begingroup$ 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. $\endgroup$ – Mateus de Oliveira Oliveira Mar 24 '17 at 23:17
  • $\begingroup$ @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. $\endgroup$ – András Salamon Mar 27 '17 at 13:33
  • $\begingroup$ @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. $\endgroup$ – Mateus de Oliveira Oliveira Mar 27 '17 at 14:18
  • 1
    $\begingroup$ 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. $\endgroup$ – Mateus de Oliveira Oliveira Mar 27 '17 at 14:21
  • $\begingroup$ @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? $\endgroup$ – András Salamon Mar 28 '17 at 8:42

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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.