A Graphical #SAT Algorithm for Formulae with Small Clause Density
Tuomas Laakkonen, Konstantinos Meichanetzidis, John van de Wetering
TL;DR
This work uses the ZH-calculus, a graphical language originally developed for quantum circuits, to derive improved upper bounds for #SAT that are independent of maximum clause size. By expressing #SAT as ZH-diagrams and reducing to a weighted variant #2SAT_ pm, the authors obtain a time bound of $O^*(1.2377^{n + m_{\geq 3}})$, with a clause-density threshold $\delta < 2.2503$ for beating brute force. They also achieve an $O^*(1.1740^L)$ bound in terms of the total number of literals and provide refined results for #3SAT at specific densities, alongside a method to bound quantum circuit amplitudes in terms of gate count. The work demonstrates that graphical reasoning can yield new, nontrivial algorithmic insights for counting problems and related quantum-classical tasks, and it suggests several avenues for future refinement and application to other domains.
Abstract
We study the counting version of the Boolean satisfiability problem #SAT using the ZH-calculus, a graphical language originally introduced to reason about quantum circuits. Using this, we generalize #SAT to a weighted variant we call #SAT+-, which is complete for the class GapP. We show there is an efficient linear-time reduction from #SAT to #2SAT+-, unlike previous reductions from #SAT to #2SAT which blow up the size of the formula by a polynomial factor. Our main conceptual contribution is that introducing weights to #SAT allows for more efficient translations, and we use this to remove the dependence on clause width k in this case. We observe that DPLL-style algorithms for #2SAT can be adapted to #2SAT+- directly and hence the best-known upper bounds for #2SAT apply. Applying an upper bound for #2SAT in terms of variables gives us upper bounds for #SAT in terms of clauses and variables that are better than O*(2^n) for small clause densities of m/n < 2.25, and improve on previous average-case and worst-case bounds for k >= 6 and k >= 4, respectively. Applying a similar bound in terms of clauses produces a bound of O*(1.1740^L) in terms of the length of the formula. These are, to our knowledge, the first non-trivial upper bounds for #SAT that is independent of clause size, and in terms of formula length, respectively. Based on a result of Kutzkov, we find an improved bound on #3SAT for 1.2577 < m/n <= 7/3. Finally, we use this technique to find an upper bound on the complexity of calculating amplitudes of quantum circuits in terms of the total number of gates. Our results demonstrate that graphical reasoning can lead to new algorithmic insights, even outside the domain of quantum computing that the calculus was intended for.