Solving Restricted Versions of #SAT Faster than $2^m$: Algorithms and Lower Bounds

Under the Strong Exponential Time Hypothesis (SETH), for any constant $\epsilon >0$, the #SAT problem (counting the number of satisfying assignments of a CNF formula) cannot be solved in ${\mathcal{O}}^{\ast }((2-\epsilon {)}^n)$ or ${\mathcal{O}}^{\ast }((2-\epsilon {)}^m)$ time, where $n$ is the number of variables and $m$ is the number of clauses. On the other hand, simple exhaustive search and the standard inclusion-exclusion give ${\mathcal{O}}^{\ast }(2^n)$-time and ${\mathcal{O}}^{\ast }(2^m)$-time algorithms, respectively. A natural line of research is to beat these SETH-based barriers for restricted versions, such as #$k$-SAT (where each clause contains at most $k$ literals) or #$d$-occ-SAT (where each variable appears in at most $d$ clauses). It is known that the $2^n$-barrier can be broken when $k$ or $d$ is any constant; yet, whether the $2^m$-barrier can also be broken in these cases remains unknown. We present two simple algorithms that overcome the $2^m$-barrier. First, for #$k$-SAT, we give an ${\mathcal{O}}^{\ast }(2^{m(1-1\mathrm{/}O(k))})$-time algorithm, thereby breaking the $2^m$-barrier for any constant $k$. Second, for #$2$-occ-SAT (which also includes the problem of counting the number of edge covers in a graph as a special case), we provide an algorithm with runtime ${\mathcal{O}}^{\ast }(2^{m\omega \mathrm{/}3})$, where $\omega <2.3714$ is the matrix multiplication exponent. Furthermore, we demonstrate that both algorithms generalize to the weighted counting setting while preserving the same runtime bounds. On the hardness side, we present a reduction from #Max-$d$-SAT to #$d$-occ-SAT, showing that for any $d\ge 3$, #$d$-occ-SAT admits no ${\mathcal{O}}^{\ast }((2-\epsilon {)}^m)$-time algorithm for any constant $\epsilon >0$, even on positive formulas, under the hypothesis that #Max-3-SAT on $n$ variables admits no ${\mathcal{O}}^{\ast }((2-\epsilon {)}^n)$-time algorithm for any such $\epsilon$.