Proofs for Propositional Model Counting

Abstract

Although propositional model counting (#SAT) was long considered too hard to be practical, today’s highly efficient solvers facilitate applications in probabilistic reasoning, reliability estimation, quantitative design space exploration, and more. The current trend of solvers growing more capable every year is likely to continue as a diverse range of algorithms are explored in the field. However, to establish model counters as reliable tools like SAT-solvers, correctness is as critical as speed. As in the nature of complex systems, bugs emerge as soon as the tools are widely used. To identify and avoid bugs, explain decisions, and provide trustworthy results, we need verifiable results. We propose a novel system for certifying model counts. We show how proof traces can be generated for exact model counters based on dynamic programming, counting CDCL with component caching, and knowledge compilation to Decision-DNNF, which are the predominant techniques in today’s exact implementations. We provide proof-of-concepts for emitting proofs and a parallel trace checker. Based on this, we show the feasibility of using certified model counting in an empirical experiment.