Engineering an Efficient Probabilistic Exact Model Counter
摘要
Given a formula F, the problem of model counting, also known as #SAT, is to compute the number of satisfying assignments of F. While model counting has emerged as a crucial primitive in diverse domains from quantitative information flow analysis to neural network verification, scalability remains a fundamental challenge despite advances in both exact and approximate counting techniques. We present \(\textsf{Ganak2}\) , a novel framework that achieves substantial performance improvements through three key technical innovations: (1) refined residual formula processing incorporating SAT-specific techniques while maintaining seamless state transitions, (2) dual independent set framework maintaining distinct SAT-eligibility and decision sets, and (3) chronological backtracking specifically adapted to model counting. Our empirical evaluation on 1600 previous model counting competition instances demonstrates that \(\textsf{Ganak2}\) successfully computes counts for 1121 instances within the one hour time limit, compared to 1032 instances by the prior state of the art approach, representing an 8.7% improvement. This progress is especially remarkable considering the extensive development and refinement of model counting tools over the years, driven by yearly competitive evaluation in the field.