Research map / Learning theory and algorithms / Combinatorial and search optimization
Engineering an Exact Pseudo-Boolean Model Counter
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes PBCount, the first exact pseudo-Boolean model counter, which compiles PB constraints into algebraic decision diagrams (top-down and bottom-up) and counts via the ADDMC framework, completing 1513 of 3473 benchmarks versus 1013 for the best CNF counter.
Problem
Exact model counting for pseudo-Boolean formulas has been largely neglected; existing approaches convert PB to CNF and use CNF model counters, which is inefficient given PB's succinctness.
Approach
Compile each PB constraint directly into an ADD using either a top-down (ITE-based, with early termination) or bottom-up (apply-based, with subset-sum leaf reduction) method, choose between them dynamically per constraint, and then run ADDMC's dynamic programming counting over the constraint ADDs.
Key results
- PBCount completes 1513 of 3473 instances in 3600s versus 1013 for GPMC, 963 for D4, and 782 for DPMC.
- On multi-dimension knapsack PBCount completes 503 instances versus 281 for D4 and 279 for GPMC; on auctions 372 versus 159 for GPMC.
- Bottom-up compilation outperforms top-down on auction and knapsack (e.g., 375 vs 158 auction instances); dynamic selection completes 372 auction instances.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use native PB counting with PBCount rather than projected CNF counting with GPMC | PB model counting · All benchmarks | instances completed (3600s): 1013 -> 1513 | Helped |
| Use native PB counting with PBCount rather than the strongest CNF counter on each benchmark | Sensor placement · Sensor placement | instances completed (3600s): 625 -> 638 | Helped |
| Use native PB counting with PBCount rather than the strongest CNF counter on each benchmark | PBCount · M-dim knapsack | instances completed (3600s): 281 -> 503 | Helped |
| Use native PB counting with PBCount rather than the strongest CNF counter on each benchmark | PBCount · Auction | instances completed (3600s): 159 -> 372 | Helped |
| Use bottom-up instead of top-down constraint compilation (ablation) | PBCount · Sensor placement | instances completed: 580 -> 638 | Helped |
| Use bottom-up instead of top-down constraint compilation (ablation) | PBCount · M-dim knapsack | instances completed: 109 -> 503 | Helped |
| Use bottom-up instead of top-down constraint compilation (ablation) | PBCount · Auction | instances completed: 158 -> 375 | Helped |
| Use dynamic compilation instead of bottom-up compilation (ablation) | PBCount · Auction | instances completed: 375 -> 372 | Hurt |
| Add dynamic compilation and term coefficient optimization instead of always using bottom-up (ablation) | PBCount · Auction benchmarks completed by both approaches | instances faster: 257 points beneath red diagonal line; 115 points above | Mixed |
| Disable preprocessing (ablation) | PBCount · All benchmarks | instances completed (3600s): 1513 -> 1510 | Hurt |
| Disable preprocessing (ablation) | GPMC · All benchmarks | instances completed (3600s): 1013 -> 966 | Hurt |
| Set auction constraint coefficients to one of three randomly generated values instead of one shared random magnitude (ablation) | PBCount bottom-up compilation · Auction modified benchmarks | instances completed: 758 -> 705 | Hurt |
Surprising findings
- PBCount achieves superior performance with minimal preprocessing; without preprocessing it completes 1510 instances versus GPMC's 966 without preprocessing.
- Top-down compilation can be much slower than bottom-up even when all coefficients are unique, when early termination is not possible.
Limitations
- Preprocessing is preliminary (unit propagation and assumption probing only); the authors note more advanced preprocessing is future work.
- Dynamic compilation heuristic thresholds are empirically designed and only tuned on the studied benchmarks.
- Evaluation limited to three synthetic benchmark families generated by the authors.
Experimental setup
Datasets: sensor placement benchmarks (1473 instances) combinatorial auction benchmarks (1000 instances) multi-dimension knapsack benchmarks (1000 instances)
Benchmarks: sensor placement multi-dimension knapsack auction counting benchmarks
Metrics: number of instances completed within 3600s unique instances solved runtime
Baselines: GPMC DPMC D4 PBLib + CNF counters
Builds on: ADDMC PBLib Ganak GPMC
Closest papers by meaning
- Towards Projected and Incremental Pseudo-Boolean Model Counting (AAAI 2025 · similarity 0.95)
- Towards Real-Time Approximate Counting (AAAI 2025 · similarity 0.89)
- An Approximate Skolem Function Counter (AAAI 2024 · similarity 0.88)
- Auditable Algorithms for Approximate Model Counting (AAAI 2024 · similarity 0.87)
- The Gradient of Algebraic Model Counting (AAAI 2025 · similarity 0.86)
- Submodel Enumeration for CTL Is Hard (AAAI 2024 · similarity 0.85)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.