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 kcps kcps (knowledge compilation proof system), MICE MICE (model counting induction by claim extension), and CPOG CPOG (certified partitioned-operation graphs) have been introduced with the aim to model #SAT solving and enable proof logging for solvers. A fourth system, CLIP CLIP (circuit linear introduction proposition), is a very powerful proof system of theoretical interest. Prior to this paper, it was only known that CLIP 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 CPOG CPOG simulates both MICE MICE and kcps kcps , while MICE MICE and kcps kcps are exponentially incomparable. This implies that CPOG CPOG is strictly stronger than the other two systems.