Engineering an Exact Pseudo-Boolean Model Counter

TL;DR

This work addresses accurate counting of solutions to Pseudo-Boolean constraints, a representation more succinct than CNF for many real-world problems. It introduces PBCount, the first exact PB model counter, which directly compiles PB constraints into Algebraic Decision Diagrams (ADDs) and reuses ADD-based counting techniques. The authors implement dual PB constraint compilation strategies (bottom-up and top-down) plus optimizations and a dynamic compilation heuristic, demonstrating substantial improvements over state-of-the-art CNF-based counters across sensor placement, knapsack, and auction benchmarks. The results highlight the practicality and scalability of native PB reasoning, motivating further preprocessing and PB-focused techniques for counting.

Abstract

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.

Figures (8)

• Figure 1: An ADD representing $3x_1 + 4x_2$
• Figure 2: Overall flow of our PB model counter $\mathsf{PBCount}$. Shaded boxes indicate our contributions.
• Figure 3: Preprocessing of PB formula
• Figure 4: An ADD $\psi_1$ representing $3x_1 + 4x_2 \geq 3$
• Figure 5: Cactus plot of number of benchmark instances completed by different counters. A point ($x,y$) on each line plot indicates the corresponding counter completes $x$ number of benchmarks after $y$ seconds has elapsed.