<h1>FPT results</h1>

<p>The complexity of SAT, #SAT and MaxSAT parametrized by primal and incidence treewidth is FPT for all cases and of the form <span class="math-container">$2^{ck}\|F\|^d$</span> where <span class="math-container">$\|F\|=\sum_{C \in F} |var(C)|$</span> is the size of a reasonable encoding of a CNF <span class="math-container">$F$</span>, <span class="math-container">$k$</span> is the (primal/incidence) treewidth and <span class="math-container">$c$</span> and <span class="math-container">$d$</span> are constants.</p>

<p>In this answer, I will denote by SAT(ptw) the problem SAT parametrized by primal treewidth. Same notations for #SAT(ptw), MaxSAT(ptw) and SAT(itw) for incidence treewidth. </p>

<p>For SAT(ptw), it is hard to pinpoint the exact first reference as their are many works going in this direction and proving similar results without being exactly stated this way. I would thus point to [1] where Alekhnovich and Razborov proves that SAT parametrized by branch-width is FPT. They also observe that branch-width is similar to treewidth up to a constant factor. I also advice to read the introduction of this paper to have a good overview of the previous literature on similar results.</p>

<p>For SAT(itw) and #SAT(itw), it is a consequence of Courcelle's Theorem that was first observed in [4], but, as observed by Szeider in [2], the hidden constants may be very high. For #SAT(ptw), an observation that exhaustive DPLL would run in FPT time with reasonable constant has been made in [3] by Bacchus, Shannon and Pitassi but without formally proving this. Explicit algorithms with better complexity bounds are given by Szeider and Samer in [5] for #SAT(itw) and #SAT(ptw). </p>

<p>For MaxSAT(ptw) and MaxSAT(itw), I do not know any reference doing it directly. I suspect the community to be aware of the fact that easy modifications in the algorithm for #SAT and thus too straightforward to be published anywhere. An notable exception is, that appeared much later, [6] where Sæther, Telle and Vatshelle give an algorithm for MaxSAT(ps-width), a parameter more general than treewidth. They also observe that it is roughly the same algorithm for #SAT and weighted MaxSAT. </p>

<p>All algorithms mentioned above can also be transformed into algorithms for weighted versions of our problems. One uniform way of seeing this is through the spectrum of Knowledge Compilation. Basically, what you can observe it that all these algorithms are implicitly rewriting, in FPT time, the CNF formula into a very restricted Boolean circuit (known in the literature of knowledge compilation as d-DNNF) computing the same Boolean function, see [7] where it is proven for a very general parameter. The catch is that many problems are tractable on this new representation such as (weighted) model counting, enumeration or finding a model with minimal Hamming weight, etc. Thus, everything that is ptime on d-DNNF becomes FPT on bounded treewidth CNF for free: change the representation in FPT time and solve it on the new circuit (that is also of FPT size). </p>

<p>This encompasses SAT, #SAT, weighted #SAT and also MaxSAT by working a bit more. Indeed, changing the representation of an UNSAT formula is quite easy: just output the 0 circuit. So it will not help you. However, compiling <span class="math-container">$F' = \bigwedge_{C \in F} s_C \vee C$</span> where you add in each clause of <span class="math-container">$F$</span> a fresh selector variable <span class="math-container">$s_C$</span> is more interesting. <span class="math-container">$F'$</span> has the same treewidth as <span class="math-container">$F$</span> (+ constant) and is of course satisfiable (set <span class="math-container">$s_C=1$</span> for every <span class="math-container">$C$</span>). Now, solving MaxSAT(<span class="math-container">$F$</span>) is equivalent to finding the solution of <span class="math-container">$F'$</span> setting the smallest number of <span class="math-container">$s_C$</span> to <span class="math-container">$1$</span>, something that can be done in polynomial time for d-DNNF. A proof of this can be found in my thesis, Section 3.2.2 [8].</p>

<h1>Best complexity</h1>

<p>In [5], the complexity bounds are given very explicitly. For #SAT(ptw) (and thus for SAT(ptw) as well), the complexity is <span class="math-container">$O(2^{k}kNd)$</span> where <span class="math-container">$N$</span> is the number of variables and <span class="math-container">$d$</span> is the maximal number of occurrence of a variable in the formula. Not that <span class="math-container">$Nd$</span> may not be linear in <span class="math-container">$\|F\|$</span> but is very close from it. A linear time (in the formula size) compilation algorithm can be found in the appendix of [9] which gives also a linear time algorithm for SAT, #SAT, maxSAT etc. The complexity is of the form <span class="math-container">$O(2^{ck}\|F\|)$</span> but the exact value of <span class="math-container">$c$</span> is not discussed here as it was not really necessary in this paper. I would say that a thorough analysis would give <span class="math-container">$c=1$</span> but I have not checked it carefully.</p>

<p>For SAT(itw), [5] gives a complexity of <span class="math-container">$O(2^k k (l+2^k) \|F\|)$</span> where <span class="math-container">$l$</span> is the size of the longest clause of <span class="math-container">$F$</span>. If one wants linear time in <span class="math-container">$\|F\|$</span>, one can rewrite <span class="math-container">$F$</span> as an equivalent 3-CNF without changing its incidence treewidth as shown by Lampel, Mengel and Mitsou in [10], which thus gives an equivalent 3-CNF which thus has primal treewidth at most <span class="math-container">$3k$</span> and now use the algorithm for primal treewith but it would spoil the constant in the exponent. </p>

<p>These are the best <em>explicitly</em> stated/known complexity upper bounds. I would not be surprised if they can still be improved, especially going from <span class="math-container">$4^k$</span> to <span class="math-container">$2^{k+O(1)}$</span> for incidence treewidth. This can be explained by the fact that these results are mostly interesting in theory where the precise constant is not important and the work to get it down is not really worth it. Friedrich Slivovsky mentioned in personal communication that there may be some algebraic trick in the algorithm of [5] for itw to get a better complexity bound but as far as I know, it has never been written formally.</p>

<h1>References</h1>

<p>[1] M.Alekhnovich and A.A.Razborov, Satisability, branch-width and Tseitin tautologies. In 43rd Annual IEEE Symposiumon Foundations of ComputerScience (FOCS'02)</p>

<p>[2] On fixed-parameter tractable parameterizations of SAT, Stefan Szeider, Theory and Applications of Satisfiability, 6th International Conference, SAT 2003</p>

<p>[3] Bacchus, Fahiem, Shannon Dalmao, and Toniann Pitassi. "Solving #SAT and Bayesian inference with backtracking search." Journal of Artificial Intelligence Research 34 (2009).</p>

<p>[4] Courcelle, Bruno, Johann A. Makowsky, and Udi Rotics. "On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic." Discrete Applied Mathematics 108.1-2 (2001).</p>

<p>[5] Samer, Marko, and Stefan Szeider. "Algorithms for propositional model counting." Journal of Discrete Algorithms 8.1 (2010): 50-64.</p>

<p>[6] Sæther, Sigve Hortemo, Jan Arne Telle, and Martin Vatshelle. "Solving# SAT and MAXSAT by dynamic programming." Journal of Artificial Intelligence Research 54 (2015): 59-82.</p>

<p>[7] Bova, Simone, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky. "On compiling CNFs into structured deterministic DNNFs." In International Conference on Theory and Applications of Satisfiability Testing, pp. 199-214. Springer, Cham, 2015.</p>

<p>[8] Structural restriction of CNF-formulas: application to model counting and knowledge compilation, Thèse de Doctorat, 2016. </p>

<p>[9] Capelli, Florent, and Stefan Mengel. "Knowledge compilation, width and quantification." arXiv preprint <a href="https://arxiv.org/abs/1807.04263" rel="noreferrer">arXiv:1807.04263</a> (2018).</p>

<p>[10] Lampis, Michael, Stefan Mengel, and Valia Mitsou. "QBF as an Alternative to Courcelle’s Theorem." International Conference on Theory and Applications of Satisfiability Testing. Springer, Cham, 2018.</p>

CC BY-SA 4.0
2019-10-09T22:24:23.387Z
Thanks for the very thorough answer. I find it surprising that there has been not
 much interest in finding the precise constants because that kind of results could be strongly connected to the strong exponential time hypothesis (SETH).
Laakeri
CC BY-SA 4.0
2019-10-09T22:07:33.937Z
2019-10-09T22:07:33.937Z
holf
<p>Many papers state that Boolean satisfiability is in FPT when parameterized by primal, dual, or incidence treewidth. What are the best known time complexities of these parameterized algorithms? In particular, I would expect something like <span class="math-container">$O(2^{tw} nm)$</span> time complexity for at least primal treewidth, but I cannot find a reference for it.</p>

<p>Also, how about (weighted) Max-SAT and #SAT?</p>

CC BY-SA 4.0
2019-10-07T05:49:23.340Z
A good survey is *On Fixed-Parameter Tractable Parameterizations of SAT* by S. Szeider. See also my recent answer where #SAT is also mentioned https://cstheory.stackexchange.com/questions/45579/on-theoretical-aproaches-for-solving-mathsfsat-in-special-cases. What are you *exactly* interested in? Can you be more precise as finding such references is very easy so I guess you had something else in mind.
holf
CC BY-SA 4.0
2019-10-07T08:20:36.727Z
I know that these problems can be solved in $O(c^{tw} (n+m)^d)$ for some constants $c$ and $d$. I'm interested in the best known constants $c$ and $d$ in these time complexities. None of the references in your answer nor the survey give algorithms with time complexity $O^*(2^{tw})$ for SAT parameterized by primal treewidth. They just state that there is an $O^*(c^{tw})$ algorithm for some constant $c$.
Laakeri
CC BY-SA 4.0
2019-10-07T08:34:42.840Z
Quickly (I will try to answer more precisely later): you have more precise bounds in *Algorithms for propositional model counting*, Marko Samer, Stefan Szeider. For #SAT as well (not too hard to see it works for maxSAT as well). It comes close from what you look for for primal tw. For incidence tw, it may be improved using some algebraic trick but I do not think it has been written down. You can also reduce this case to primal tw (see M. Lampis,  S. Mengel, V. Mitsou. QBF as an alternative to Courcelle’s theorem). See the appendix of https://arxiv.org/abs/1807.04263 for linear time.
holf
CC BY-SA 4.0
2019-10-07T08:57:51.217Z
Thank you. The paper _Algorithms for propositional model counting_ of Samer and Szeider gives satisfying answers for SAT and #SAT for primal, dual and incidence treewidth. I agree that for sure these algorithms should work for maxSAT as well, but of course it would be nice to see that written down somewhere. The reduction from incidence to primal treewidth increases the treewidth by a factor of 3, so it does not improve the before mentioned paper. (btw the correct arxiv link is [arxiv.org/abs/1805.08456](https://arxiv.org/abs/1805.08456))
Laakeri
CC BY-SA 4.0
2019-10-07T09:36:14.910Z
The last arxiv link was a separate reference. It is proven in the appendix that you can be linear in the formula size (not optimized in the exponent). For maxSAT, you can use knowledge compilation approaches to get it directly: compile $F' = \bigwedge_{C \in F} s_C \vee C$ to a FPT-size d-DNNF where $s_C$ is a fresh selector variable (it does not increase tw by much). Now you only have to find the assignment with maximal $s_C$ set to $0$ which is linear on d-DNNF. For compilation, see On compiling CNFs into structured deterministic DNNFs
S Bova, F Capelli, S Mengel, F Slivovsky.
holf
CC BY-SA 4.0
2019-10-07T20:13:57.503Z
@holf since you are answering at least some of the questions, please consider turning your really informed comments into an answer!
Hermann Gruber
CC BY-SA 4.0
2019-10-07T20:43:53.230Z
I will, later this week, I do not have much time to write a proper and thorough answer.
holf
<sat><treewidth><fixed-parameter-tractable>
Complexity of SAT parameterized by treewidth
Laakeri
# Complexity of SAT parameterized by treewidth

(Asked by: username_0 on 2019-10-06)

Many papers state that Boolean satisfiability is in FPT when parameterized by primal, dual, or incidence treewidth. What are the best known time complexities of these parameterized algorithms? In particular, I would expect something like $O(2^{tw} nm)$ time complexity for at least primal treewidth, but I cannot find a reference for it.

Also, how about (weighted) Max-SAT and #SAT?

**Tags:** sat, treewidth, fixed-parameter-tractable

> **Comments:**
> **username_1**: A good survey is *On Fixed-Parameter Tractable Parameterizations of SAT* by S. Szeider. See also my recent answer where #SAT is also mentioned https://cstheory.stackexchange.com/questions/45579/on-theoretical-aproaches-for-solving-mathsfsat-in-special-cases. What are you *exactly* interested in? Can you be more precise as finding such references is very easy so I guess you had something else in mind.  
> **username_0**: I know that these problems can be solved in $O(c^{tw} (n+m)^d)$ for some constants $c$ and $d$. I'm interested in the best known constants $c$ and $d$ in these time complexities. None of the references in your answer nor the survey give algorithms with time complexity $O^*(2^{tw})$ for SAT parameterized by primal treewidth. They just state that there is an $O^*(c^{tw})$ algorithm for some constant $c$.  
> **username_1**: Quickly (I will try to answer more precisely later): you have more precise bounds in *Algorithms for propositional model counting*, Marko Samer, Stefan Szeider. For #SAT as well (not too hard to see it works for maxSAT as well). It comes close from what you look for for primal tw. For incidence tw, it may be improved using some algebraic trick but I do not think it has been written down. You can also reduce this case to primal tw (see M. Lampis,  S. Mengel, V. Mitsou. QBF as an alternative to Courcelle’s theorem). See the appendix of https://arxiv.org/abs/1807.04263 for linear time.  
> **username_0**: Thank you. The paper _Algorithms for propositional model counting_ of Samer and Szeider gives satisfying answers for SAT and #SAT for primal, dual and incidence treewidth. I agree that for sure these algorithms should work for maxSAT as well, but of course it would be nice to see that written down somewhere. The reduction from incidence to primal treewidth increases the treewidth by a factor of 3, so it does not improve the before mentioned paper. (btw the correct arxiv link is [arxiv.org/abs/1805.08456](https://arxiv.org/abs/1805.08456))  
> **username_1**: The last arxiv link was a separate reference. It is proven in the appendix that you can be linear in the formula size (not optimized in the exponent). For maxSAT, you can use knowledge compilation approaches to get it directly: compile $F' = \bigwedge_{C \in F} s_C \vee C$ to a FPT-size d-DNNF where $s_C$ is a fresh selector variable (it does not increase tw by much). Now you only have to find the assignment with maximal $s_C$ set to $0$ which is linear on d-DNNF. For compilation, see On compiling CNFs into structured deterministic DNNFs S Bova, F Capelli, S Mengel, F Slivovsky.  
> **username_2**: @username_1 since you are answering at least some of the questions, please consider turning your really informed comments into an answer!  
> **username_1**: I will, later this week, I do not have much time to write a proper and thorough answer.  

---

## 1 answers

### Answer by username_1 on 2019-10-09. Score: 7 | Accepted answer

# FPT results

The complexity of SAT, #SAT and MaxSAT parametrized by primal and incidence treewidth is FPT for all cases and of the form $2^{ck}\|F\|^d$ where $\|F\|=\sum\_{C \in F} |var(C)|$ is the size of a reasonable encoding of a CNF $F$, $k$ is the (primal/incidence) treewidth and $c$ and $d$ are constants.

In this answer, I will denote by SAT(ptw) the problem SAT parametrized by primal treewidth. Same notations for #SAT(ptw), MaxSAT(ptw) and SAT(itw) for incidence treewidth.

For SAT(ptw), it is hard to pinpoint the exact first reference as their are many works going in this direction and proving similar results without being exactly stated this way. I would thus point to [1] where Alekhnovich and Razborov proves that SAT parametrized by branch-width is FPT. They also observe that branch-width is similar to treewidth up to a constant factor. I also advice to read the introduction of this paper to have a good overview of the previous literature on similar results.

For SAT(itw) and #SAT(itw), it is a consequence of Courcelle's Theorem that was first observed in [4], but, as observed by Szeider in [2], the hidden constants may be very high. For #SAT(ptw), an observation that exhaustive DPLL would run in FPT time with reasonable constant has been made in [3] by Bacchus, Shannon and Pitassi but without formally proving this. Explicit algorithms with better complexity bounds are given by Szeider and Samer in [5] for #SAT(itw) and #SAT(ptw).

For MaxSAT(ptw) and MaxSAT(itw), I do not know any reference doing it directly. I suspect the community to be aware of the fact that easy modifications in the algorithm for #SAT and thus too straightforward to be published anywhere. An notable exception is, that appeared much later, [6] where Sæther, Telle and Vatshelle give an algorithm for MaxSAT(ps-width), a parameter more general than treewidth. They also observe that it is roughly the same algorithm for #SAT and weighted MaxSAT.

All algorithms mentioned above can also be transformed into algorithms for weighted versions of our problems. One uniform way of seeing this is through the spectrum of Knowledge Compilation. Basically, what you can observe it that all these algorithms are implicitly rewriting, in FPT time, the CNF formula into a very restricted Boolean circuit (known in the literature of knowledge compilation as d-DNNF) computing the same Boolean function, see [7] where it is proven for a very general parameter. The catch is that many problems are tractable on this new representation such as (weighted) model counting, enumeration or finding a model with minimal Hamming weight, etc. Thus, everything that is ptime on d-DNNF becomes FPT on bounded treewidth CNF for free: change the representation in FPT time and solve it on the new circuit (that is also of FPT size).

This encompasses SAT, #SAT, weighted #SAT and also MaxSAT by working a bit more. Indeed, changing the representation of an UNSAT formula is quite easy: just output the 0 circuit. So it will not help you. However, compiling $F' = \bigwedge\_{C \in F} s\_C \vee C$ where you add in each clause of $F$ a fresh selector variable $s\_C$ is more interesting. $F'$ has the same treewidth as $F$ (+ constant) and is of course satisfiable (set $s\_C=1$ for every $C$). Now, solving MaxSAT($F$) is equivalent to finding the solution of $F'$ setting the smallest number of $s\_C$ to $1$, something that can be done in polynomial time for d-DNNF. A proof of this can be found in my thesis, Section 3.2.2 [8].

# Best complexity

In [5], the complexity bounds are given very explicitly. For #SAT(ptw) (and thus for SAT(ptw) as well), the complexity is $O(2^{k}kNd)$ where $N$ is the number of variables and $d$ is the maximal number of occurrence of a variable in the formula. Not that $Nd$ may not be linear in $\|F\|$ but is very close from it. A linear time (in the formula size) compilation algorithm can be found in the appendix of [9] which gives also a linear time algorithm for SAT, #SAT, maxSAT etc. The complexity is of the form $O(2^{ck}\|F\|)$ but the exact value of $c$ is not discussed here as it was not really necessary in this paper. I would say that a thorough analysis would give $c=1$ but I have not checked it carefully.

For SAT(itw), [5] gives a complexity of $O(2^k k (l+2^k) \|F\|)$ where $l$ is the size of the longest clause of $F$. If one wants linear time in $\|F\|$, one can rewrite $F$ as an equivalent 3-CNF without changing its incidence treewidth as shown by Lampel, Mengel and Mitsou in [10], which thus gives an equivalent 3-CNF which thus has primal treewidth at most $3k$ and now use the algorithm for primal treewith but it would spoil the constant in the exponent.

These are the best *explicitly* stated/known complexity upper bounds. I would not be surprised if they can still be improved, especially going from $4^k$ to $2^{k+O(1)}$ for incidence treewidth. This can be explained by the fact that these results are mostly interesting in theory where the precise constant is not important and the work to get it down is not really worth it. Friedrich Slivovsky mentioned in personal communication that there may be some algebraic trick in the algorithm of [5] for itw to get a better complexity bound but as far as I know, it has never been written formally.

# References

[1] M.Alekhnovich and A.A.Razborov, Satisability, branch-width and Tseitin tautologies. In 43rd Annual IEEE Symposiumon Foundations of ComputerScience (FOCS'02)

[2] On fixed-parameter tractable parameterizations of SAT, Stefan Szeider, Theory and Applications of Satisfiability, 6th International Conference, SAT 2003

[3] Bacchus, Fahiem, Shannon Dalmao, and Toniann Pitassi. "Solving #SAT and Bayesian inference with backtracking search." Journal of Artificial Intelligence Research 34 (2009).

[4] Courcelle, Bruno, Johann A. Makowsky, and Udi Rotics. "On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic." Discrete Applied Mathematics 108.1-2 (2001).

[5] Samer, Marko, and Stefan Szeider. "Algorithms for propositional model counting." Journal of Discrete Algorithms 8.1 (2010): 50-64.

[6] Sæther, Sigve Hortemo, Jan Arne Telle, and Martin Vatshelle. "Solving# SAT and MAXSAT by dynamic programming." Journal of Artificial Intelligence Research 54 (2015): 59-82.

[7] Bova, Simone, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky. "On compiling CNFs into structured deterministic DNNFs." In International Conference on Theory and Applications of Satisfiability Testing, pp. 199-214. Springer, Cham, 2015.

[8] Structural restriction of CNF-formulas: application to model counting and knowledge compilation, Thèse de Doctorat, 2016.

[9] Capelli, Florent, and Stefan Mengel. "Knowledge compilation, width and quantification." arXiv preprint [arXiv:1807.04263](https://arxiv.org/abs/1807.04263) (2018).

[10] Lampis, Michael, Stefan Mengel, and Valia Mitsou. "QBF as an Alternative to Courcelle’s Theorem." International Conference on Theory and Applications of Satisfiability Testing. Springer, Cham, 2018.

> **Comments:**
> **username_0**: Thanks for the very thorough answer. I find it surprising that there has been not  much interest in finding the precise constants because that kind of results could be strongly connected to the strong exponential time hypothesis (SETH).  

---

