A Graphical #SAT Algorithm for Formulae with Small Clause Density

Tuomas Laakkonen, Konstantinos Meichanetzidis, John van de Wetering

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 t…