Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

WME: Extending CDCL-based Model Enumeration with Weights

Giuseppe Spallitta, Moshe Y. Vardi

TL;DR

This work establishes WME as a solver-level reasoning task and provides a systematic exploration of its algorithmic foundations, highlighting trade-offs in pruning effectiveness with weights and clarifying when each performs best.

Abstract

In this work we investigate Weighted Model Enumeration (WME): given a Boolean formula and a weight function over its satisfying assignments, enumerate models while accounting for their weights. This setting supports weight-driven queries, such as producing the top-k models or all models above a threshold. While related to AllSAT, Weighted Model Counting, and MaxSAT, these paradigms do not treat selective enumeration under weights as a native solver task. We present CDCL-based algorithms for WME that integrate weight propagation, weight-based pruning, and weight-aware conflict analysis into both chronological and non-chronological backtracking frameworks. Chronological backtracking exploits implicit blocking and keeps the clause database compact, thereby reducing memory footprint and enabling efficient propagation. In contrast, non-chronological backtracking with clause learning supports explicit blocking and restarts. We show that both approaches are feasible and complementary, highlighting trade-offs in pruning effectiveness with weights and clarifying when each performs best. This work establishes WME as a solver-level reasoning task and provides a systematic exploration of its algorithmic foundations.

WME: Extending CDCL-based Model Enumeration with Weights

TL;DR

This work establishes WME as a solver-level reasoning task and provides a systematic exploration of its algorithmic foundations, highlighting trade-offs in pruning effectiveness with weights and clarifying when each performs best.

Abstract

In this work we investigate Weighted Model Enumeration (WME): given a Boolean formula and a weight function over its satisfying assignments, enumerate models while accounting for their weights. This setting supports weight-driven queries, such as producing the top-k models or all models above a threshold. While related to AllSAT, Weighted Model Counting, and MaxSAT, these paradigms do not treat selective enumeration under weights as a native solver task. We present CDCL-based algorithms for WME that integrate weight propagation, weight-based pruning, and weight-aware conflict analysis into both chronological and non-chronological backtracking frameworks. Chronological backtracking exploits implicit blocking and keeps the clause database compact, thereby reducing memory footprint and enabling efficient propagation. In contrast, non-chronological backtracking with clause learning supports explicit blocking and restarts. We show that both approaches are feasible and complementary, highlighting trade-offs in pruning effectiveness with weights and clarifying when each performs best. This work establishes WME as a solver-level reasoning task and provides a systematic exploration of its algorithmic foundations.
Paper Structure (19 sections, 2 theorems, 23 equations, 4 figures, 4 tables, 4 algorithms)

This paper contains 19 sections, 2 theorems, 23 equations, 4 figures, 4 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Contributions
  3. Related Work
  4. Weighted Model Enumeration
  5. Comparison to Existing Approaches
  6. Integrating Weight Reasoning into CDCL-Based Frameworks
  7. Weight Propagation and Pruning
  8. Weight Conflict Analysis
  9. Residual-Aware Backtracking for Top-$k$ Enumeration
  10. Weight-based Variable Priority for Top-$k$ Enumeration
  11. Chronological vs. Non-Chronological Backtracking
  12. Chronological Backtracking Framework
  13. Non-Chronological Backtracking Framework
  14. Experimental Evaluation
  15. Benchmarks
  16. ...and 4 more sections

Key Result

Proposition 3

Let $\mu$ be any partial trail reachable by the main CDCL loop, and let $w(\mu)$ and $I_{\max}(\mu)$ be maintained as in Algorithm algo:weights. Then: In particular, if $\textsc{WeightConflict}(\mu)$ returns true, i.e., $w(\mu) \cdot I_{\max}(\mu) < \theta$, then no completion $\eta \supseteq \mu$ can satisfy $w(\eta) \ge \theta$.

Figures (4)

  • Figure 1: Top-1 enumeration results of the two WME frameworks on synthetic and real benchmarks. Notice that in all scatter plots the axes are log-scaled.
  • Figure 2: Top-$k$ enumeration experiments. Left & center: top-1 performance of WME-NCB compared with state-of-the-art solvers. Right: median runtime of native top-$k$ enumeration in WME-NCB compared with a baseline obtained by repeating the top-1 procedure.
  • Figure 4: Timeout statistics for thresholded WME framework variants on rnd3sat-1.5.
  • Figure 4: Ablation studies. Left: threshold-based enumeration. Right: top-$1$ enumeration.

Theorems & Definitions (9)

  • Definition 1: Weighted Model Enumeration
  • Remark 2
  • Proposition 3: Weight pruning soundness
  • Example 4
  • Definition 5: Weight conflict
  • Proposition 6: Soundness of greedy weight-conflict learning
  • Example 7
  • Example 8
  • Example 9