Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR24-081 | 2nd April 2024 22:56

Circuits, Proofs and Propositional Model Counting



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.

ISSN 1433-8092 | Imprint