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$.

Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.