In this paper we present a new proof system framework CLIP (Circuit Linear Induction Proposition) for propositional model counting (#SAT). A CLIP proof firstly involves a Boolean circuit, calculating the cumulative function (or running count) of models counted up to a point, and secondly a propositional proof arguing for the correctness of the circuit.

This concept is remarkably simple and CLIP is modular so allows us to use existing checking formats from propositional logic, especially strong proof systems. CLIP has polynomial-size proofs for XOR-pairs which are known to require exponential-size proofs in MICE [Fichte et. al., SAT 2022]. The existence of a strong proof system that can tackle these hard problems was posed as an open problem in [Beyersdorff et al., SAT 2023]. In addition, CLIP systems can p-simulate all other existing #SAT proofs systems (KCPS(#SAT) [Capelli, SAT 19], CPOG [Bryant et. al., SAT, 2023], MICE).

Furthermore, CLIP has a theoretical advantage over the other #SAT proof systems in the sense that CLIP only has lower bounds from its propositional proof system or if P^{#P} is not contained in P/poly, which is a major open problem in circuit complexity.

CLIP uses unrestricted circuits in its proof as compared to restricted structures used by the existing #SAT proof systems. In this way, CLIP avoids hardness or limitations due to circuit restrictions.

Added new results including p-simulation of CPOG proof system.

In this paper we present a new proof system framework CLIP (Cumulation Linear Induction Proposition) for propositional model counting. A CLIP proof firstly involves a circuit, calculating the cumulative function (or running count) of models counted up to a point, and secondly a propositional proof arguing for the correctness of the circuit. This concept is remarkably simple and CLIP is modular so allows us to use existing checking formats from propositional logic, especially strong proof systems. Despite model counting being a harder problem than unsatisfiability, we find that CLIP only has lower bounds from its propositional proof system or if P^#P is not contained in P/poly, similar to results in QBF proof complexity (Beyersdorff et al. Journal of the ACM 2020). From a proof complexity point of view we find it is exponentially stronger than existing proof systems MICE (Fichte et al. SAT 2022) and KCPS(#SAT) (Capelli SAT 2019) for propositional model counting.