Circuits, Proofs and Propositional Model Counting

Abstract

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 [16]. The existence of a strong proof system that can tackle these hard problems was posed as an open problem in Beyersdorff et al. [3]. In addition, CLIP systems can p-simulate all other existing #SAT proofs systems (KCPS(#SAT) [8], CPOG [4], 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.