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.

我们提出了第一个准确的伪布尔模型计数器PBCount，它通过代数决策图的知识编译方法来实现。我们的实证评估表明，PBCount可以计算1513个实例的计数，而当前最先进的方法只能处理1013个实例。我们的工作为进一步研究伪布尔公式的模型计数提供了几个方向，如预处理技术的开发和除知识编译之外的其他方法的探索。

构建精确的伪布尔模型计数器