WME: Extending CDCL-based Model Enumeration with Weights
This work establishes WME as a solver-level reasoning task for applications requiring weight-driven queries, such as top-k model generation, but it is incremental as it builds on existing CDCL and enumeration techniques.
The paper tackles the problem of Weighted Model Enumeration (WME) for Boolean formulas, introducing CDCL-based algorithms with weight propagation and pruning to efficiently enumerate models based on weights, showing feasibility and trade-offs between chronological and non-chronological backtracking approaches.
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.