Model counting, a fundamental task in computer science, involves determining the number of satisfying assignments to a Boolean formula, typically represented in conjunctive normal form (CNF). While model counting for CNF formulas has received extensive attention with a broad range of applications, the study of model counting for Pseudo-Boolean (PB) formulas has been relatively overlooked. Pseudo-Boolean formulas, being more succinct than propositional Boolean formulas, offer greater flexibility in representing real-world problems. Consequently, there is a crucial need to investigate efficient techniques for model counting for PB formulas. In this work, we propose the first exact Pseudo-Boolean model counter, PBCount, that relies on knowledge compilation approach via algebraic decision diagrams. Our extensive empirical evaluation shows that PBCount can compute counts for 1513 instances while the current state-of-the-art approach could only handle 1013 instances. Our work opens up several avenues for future work in the context of model counting for PB formulas, such as the development of preprocessing techniques and exploration of approaches other than knowledge compilation.

翻译：模型计数是计算机科学中的一项基础任务，涉及确定布尔公式（通常表示为合取范式）的满足赋值数量。尽管针对CNF公式的模型计数已受到广泛关注并应用于诸多领域，但针对伪布尔公式的模型计数研究相对不足。伪布尔公式比命题布尔公式更简洁，在表示实际问题时具有更强的灵活性。因此，亟需探索高效的伪布尔公式模型计数技术。本文提出了首个精确伪布尔模型计数器PBCount，该计数器采用基于代数决策图的知识编译方法。广泛的实验评估表明，PBCount能对1513个实例完成计数，而当前最先进的方法仅能处理1013个实例。本工作为伪布尔公式模型计数的未来研究开辟了多项方向，例如开发预处理技术以及探索知识编译之外的其他方法。