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

Abstract

Under the Strong Exponential Time Hypothesis (SETH), for any constant $\varepsilon > 0$, the #SAT problem (counting the number of satisfying assignments of a CNF formula) cannot be solved in $\mathcal{O}^*((2-\varepsilon)^n)$ or $\mathcal{O}^*((2-\varepsilon)^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}^*(2^n)$-time and $\mathcal{O}^*(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}^*(2^{m(1-1/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}^*(2^{mω/3})$, where $ω< 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}^*((2-\varepsilon)^m)$-time algorithm for any constant $\varepsilon>0$, even on positive formulas, under the hypothesis that #Max-3-SAT on $n$ variables admits no $\mathcal{O}^*((2-\varepsilon)^n)$-time algorithm for any such $\varepsilon$.