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?
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].
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.
[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 (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.
