Research map / Continual learning / Online and replay-based
Towards Projected and Incremental Pseudo-Boolean Model Counting
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.
Introduces PBCount2, the first exact PB model counter supporting projected and incremental counting, using a Least Occurrence Weighted Min Degree ordering and an ADD cache.
Problem
Exact pseudo-Boolean (PB) model counting lacks support for projected and incremental settings, which hinders adoption of PB counters compared to CNF counters.
Approach
Bottom-up ADD-based PB counter that orders variable merges/projections via a weighted min-degree heuristic (LOWMD) compatible with projected counting (OR-projection for non-projection variables before ADD-sum projection for projection variables), plus a cache of intermediate ADDs keyed by constraint sets and projected-away variables to reuse computation across constraint additions/removals.
Key results
- On projected counting, PBCount2 completed 1957 instances versus 1398 for D4 and 1315 for GPMC (about 1.40x the best competitor).
- On 5-step incremental benchmarks, PBCount2 completed 1618 instances versus 1371 for PBCount (1.18x) and 676 for D4 and 886 for GPMC.
- On 3-step incremental benchmarks, PBCount2 completed 1658 instances, 1.16x PBCount's 1427.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use PBCount2 for native projected PB model counting instead of converting PB formulas to CNF for d4 | Projected PB counting · Projected benchmarks — Total | completed instances: 1398 -> 1957 | Helped |
| Use PBCount2 for native projected PB model counting instead of converting PB formulas to CNF for gpmc | Projected PB counting · Projected benchmarks — Total | completed instances: 1315 -> 1957 | Helped |
| Add projected-counting support with the Least Occurrence Weighted Min Degree ordering heuristic | PBCount2 · Projected benchmarks — Total | completed instances: 1398 -> 1957 | Helped |
| Add incremental counting with cached intermediate ADDs | PBCount2 · Incremental 3-step — Total | completed instances: 1427 -> 1658 | Helped |
| Add incremental counting with cached intermediate ADDs | PBCount2 · Incremental 5-step — Total | completed instances: 1371 -> 1618 | Helped |
| Disable preprocessing (ablation) | PBCount · Incremental 3-step — Total | completed instances: 1427 -> 1401 | Hurt |
| Disable preprocessing (ablation) | PBCount · Incremental 5-step — Total | completed instances: 1371 -> 1347 | Hurt |
Surprising findings
- Disabling preprocessing in PBCount reduces its incremental completions (1427 to 1401 in 3-step), indicating preprocessing removal is a cost of incrementality.
Limitations
- Incremental mode requires disabling preprocessing, which costs performance.
- Evaluated only on synthetic benchmarks derived from prior work.
- Cache retrieval adds search overhead.
Experimental setup
Datasets: auction benchmarks multi-dimension knapsack benchmarks sensor placement benchmarks
Benchmarks: auction multi-dimension knapsack sensor placement
Metrics: number of instances completed within 3600s timeout
Baselines: D4 GPMC PBCount ApproxMC-PB
Builds on: PBCount AddMC project-join tree framework CUDD
Closest papers by meaning
- Engineering an Exact Pseudo-Boolean Model Counter (AAAI 2024 · similarity 0.95)
- Towards Real-Time Approximate Counting (AAAI 2025 · similarity 0.89)
- Auditable Algorithms for Approximate Model Counting (AAAI 2024 · similarity 0.87)
- An Approximate Skolem Function Counter (AAAI 2024 · similarity 0.86)
- Model Counting and Sampling via Semiring Extensions (AAAI 2024 · similarity 0.84)
- The Gradient of Algebraic Model Counting (AAAI 2025 · similarity 0.83)
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.