Model counting is a fundamental task that involves determining the number of satisfying assignments to a logical formula, typically in conjunctive normal form (CNF). While CNF model counting has received extensive attention over recent decades, interest in Pseudo-Boolean (PB) model counting is just emerging partly due to the greater flexibility of PB formulas. As such, we observed feature gaps in existing PB counters such as a lack of support for projected and incremental settings, which could hinder adoption. In this work, our main contribution is the introduction of the PB model counter PBCount2, the first exact PB model counter with support for projected and incremental model counting. Our counter, PBCount2, uses our Least Occurrence Weighted Min Degree (LOW-MD) computation ordering heuristic to support projected model counting and a cache mechanism to enable incremental model counting. In our evaluations, PBCount2 completed at least 1.40x the number of benchmarks of competing methods for projected model counting and at least 1.18x of competing methods in incremental model counting.

翻译：模型计数是一项基础任务，旨在确定逻辑公式（通常为合取范式）满足赋值（SAT）的数量。尽管合取范式模型计数在近几十年得到了广泛关注，但伪布尔模型计数的研究兴趣才刚刚兴起，部分原因在于伪布尔公式具有更高的灵活性。因此，我们观察到现有伪布尔计数器存在功能缺口，例如缺乏对投影和增量设置的支持，这可能阻碍其应用。本工作的主要贡献是引入了伪布尔模型计数器PBCount2，这是首个支持投影与增量模型计数的精确伪布尔模型计数器。我们的计数器PBCount2采用我们提出的最小出现次数加权最小度计算排序启发式算法来支持投影模型计数，并利用缓存机制实现增量模型计数。在评估中，PBCount2在投影模型计数方面完成的基准测试数量至少达到竞争方法的1.40倍，在增量模型计数方面至少达到竞争方法的1.18倍。