Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Projected and Incremental Pseudo-Boolean Model Counting

Suwei Yang, Kuldeep S. Meel

TL;DR

This work introduces PBCount2, the first exact PB model counter with native support for both projected and incremental model counting. It combines a novel LOW-MD variable ordering with a caching mechanism to efficiently merge PB constraints, project away variables, and reuse intermediate results across incremental changes. The approach is grounded in an $X,Y$-graded project join tree framework and ADD-based representations, ensuring correctness for projected PB counting. Empirical results show PBCount2 outperforming state-of-the-art projected CNF solvers and PB counters on diverse benchmarks, highlighting practical gains for applications requiring projections and incremental updates in PB formulations.

Abstract

Model counting is a fundamental task that involves determining the number of satisfying assignments to a logical formula, typically in conjunctive normal form (CNF). While CNF model counting has received extensive attention over recent decades, interest in Pseudo-Boolean (PB) model counting is just emerging partly due to the greater flexibility of PB formulas. As such, we observed feature gaps in existing PB counters such as a lack of support for projected and incremental settings, which could hinder adoption. In this work, our main contribution is the introduction of the PB model counter PBCount2, the first exact PB model counter with support for projected and incremental model counting. Our counter, PBCount2, uses our Least Occurrence Weighted Min Degree (LOW-MD) computation ordering heuristic to support projected model counting and a cache mechanism to enable incremental model counting. In our evaluations, PBCount2 completed at least 1.40x the number of benchmarks of competing methods for projected model counting and at least 1.18x of competing methods in incremental model counting.

Towards Projected and Incremental Pseudo-Boolean Model Counting

TL;DR

This work introduces PBCount2, the first exact PB model counter with native support for both projected and incremental model counting. It combines a novel LOW-MD variable ordering with a caching mechanism to efficiently merge PB constraints, project away variables, and reuse intermediate results across incremental changes. The approach is grounded in an -graded project join tree framework and ADD-based representations, ensuring correctness for projected PB counting. Empirical results show PBCount2 outperforming state-of-the-art projected CNF solvers and PB counters on diverse benchmarks, highlighting practical gains for applications requiring projections and incremental updates in PB formulations.

Abstract

Model counting is a fundamental task that involves determining the number of satisfying assignments to a logical formula, typically in conjunctive normal form (CNF). While CNF model counting has received extensive attention over recent decades, interest in Pseudo-Boolean (PB) model counting is just emerging partly due to the greater flexibility of PB formulas. As such, we observed feature gaps in existing PB counters such as a lack of support for projected and incremental settings, which could hinder adoption. In this work, our main contribution is the introduction of the PB model counter PBCount2, the first exact PB model counter with support for projected and incremental model counting. Our counter, PBCount2, uses our Least Occurrence Weighted Min Degree (LOW-MD) computation ordering heuristic to support projected model counting and a cache mechanism to enable incremental model counting. In our evaluations, PBCount2 completed at least 1.40x the number of benchmarks of competing methods for projected model counting and at least 1.18x of competing methods in incremental model counting.

Paper Structure

This paper contains 30 sections, 5 theorems, 10 equations, 5 figures, 4 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Notations and Preliminaries
  3. Pseudo-Boolean Formula
  4. Projected Model Counting
  5. Projections
  6. Algebraic Decision Diagram
  7. Project-Join Tree
  8. X,Y-Graded Project-Join Tree
  9. Projected Model Counting with Project Join Trees
  10. Related Work
  11. Search-Based Model Counters
  12. Decision Diagram-Based Model Counters
  13. Pseudo-Boolean Model Counting
  14. Incremental SAT Solving
  15. Approach
  16. ...and 15 more sections

Key Result

Theorem 1

Let $F$ be a formula defined over $X \cup Y$ such that $X$ is the projection set, and $Y$ is the set of variables not in projection set, then given an instance $(F,X,Y)$, Algorithm alg:pbcount-greedy-mc returns $c$ such that $c = \sum_{\beta \in 2^X} (\max_{\alpha \in 2^Y} [F](\alpha \cup \beta))$

Figures (5)

  • Figure 1: An ADD representing $2 x_1 + x_2 + x_3$ with ordering $x_1,x_2,x_3$
  • Figure 2: An ADD representing $2 x_1 + x_2 + x_3 \geq 2$ with ordering $x_1,x_2,x_3$
  • Figure 3: Overall flow of our projected model counter $\mathsf{PBCount2}$. Shaded boxes indicate our contributions and white box indicates techniques adapted from existing works. Line numbers correspond to lines in Algorithm \ref{['alg:pbcount-greedy-mc']}.
  • Figure 4: Runtime cactus plots of $\mathsf{PBCount2}$ and competing methods for each benchmark set, for projected model counting.
  • Figure 5: Runtime cactus plots of $\mathsf{PBCount2}$ and competing methods for each benchmark set, for incremental counting with 5 steps.

Theorems & Definitions (12)

  • Theorem 1
  • proof
  • Definition 1: Projected Valuation
  • Definition 2: Early Projection
  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Lemma 3
  • proof
  • ...and 2 more