A Graphical SAT Algorithm for Formulae with Small Clause Density

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 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 Wahlström’s𝑂^∗ (1.2377^𝑛 ) 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 𝑂^∗(2 ^𝑛 ) for small clause densities of 𝑚/𝑛 < 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 𝑚/𝑛 < 1.85 and 𝑘 ≥ 4, and the Williams’ average-case analysis whenever 𝑚/𝑛 < 1.21 and 𝑘 ≥ 6. We also obtain an unconditional upper bound of 𝑂^∗ (1.88𝑚) for #4SAT in terms of clauses only, and find an improved bound on #3SAT for 1.2577 < 𝑚/𝑛 ≤ 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.