435 - 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 moderate 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.