# PBCounter: Weighted Model Counting on Pseudo-Boolean Formulas

arXiv: https://arxiv.org/abs/2312.15877 · HTML: https://mlsanity.com/paper/2312.15877/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 57 references that are in the map.
- First posted on arXiv 26 Dec 2023.

## Builds on (most cited first, 7 of 7)

- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [A Scalable Approximate Model Counter](https://mlsanity.com/paper/1306.5726/) (2013)
- [ADDMC: Weighted Model Counting with Algebraic Decision Diagrams](https://mlsanity.com/paper/1907.05000/) (2019)
- [Arjun: An Efficient Independent Support Computation Technique and its Applications to Counting and Sampling](https://mlsanity.com/paper/2110.09026/) (2021)
- [A New Look at BDDs for Pseudo-Boolean Constraints](https://mlsanity.com/paper/1401.5860/) (2014)
- [SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints](https://mlsanity.com/paper/2110.08068/) (2021)
- [Fast Converging Anytime Model Counting](https://mlsanity.com/paper/2212.09390/) (2022)

## Built on by (most cited first, 1 of 1)

- [Scalable Precise Computation of Shannon Entropy](https://mlsanity.com/paper/2502.01160/) (2025)

## Abstract (arXiv)

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.