In Weighted Model Counting (WMC), we assign weights to literals and compute the sum of the weights of the models of a given propositional formula where the weight of an assignment is the product of the weights of its literals. The current WMC solvers work on Conjunctive Normal Form (CNF) formulas. However, CNF is not a natural representation for human-being in many applications. Motivated by the stronger expressive power of pseudo-Boolean (PB) formulas than CNF, we propose to perform WMC on PB formulas. Based on a recent dynamic programming algorithm framework called ADDMC for WMC, we implement a weighted PB counting tool PBCounter. We compare PBCounter with the state-of-the-art weighted model counters SharpSAT-TD, ExactMC, D4, and ADDMC, where the latter tools work on CNF with encoding methods that convert PB constraints into a CNF formula. The experiments on three domains of benchmarks show that PBCounter is superior to the model counters on CNF formulas.

翻译：在加权模型计数中，我们为文字赋予权重，并计算给定命题公式的模型权重之和，其中每个赋值的权重等于其各文字权重的乘积。当前的加权模型计数求解器适用于合取范式公式。然而，在许多应用场景中，合取范式并非人类直觉的自然表示方式。鉴于伪布尔公式比合取范式具有更强的表达能力，我们提出对伪布尔公式进行加权模型计数。基于近期针对加权模型计数提出的动态规划算法框架ADDMC，我们实现了加权伪布尔计数工具PBCounter。我们将PBCounter与当前最先进的加权模型计数器SharpSAT-TD、ExactMC、D4及ADDMC进行对比——这些工具均通过编码方法将伪布尔约束转换为合取范式公式后进行处理。在三个基准测试领域的实验表明，PBCounter相较于基于合取范式的模型计数器具有显著优势。