2026-08-17T16:38:21Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22207 2024-12-05T15:18:03Z ddc:004 open_access

Circuits, Proofs and Propositional Model Counting Chede, Sravanthi Chew, Leroy Shukla, Anil Propositional model counting Boolean circuits #SAT Proof Systems Certified Partition Operation Graph (CPOG) 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 it 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., 2022]. The existence of a strong proof system that can tackle these hard problems was posed as an open problem in Beyersdorff et al. [Olaf Beyersdorff et al., 2023]. In addition, CLIP systems can p-simulate all other existing #SAT proofs systems (KCPS(#SAT) [Florent Capelli, 2019], CPOG [Bryant et al., 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 𝖯^#𝖯 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sravanthi Chede and Leroy Chew and Anil Shukla 2024 Is Part Of LIPIcs, Volume 323, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2024.18 urn:nbn:de:0030-drops-222079 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.18 eng https://creativecommons.org/licenses/by/4.0/legalcode