Algorithms break exponential clause count barrier for counting solutions
Solving Restricted Versions of #SAT Faster than $2^m$: Algorithms and Lower Bounds
Data Structures and Algorithms
Summary
Counting the number of ways to satisfy a logical formula (#SAT) is a fundamental problem in computer science with known limits on how fast it can be solved. The authors show new algorithms that can count solutions faster than the usual methods for certain restricted kinds of formulas: those with clauses of limited size and those where each variable appears a limited number of times. They also show that for some cases, no significantly faster algorithm likely exists, based on existing complexity hypotheses. These findings help us better understand when and how counting solutions can be done more efficiently.
What this means in practice
- •For algorithm engineers: Design faster counting algorithms for formulas with small clauses or limited variable occurrences using the presented methods to improve performance beyond standard bounds.
- •For graph algorithm developers: Implement improved algorithms for counting edge covers in graphs derived from #2-occurrence SAT instances to speed up combinatorial analysis tasks.
A theory result. No direct application yet.
Authors
Sanjay Jain, Junqiang Peng, Frank Stephan, Mingyu Xiao
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$.