The Relative Strength of #SAT Proof Systems

The propositional model counting problem #SAT asks to compute the number of satisfying assignments for a given propositional formula. Recently, three #SAT proof systems $\mathrm{kcps}$ (knowledge compilation proof system), $\mathrm{MICE}$ (model counting induction by claim extension), and $\mathrm{CPOG}$ (certified partitioned-operation graphs) have been introduced with the aim to model #SAT solving and enable proof logging for solvers. A fourth system, $\mathrm{CLIP}$ (circuit linear introduction proposition), is a very powerful proof system of theoretical interest. Prior to this paper, it was only known that $\mathrm{CLIP}$ simulates the three other systems. All the remaining relations between the systems have been unclear and very few proof complexity results are known. We completely determine the simulation order of the four systems, establishing that $\mathrm{CPOG}$ simulates both $\mathrm{MICE}$ and $\mathrm{kcps}$ , while $\mathrm{MICE}$ and $\mathrm{kcps}$ are exponentially incomparable. This implies that $\mathrm{CPOG}$ is strictly stronger than the other two systems.