A Novel Reduction from #SAT to #2SAT Based on Symmetry: Simply Drop the Large Clauses

The counting problem #2sat is complete for #P under Turing (many-call) reductions, which dates back to the seminal work by Valiant from 1979. Arguably, this reduction is the opposite from being simple as it is a sophisticated chain of transformation from #sat, via several variations of the problem of computing the permanent, to the task of counting matchings in graphs, and then finally to #2sat. In contrast, we give a simple reduction that makes only two calls instead of polynomially many calls. Our reduction is based on the inclusion-exclusion principle from #sat to weighted #2sat with weights in \(\{-1, 1\}\). From there, we map the computation of such weighted model counting problems to the subtraction of two unweighted model counting problems using parity constraints. We can encode these parity constraints using almost solely binary clauses and very few clauses of size four. Then, thanks to the subtraction and the symmetry between the two formulas, these clauses of size four can simply be omitted without changing the overall result of the computation — thus leading to a surprisingly simple reduction from #sat to two calls of #2sat.