John van de Wetering

We study the counting version of the Boolean satisfiability problem sSAT 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 labelled 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 fracmn < 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 fracmn < 1.85 and k geq 4, and the Williams' average-case analysis whenever fracmn < 1.21 and k geq 6. We also obtain an upper bound of O^*(1.1740^L) for sSAT in terms of the length of the formula, and find an improved bound on #textbf3SAT for 1.2577 < fracmn łeq frac73. 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. In addition, using the connection to counting problems, we find a new classical simulation algorithm for quantum computations that runs in O(1.38^g) where g is the number of gates.