Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR24-030 | 22nd February 2024 12:09

Proof Complexity of Propositional Model Counting

RSS-Feed




TR24-030
Authors: Olaf Beyersdorff, Tim Hoffmann, Luc Nicolas Spachmann
Publication: 22nd February 2024 12:46
Downloads: 291
Keywords: 


Abstract:

Recently, the proof system MICE for the model counting problem #SAT was introduced by Fichte, Hecher and Roland (SAT’22). As demonstrated by Fichte et al., the system MICE can be used for proof logging for state-of-the-art #SAT solvers.
We perform a proof-complexity study of MICE. For this we first simplify the rules of MICE and obtain a calculus MICE? that is polynomially equivalent to MICE. We then establish an exponential lower bound for the number of proof steps in MICE? (and hence also in MICE) for a specific family of CNFs. We also explain a tight connection between MICE proofs and decision DNNFs.



ISSN 1433-8092 | Imprint