WME: Extending CDCL-based Model Enumeration with Weights

This paper introduces Weighted Model Enumeration (WME) as a distinct solver-level task and presents complementary CDCL-based algorithms that integrate weight propagation, pruning, and conflict analysis into both chronological and non-chronological backtracking frameworks to efficiently enumerate weighted models.

The Gist

Imagine you are a talent scout looking for the best actors for a movie.

In the old days, computer programs (called "SAT solvers") were like scouts who would just find any actor who could read a line. They didn't care if the actor was a superstar or a nobody; they just wanted someone who fit the script. This is called AllSAT.

Other programs were like accountants. They could tell you the total box office potential of the entire cast, but they couldn't tell you who the specific stars were. This is Weighted Model Counting.

And some programs were like directors who only wanted the single best actor for the lead role. They would find the "Most Probable Explanation" (the best one) and stop. This is MaxSAT.

But what if you want to find the Top 10 best actors, or every actor whose "star power" score is above a certain number? You need a new kind of scout. This paper introduces WME (Weighted Model Enumeration).

Here is how the authors built this new scout, explained through a few simple metaphors:

1. The "Star Power" Score

Imagine every actor has a "Star Power" score (a weight).

• If you cast Actor A, you get 0.8 stars.
• If you cast Actor B, you get 0.2 stars.
• The total score of your movie is the product of all the actors you cast.

The goal of WME is to find all the movie casts that work (satisfy the script) and have a high enough total star power.

2. The "Magic Compass" (Weight Propagation)

The biggest problem with finding high-scoring casts is that there are billions of possibilities. Checking them one by one takes forever.

The authors gave their solver a Magic Compass.

• As the solver starts picking actors, the Compass calculates the maximum possible score the current cast could ever reach if they picked the absolute best remaining actors.
• The Trick: If the Compass says, "Even if you pick the best remaining actors, your total score will only be 0.1, but you need 0.5 to make the cut," the solver immediately stops. It doesn't waste time checking the rest of that path.
• This is called Weight-Based Pruning. It's like realizing halfway through a hike that you won't reach the summit before sunset, so you turn back immediately instead of walking the whole way.

3. The "Do-Not-Enter" Signs (Conflict Analysis)

When the solver realizes a path is a dead end (too low a score), it doesn't just turn back; it puts up a "Do-Not-Enter" sign (a learned clause) on that path.

• Next time the solver sees a similar situation, it sees the sign and skips that whole area instantly.
• This prevents the solver from making the same mistake twice.

4. Two Different Ways to Walk the Maze

The paper explores two different strategies for how the solver moves through the possibilities, like two different hiking styles:

Strategy A: The "Backtracker" (Chronological)

• How it works: This solver walks forward. If it hits a wall, it takes one step back, tries the other door, and keeps going. It doesn't jump far back.
• Pros: It uses very little memory (like a small backpack). It's very fast at finding many solutions if the "good" solutions are everywhere.
• Cons: It can get stuck in a bad neighborhood for a long time if it makes a wrong turn early on. It's sensitive to the order in which it checks things.

Strategy B: The "Teleporter" (Non-Chronological)

• How it works: This solver is aggressive. If it hits a wall, it analyzes why it hit the wall, puts up a big "Do-Not-Enter" sign, and teleports (backjumps) way back to the beginning of the problem to try a completely different path.
• Pros: It's great at finding the single best solution or the top few solutions quickly. It learns from its mistakes and reorganizes its search to avoid bad areas.
• Cons: It carries a heavy backpack (lots of memory) because it keeps all those "Do-Not-Enter" signs. If you need to find thousands of solutions, the backpack gets too heavy, and it slows down.

5. The Results: Which Strategy Wins?

The authors tested these two strategies on different types of problems:

• Scenario 1: "Find the Top 10 Stars" (Top-k)

  • Winner: The Teleporter (Non-Chronological).
  • Why: You want the best ones fast. The Teleporter quickly eliminates the "bad" actors and focuses on the "stars," using its heavy backpack of signs to prune the search space efficiently.

• Scenario 2: "Find Everyone with a Score Above 0.5" (Threshold)

  • Winner: The Backtracker (Chronological).
  • Why: There are so many valid solutions that you don't want to carry a heavy backpack of signs. The Backtracker is lightweight and can sweep through the "good" area quickly without getting bogged down by too many rules.

The Big Takeaway

This paper is like a manual for a new kind of smart search engine. It teaches computers how to not just find answers, but to find the best answers (or all answers above a certain quality) much faster than before.

By combining the logic of "finding a solution" with the math of "scoring a solution," they created a tool that can handle complex tasks like:

• AI Decision Making: "Show me the top 3 reasons why this system failed."
• Medical Diagnosis: "List all possible disease combinations that explain these symptoms with high probability."
• Database Queries: "Show me the top 100 most relevant search results."

The authors essentially built a smart filter that sits inside the computer's brain, letting it ignore the "junk" answers instantly and focus only on the "gold."

Technical Summary

Here is a detailed technical summary of the paper "WME: Extending CDCL-based Model Enumeration with Weights" by Giuseppe Spallitta and Moshe Y. Vardi.

1. Problem Definition: Weighted Model Enumeration (WME)

The paper addresses a gap in automated reasoning where existing solvers fail to natively support the enumeration of "high-quality" models based on a weight function.

• Context: In applications like probabilistic inference, fault diagnosis, and interpretable machine learning, users often need more than just any satisfying assignment (AllSAT) or a single optimal assignment (MaxSAT). They require a ranked list of models (Top-k) or all models exceeding a specific weight threshold.
• Limitations of Existing Approaches:
  • AllSAT: Enumerates all models indiscriminately, ignoring weights. Post-hoc filtering is computationally prohibitive for large solution spaces.
  • Weighted Model Counting (WMC): Computes aggregate weights but does not expose individual models.
  • MaxSAT: Finds a single maximum-weight solution but lacks native mechanisms for ranking multiple alternatives or incremental threshold-based enumeration.
• Formal Definition: Given a Boolean formula $F$ and a weight function $w$ over literals, WME aims to enumerate the set $M_w(F) = \{(\eta, w(\eta)) \mid \eta \models F\}$, where $w(\eta) = \prod_{\ell \in \eta} w(\ell)$. The goal is to support Threshold WME (all $\eta$ where $w(\eta) \ge \theta$) and Top-k WME (the $k$ models with the highest weights).

2. Methodology: Integrating Weights into CDCL

The authors propose a CDCL-based framework that integrates weight reasoning directly into the search loop, rather than treating it as a post-processing step. The core mechanisms include:

A. Weight Propagation and Pruning

The solver maintains two values during the search:

1. Partial Weight ($w(\mu)$): The product of weights of assigned literals in the current trail $\mu$.
2. Optimistic Residual Bound ($I_{max}(\mu)$): The product of the maximum possible weights ($best(A) = \max(w(A), w(\neg A))$) for all unassigned variables.

Pruning Logic: If $w(\mu) \cdot I_{max}(\mu) < \theta$, the current branch cannot possibly reach the threshold $\theta$, even under the most optimistic completion. This triggers a Weight Conflict, allowing the solver to prune the branch early.

B. Weight Conflict Analysis

When a weight conflict is detected, the solver performs conflict analysis to generate a Weight-Conflict Clause ($C_w$).

• Mechanism: A greedy algorithm selects a subset of literals $S \subseteq \mu$ with the lowest weight contributions such that their removal (or negation) explains why the threshold cannot be met.
• Result: A clause $C_w = \bigvee_{\ell \in S} \neg \ell$ is learned. This prevents the solver from revisiting the specific combination of literals that led to an infeasible weight, similar to how standard CDCL learns clauses from Boolean conflicts.

C. Residual-Aware Backtracking

In Top-k enumeration, finding a new high-weight model tightens the threshold $\theta$.

• Instead of backtracking chronologically or to the first UIP immediately, the solver uses the residual bound to determine the deepest decision level from which a better solution is still possible.
• If $w(\mu) \cdot I_{max}(\mu) \le \theta$ at a certain level, the solver backtracks past that level immediately, skipping irrelevant subspaces.

D. Variable Prioritization

The framework distinguishes between weight-relevant and weight-irrelevant variables (e.g., Tseitin variables with symmetric weights). The branching heuristic prioritizes weight-relevant variables to tighten bounds faster, deferring the assignment of irrelevant variables until necessary.

3. Key Contributions

1. Formalization of WME: Defined as a distinct solver-level task generalizing AllSAT, WMC, and MaxSAT.
2. Algorithmic Extensions: Introduced weight-aware propagation, pruning, and conflict analysis integrated into the CDCL loop.
3. Dual Frameworks: Developed and compared two distinct backtracking strategies:
   • Chronological Backtracking (WME-CB): Uses implicit blocking (traversal order prevents revisiting). Low memory footprint, fast propagation, but sensitive to decision order.
   • Non-Chronological Backtracking (WME-NCB): Uses explicit blocking clauses and restarts. Robust to decision order, effective for Top-k, but incurs higher memory and propagation overhead.
4. Empirical Validation: Comprehensive evaluation on synthetic and real-world benchmarks (Bayesian networks, SATLIB).

4. Experimental Results

The authors implemented both variants (WME-CB and WME-NCB) atop the CaDiCaL solver and compared them against state-of-the-art tools (DPO, MaxHS) and iterative baselines.

• Top-k Enumeration:
  • WME-NCB significantly outperformed WME-CB and competitors (DPO, MaxHS) on most benchmarks.
  • The ability to learn weight-conflict clauses and use restarts allowed WME-NCB to rapidly tighten bounds and prune large search spaces.
  • Native Top-k enumeration was found to be more efficient than iteratively calling Top-1 with blocking, as it reuses accumulated search information.
• Threshold-Based Enumeration:
  • WME-CB outperformed WME-NCB, particularly on instances with dense solution spaces.
  • In scenarios requiring the enumeration of many models, the memory overhead and propagation cost of explicit blocking clauses in WME-NCB became a bottleneck. Chronological traversal proved more efficient here.
• Ablation Studies: Disabling weight-based pruning resulted in substantial performance degradation, confirming that early weight-driven pruning is essential for WME.

5. Significance and Conclusion

This work establishes Weighted Model Enumeration as a native reasoning task for modern SAT solvers.

• Theoretical Impact: It bridges the gap between model counting, optimization, and enumeration, showing that weight constraints can be handled natively within CDCL without resorting to knowledge compilation or external filtering.
• Practical Impact: Provides a unified framework for applications requiring ranked explanations or threshold-based filtering (e.g., "Show me the top 5 most probable system failures").
• Design Insight: The paper highlights a critical trade-off: Non-chronological backtracking is superior for finding a few high-quality solutions (Top-k) due to aggressive pruning via learned clauses, while chronological backtracking is superior for exhaustive enumeration of many solutions (Threshold) due to lower memory and propagation overhead.
• Future Directions: The authors suggest making solvers adaptive to switch between these strategies based on instance characteristics and extending WME to SMT (Satisfiability Modulo Theories) for richer background theories.