Proof Systems That Tightly Characterise Model Counting Algorithms

Several proof systems for model counting have been introduced in recent years, mainly in an attempt to model #SAT solving and to allow proof logging of solvers. We reexamine these different approaches and show that: (i) with slight adaptations, the conceptually quite different proof models of the dynamic system MICE (Fichte, Hecher, and Roland 2022) and the static system of annotated Decision DNNFs (Capelli, Lagniez, and Marquis 2021) are equivalent and (ii) they tightly characterise state-of-the-art #SAT solving. Thus, these proof systems provide a precise and robust proof-theoretic underpinning of current model counting. We also propose new strengthenings of these proof systems that might lead to stronger model counters.