PBCounter: Weighted Model Counting on Pseudo-Boolean Formulas
This work addresses the need for more natural and expressive representations in WMC for applications like probabilistic reasoning, though it is incremental as it builds on an existing dynamic programming framework.
The paper tackled the problem of performing Weighted Model Counting (WMC) on pseudo-Boolean formulas instead of CNF, resulting in a tool called PBCounter that outperformed state-of-the-art CNF-based counters in experiments across three benchmark domains.
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.