Weighted Model counting (WMC) is a fundamental problem in computer science with a wide variety of applications in practice, ranging from neural network verification to network reliability. The current WMC solvers work on Conjunctive Normal Form (CNF) formulas. However, CNF is not a natural representation of human beings in many applications.

Motivated by the stronger expressive power of pseudo-Boolean (PB) formulas than CNF, Yong LAI, and Minghao Yin proposed to perform WMC on PB formulas. They published their new research on 15 Mar 2025 in Frontiers of Computer Science co-published by Higher Education Press and Springer Nature.

The research is based on variable elimination and uses the algorithmic framework of dynamic programming with Algebraic Decision Diagrams (ADDs) as its main data structure. Algorithms for constructing ADDs were designed for the Relaxed normalized PB constraints. Based on the ADD representation, the research also designed two preprocessing methods for WMC on PB formulas.

The research compared their solver PBCounter with the state-of-the-art weighted model counters SharpSAT-TD, ExactMC, D4, and ADDMC, where the latter tools on CNF with encoding methods that covert 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. One future direction of this research is to develop a more effective pre-processor for the WMC task on PB constraints.

DOI: 10.1007/s11704-024-3631-1