GANAK: A Scalable Probabilistic Exact Model Counter

TLDR

Model counting (#SAT) computes the number of solutions of a Boolean formula and is central to applications such as planning and probabilistic reasoning, yet modern solvers rely on static or dynamic decomposition techniques whose core design has remained unchanged for over a decade. This work revisits the state‑of‑the‑art dynamic decomposition solver sharpSAT to demonstrate that incorporating probabilistic component caching, universal hashing, and new heuristics can substantially improve performance. We introduce GANAK, a scalable probabilistic exact model counter that employs probabilistic component caching and universal hashing with novel heuristics to accelerate exact counting. GANAK outperforms sharpSAT and ApproxMC3 in PAR‑2 score and number of instances solved, produces exact counts on all benchmarks, and shows that preprocessing techniques benefit exact counters while harming approximate ones.

Abstract

Given a Boolean formula F, the problem of model counting, also referred to as #SAT, seeks to compute the number of solutions of F. Model counting is a fundamental problem with a wide variety of applications ranging from planning, quantified information flow to probabilistic reasoning and the like. The modern #SAT solvers tend to be either based on static decomposition, dynamic decomposition, or a hybrid of the two. Despite dynamic decomposition based #SAT solvers sharing much of their architecture with SAT solvers, the core design and heuristics of dynamic decomposition-based #SAT solvers has remained constant for over a decade. In this paper, we revisit the architecture of the state-of-the-art dynamic decomposition-based #SAT tool, sharpSAT, and demonstrate that by introducing a new notion of probabilistic component caching and the usage of universal hashing for exact model counting along with the development of several new heuristics can lead to significant performance improvement over state-of-the-art model-counters. In particular, we develop GANAK, a new scalable probabilistic exact model counter that outperforms state-of-the-art exact and approximate model counters sharpSAT and ApproxMC3 respectively, both in terms of PAR-2 score and the number of instances solved. Furthermore, in our experiments, the model count returned by GANAK was equal to the exact model count for all the benchmarks. Finally, we observe that recently proposed preprocessing techniques for model counting benefit exact model counters while hurting the performance of approximate model counters.