首个支持投影与增量的精确伪布尔计数工具，提升逻辑公式解数计算效率。
Towards Projected and Incremental Pseudo-Boolean Model Counting
- 采用低频加权最小度排序启发式，实现投影模型计数。
- 引入缓存机制支持增量计数，提升重复查询效率。
- 在投影和增量场景下分别提速1.4倍和1.18倍，适合形式化验证用户。
模型计数是确定逻辑公式（通常为合取范式，CNF）满足赋值数量的基本任务。尽管CNF模型计数已受长期关注，但伪布尔（PB）模型计数因公式灵活性更高而逐渐兴起。然而，现有PB计数器存在投影和增量设置支持不足的问题，限制了其应用。本文提出首个支持投影与增量的精确PB模型计数器PBCount2。该方法采用最小度加权最低频率（LOW-MD）计算顺序启发式以支持投影计数，并引入缓存机制实现增量计数。实验表明，PBCount2在投影计数任务上至少完成竞品1.40倍的基准测试，在增量计数任务上至少完成竞品1.18倍，显著提升效率。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。