A Graphical #SAT Algorithm for Formulae with Small Clause Density
share
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 find a natural extension of #SAT which we call #SAT_±, where variables are additionally labeled by phases, which is GapP-complete. Using graphical reasoning, we find a reduction from #SAT to #2SAT_± in the ZH-calculus. We observe that the DPLL algorithm for #2SAT can be adapted to #2SAT_± directly and hence that Wahlstrom's O^*(1.2377^n) upper bound applies to #2SAT_± as well. Combining this with our reduction from #SAT to #2SAT_± gives us novel upper bounds in terms of clauses and variables that are better than O^*(2^n) for small clause densities of m/n < 2.25. This is to our knowledge the first non-trivial upper bound for #SAT that is independent of clause size. Our algorithm improves on Dubois' upper bound for #kSAT whenever m/n < 1.85 and k ≥ 4, and the Williams' average-case analysis whenever m/n < 1.21 and k ≥ 6. We also obtain an unconditional upper bound of O^*(1.88^m) for #4SAT in terms of clauses only, and find an improved bound on #3SAT for 1.2577 < m/n≤7/3. 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.
READ FULL TEXT