On Top-Down Pseudo-Boolean Model Counting

A pseudo-Boolean (PB) formula $F$ consists of a set $\mathrm{\Omega }$ of one or more pseudo-Boolean constraints. Each PB constraint $\omega \in \mathrm{\Omega }$ is of the form ${\sum }_{i=1}^n{a}_i{x}_i⊳k$, where $x_1,\mathrm{\dots },x_n$ are Boolean literals, $a_1,\mathrm{\dots },a_n$, and $k$ are integers, and $⊳$ is one of $\{\ge ,=,\le \}$. $a_1,\mathrm{\dots },a_n$ are referred to as term coefficients in the PB constraint, where each term is of the form $a_i{x}_i$ and $k$ is known as the degree of a PB constraint. An assignment $\sigma$ is a satisfying assignment if it assigns values to all variables of $F$ such that all the PB constraints in $\mathrm{\Omega }$ evaluate to true. PB model counting refers to the task of determining the number of satisfying assignments of $F$.

Without loss of generality, the PB constraints in this work are all of the “$\ge$” type unless otherwise stated as “$\le$” type constraints can be converted by multiplying -1 on both sides, and “$=$” type constraints can be replaced with a pair of “$\ge$” and “$\le$” constraints. In addition, all coefficients are positive unless stated otherwise as the signs of coefficients can be changed using $\overline{x}=1-x$ and updating the degree accordingly. We use the term gap $s$ to denote the satisfiability gap of a PB constraint $\omega$ under assignment $\sigma$. A gap value of 0 or less indicates $\omega$ is always satisfied under $\sigma$, otherwise $\omega$ is yet to be satisfied.

Model counters that are of the bottom-up design typically make use of decision diagrams, which are directed acyclic graph (DAG) representations of functions, in the computation process. In particular, the counters make use of the $\mathrm{𝖠𝗉𝗉𝗅𝗒}$ operation [2] to build up the representation of the input logical formula in a bottom-up manner. Notable bottom-up counters including $\mathrm{𝖠𝖣𝖣𝖬𝖢}$, $\mathrm{𝖣𝖯𝖬𝖢}$, $\mathrm{𝖯𝖡𝖢𝗈𝗎𝗇𝗍𝖾𝗋}$, and $\mathrm{𝖯𝖡𝖢𝗈𝗎𝗇𝗍}$ [3, 4, 5, 13, 19, 20] employ algebraic decision diagrams (ADDs) [1] to perform model counting tasks. These counters use early projection of variables to reduce the size of the intermediate decision diagrams in practice, as the complexity of the $\mathrm{𝖠𝗉𝗉𝗅𝗒}$ operation is on the order of the product of sizes of the two operand diagrams. The aforementioned counters first construct individual ADDs of the input formula components i.e. clauses in the case of CNF and constraints in the case of PB formula. The individual ADDs are then merged via the $\mathrm{𝖠𝗉𝗉𝗅𝗒}$ operation with the “$\times$” operator to produce intermediate ADDs. Variables are projected out using the $\mathrm{𝖠𝗉𝗉𝗅𝗒}$ operation with the “$+$” operator according to either an initially computed plan or via heuristics. Once all ADDs are merged and all variables are projected out, the final ADD has a single leaf node that indicates the model count.

Existing top-down model counters, typically for CNF formulas, adopt similar search methodologies in solvers, which tend to be the Conflict-Driven Clause Learning (CDCL) algorithm, to compute the model count. Notable counters with the top-down component caching design include $\mathrm{𝖣𝟦}$, $\mathrm{𝖦𝖯𝖬𝖢}$, $\mathrm{𝖦𝖺𝗇𝖺𝗄}$, and $\mathrm{𝖲𝗁𝖺𝗋𝗉𝖲𝖠𝖳}$-$\mathrm{𝖳𝖣}$ [12, 15, 17, 11] which demonstrated superior performance as winners of recent model counting competitions. On a high level, top-down counters iteratively assign values to variables until all variables are assigned a value or a conflict is encountered. In the process, sub-components are created by either branching on a variable or splitting a component into smaller variable-disjoint components. The counters cache the components and their respective counts to avoid duplicate computation. When all variables are assigned, the counter reaches a satisfying assignment and will assign the current component the count 1 and backtrack to account for other branches. When the counter encounters a conflict i.e. the existing assigned variable already falsifies the formula, it learns the reason for the conflict and prunes the search space such that this sub-branch of the search will be avoided in the remaining computation process. A leaf component in the implicit search tree either has a count of 0 for conflicts and a count of 1 when all variables are assigned. The count of a component that has variable-disjoint sub-components is the product of the counts of its sub-components. The count of a component that branches on a variable is the sum of the counts from the two branches. After accounting for all search branches, the counter returns the final count of satisfying assignments.

The overall counting approach of $\mathrm{𝖯𝖡𝖬𝖢}$ is shown in Algorithms 1 and 2. $\mathrm{𝖢𝗈𝗎𝗇𝗍𝖯𝖡𝖬𝖢}$ starts with preprocessing the input PB formula $F$ with techniques adapted from existing state-of-the-art counters [19]. Subsequently, $\mathrm{𝖢𝗈𝗎𝗇𝗍}$ sets the preprocessed $F$ as the root component, and initializes an empty cache $\zeta$ and an empty assignment $\sigma$. $\mathrm{𝖢𝗈𝗎𝗇𝗍𝖯𝖡𝖬𝖢}$ calls $\mathrm{𝖢𝗈𝗎𝗇𝗍}$ to search the space of assignments and compute the model count. The main computation process of $\mathrm{𝖯𝖡𝖬𝖢}$ in $\mathrm{𝖢𝗈𝗎𝗇𝗍}$ comprises of the following steps – propagation (line 2), conflict handling (lines 3–7), variable decision (lines 11–13), and component decomposition (line 9). As shown in $\mathrm{𝖢𝗈𝗎𝗇𝗍}$, $\mathrm{𝖯𝖡𝖬𝖢}$ starts with propagation so that variable decisions can be inferred and applied. If the propagation leads to a conflict, $\mathrm{𝖯𝖡𝖬𝖢}$ would perform conflict analysis and backjumping using similar techniques as $\mathrm{𝖱𝗈𝗎𝗇𝖽𝗂𝗇𝗀𝖲𝖺𝗍}$ [7] (lines 5–6). If the conflict is a top-level conflict, that is it cannot be resolved by backjumping, $\mathrm{𝖯𝖡𝖬𝖢}$ will terminate and return 0 as the formula is unsatisfiable (line 7). Otherwise, $\mathrm{𝖯𝖡𝖬𝖢}$ would learn a PB constraint that prunes the search space, backjump to the appropriate decision level $d$, and clear the components and recursive calls created after $d$.

If there are no conflicts, $\mathrm{𝖯𝖡𝖬𝖢}$ will attempt to split the current component into variable-disjoint child components, and the count of the current component would be the product of child component counts (lines 9–10). There are two cases of component splitting – (i) there are no new disjoint components and (ii) there are new disjoint components. In case (i) $\mathrm{𝖯𝖡𝖬𝖢}$ will proceed to branch on another variable, and the count of the current component would be the sum of counts from the two branches (lines 12–13). If there are no unassigned variables remaining, the count of the current component would be 1 (line 14). Finally, after completing the implicit search tree exploration $\mathrm{𝖯𝖡𝖬𝖢}$ returns the count of $F$ in cache $\zeta$.

In our top-down PB model counter $\mathrm{𝖯𝖡𝖬𝖢}$, we introduce a variable decision ordering heuristic that we term variable coefficient impact score ($\mathrm{𝖵𝖢𝖨𝖲}$). The intuition for a new variable decision heuristic for PB formulas came from the fact that the coefficient of each literal affects its impact on the overall counting process. Existing variable decision heuristics from CNF model counting literature do not have to consider the impact of coefficients, and therefore modifications are required to adapt to PB model counting. Additionally, tree decomposition may also be less effective when dealing with PB constraints that are relatively longer or constraints that share a lot of variables as in the case of multi-dimensional knapsack problems.

In our $\mathrm{𝖵𝖢𝖨𝖲}$ heuristics, we add a coefficient impact score for each variable as an equal-weighted additional component to prior variable decision heuristics adopted from $\mathrm{𝖦𝖯𝖬𝖢}$. The coefficient impact score for a variable $x$ is given by $\left({\sum }_{j\in {\mathrm{\Omega }}_x}{b}_x^j/k_j\right)÷|{\mathrm{\Omega }}_x|$ where ${\mathrm{\Omega }}_x$ is the set of constraints that variable $x$ appears in, $b_x^j$ is the coefficient of $x$ in constraint $j$, and $k_j$ is the degree of constraint $j$. At the start of the counting process, the score for each variable is computed, and variables are decided in descending order of scores in the counting process. In addition, the phase preferences of variable decisions are set such that the term coefficient with the largest coefficient impact score is applied, this is reflected in line 12 of Algorithm 2. The intuition is that branching on a variable with a larger score would have a greater impact on satisfiability gaps than that on a variable with a smaller score.

After computing the count of each component, we store it in the cache to avoid redundant computations when the same component is encountered in a different branch of the counting process. A component in our caching scheme contains the following information for unique identification – 1) the set of unassigned variables in the component, 2) the set of yet-to-be-satisfied PB constraints in the component, and 3) their current gaps. In our implementation, we stored variables and constraints of a component by their IDs.

We implemented our top-down PB model counter, $\mathrm{𝖯𝖡𝖬𝖢}$, in C++, building on methodologies introduced in the $\mathrm{𝖦𝖯𝖬𝖢}$ CNF model counter and $\mathrm{𝖱𝗈𝗎𝗇𝖽𝗂𝗇𝗀𝖲𝖺𝗍}$ PB solver. We performed comparisons to the existing state-of-the-art PB model counters $\mathrm{𝖯𝖡𝖢𝗈𝗎𝗇𝗍}$ [19] and $\mathrm{𝖯𝖡𝖢𝗈𝗎𝗇𝗍𝖾𝗋}$ [13], and also model counting competition (MCC2024) winner $\mathrm{𝖦𝖺𝗇𝖺𝗄}$ [17]. For consistency, we employed the same benchmark suite as prior work [19]. The suite comprises of 3500 instances across three benchmark sets for PB model counting – Auction (1000 instances), M-dim Knapsack (1000 instances), and Sensor placement (1500 instances). We ran experiments on a cluster with AMD EPYC 7713 CPUs with 1 core and 16 GB memory for each instance and a timeout of 3600 seconds.

Through our evaluations, we seek to understand the performance of our top-down exact PB model counter $\mathrm{𝖯𝖡𝖬𝖢}$. In particular, we investigate the following research questions:

RQ 1:

What is the performance of $\mathrm{𝖯𝖡𝖬𝖢}$ compared to baselines?

RQ 2:

What is the performance impact of our $\mathrm{𝖵𝖢𝖨𝖲}$ heuristic in Section 3.2?

RQ 3:

What is the performance impact of our cache entry optimization in Section 3.3?

We compared $\mathrm{𝖯𝖡𝖬𝖢}$ against the state-of-the-art PB model counter $\mathrm{𝖯𝖡𝖢𝗈𝗎𝗇𝗍}$, which has a bottom-up design, to understand how well a top-down design would perform. The results are shown in Table 1 and the cactus plot of runtime is shown in Figure 1.

Overall, $\mathrm{𝖯𝖡𝖬𝖢}$ is able to return counts for 1849 instances, 76 instances more than that of $\mathrm{𝖯𝖡𝖢𝗈𝗎𝗇𝗍}$, 341 instances more than $\mathrm{𝖯𝖡𝖢𝗈𝗎𝗇𝗍𝖾𝗋}$, and 685 instances more than $\mathrm{𝖦𝖺𝗇𝖺𝗄}$. More specifically, $\mathrm{𝖯𝖡𝖬𝖢}$ leads in auction and M dim-knapsack benchmark sets and came in second in the sensor placement benchmark set. In addition, there are 104 instances that could only be counted by $\mathrm{𝖯𝖡𝖬𝖢}$.

It is worth noting that the sensor placement benchmark instances all have coefficients of 1 or -1, and that for each instance the degree of all but one PB constraint is 1. We also compared $\mathrm{𝖯𝖡𝖬𝖢}$ and $\mathrm{𝖯𝖡𝖢𝗈𝗎𝗇𝗍}$ on a modified version of sensor placement, whereby coefficients are not all 1 or -1 by accounting for potential redundancy requirements and varying costs associated with different sensor placement locations. On the cost-aware sensor placement instances $\mathrm{𝖯𝖡𝖬𝖢}$ outperforms $\mathrm{𝖯𝖡𝖢𝗈𝗎𝗇𝗍}$ by returning counts for 715 instances whereas $\mathrm{𝖯𝖡𝖢𝗈𝗎𝗇𝗍}$ could only return for 678 instances.

We conducted further experiments to understand the impact of our $\mathrm{𝖵𝖢𝖨𝖲}$ heuristic as introduced in Section 3.2. In particular, we compared our implementation of $\mathrm{𝖯𝖡𝖬𝖢}$ with $\mathrm{𝖵𝖢𝖨𝖲}$ against a baseline version of $\mathrm{𝖯𝖡𝖬𝖢}$ that uses the existing variable decision heuristics from the $\mathrm{𝖦𝖯𝖬𝖢}$ model counter. The results are shown in Table 2 and the runtime cactus plot is shown in Figure 2.

In the evaluations, $\mathrm{𝖯𝖡𝖬𝖢}$ with our $\mathrm{𝖵𝖢𝖨𝖲}$ variable decision heuristic ($\mathrm{𝖵𝖢𝖨𝖲}$-heu) is able to return counts for 1849 benchmark instances in total, substantially more than the 1772 benchmark instances when $\mathrm{𝖯𝖡𝖬𝖢}$ is coupled with the existing heuristics from $\mathrm{𝖦𝖯𝖬𝖢}$ ($\mathrm{𝖦𝖯𝖬𝖢}$-heu). In particular, $\mathrm{𝖵𝖢𝖨𝖲}$-heu returned counts for 115 more instances than $\mathrm{𝖦𝖯𝖬𝖢}$-heu in $ℳ$-dim knapsack benchmarks, while losing out 38 instances in Auction benchmarks. Both heuristics performed the same in sensor placement benchmarks. This set of evaluations highlights the tremendous impact of variable decision ordering in the context of PB model counting and demonstrates the performance benefits of our $\mathrm{𝖵𝖢𝖨𝖲}$ variable decision heuristic.

We conducted additional experiments to understand the impact of our optimization for our caching scheme mentioned in Section 3.3, that is modifying the gap value to the smallest coefficient of remaining unassigned variables. We compared $\mathrm{𝖯𝖡𝖬𝖢}$ to a version with cache entry optimization disabled (denoted as $\mathrm{𝖯𝖡𝖬𝖢}$-$\mathrm{𝖭𝖢𝖲}$). We show the number of benchmark instances each configuration could count in Table 3. The result shows that our cache entry optimization technique has a positive impact on the performance of $\mathrm{𝖯𝖡𝖬𝖢}$, although less significant than $\mathrm{𝖵𝖢𝖨𝖲}$ heuristics in the previous set of experiments.

In RQ 1, $\mathrm{𝖯𝖡𝖬𝖢}$ demonstrated a significant lead over state-of-the-art competitors. In the process, we observed that $\mathrm{𝖯𝖡𝖬𝖢}$ performs better on PB instances with coefficients that are not just 1, as evident in the sensor placement benchmark set. In RQ 2, we showed the need for heuristics to consider PB-specific features such as coefficients through the significant performance improvement that $\mathrm{𝖵𝖢𝖨𝖲}$ enabled. We also observed that the top-down approach is rather sensitive to variable decision heuristics. Finally, in RQ 3 we showed that by simply optimizing cache entries, one can get noticeable performance improvements.