Options
Projected Model Counting: Beyond Independent Support
Journal
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN
03029743
Date Issued
2022-01-01
Author(s)
Yang, Jiong
Chakraborty, Supratik
Meel, Kuldeep S.
Abstract
Given a system of constraints over a set X of variables, projected model counting asks us to count satisfying assignments of the constraint system projected on a subset P of X. A key idea used in modern projected counters is to first compute an independent support, say I, that is often a small subset of P, and to then count models projected on I instead of on P. While this has been effective in scaling performance of counters, the question of whether we can benefit by projecting on variables beyond P has not been explored. In this paper, we study this question and show that contrary to intuition, it can be beneficial to project on variables even beyond P. In several applications, a good upper bound of the projected model count often suffices. We show that in several such cases, we can identify a set of variables, called upper bound support (UBS), that is not necessarily a subset of P, and yet counting models projected on UBS guarantees an upper bound of the projected model count. Theoretically, a UBS can be exponentially smaller than the smallest independent support. Our experiments show that even otherwise, UBS-based projected counting can be faster than independent support-based projected counting, while yielding bounds of high quality. Based on extensive experiments, we find that UBS-based projected counting can solve many problem instances that are beyond the reach of a state-of-the-art independent support-based projected model counter.
Volume
13505 LNCS