| ||||
| ||||
![]() Title:Proof Complexity of Propositional Model Counting Conference:SAT 2023 Tags:#SAT, lower bounds, model counting, proof complexity and proof systems Abstract: Recently, the first 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. Our main result establishes an exponential lower bound for the number of proof steps in MICE' (and hence also in MICE) for a specific family of CNFs. Proof Complexity of Propositional Model Counting ![]() Proof Complexity of Propositional Model Counting | ||||
Copyright © 2002 – 2025 EasyChair |