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.

翻译：本文研究了带权模型枚举（Weighted Model Enumeration, WME）问题：给定一个布尔公式及其在满足赋值上的权函数，在枚举模型的同时考虑其权重。这一设定支持权重驱动的查询，例如生成top-k模型或所有权重超过阈值的模型。虽然WME与AllSAT、带权模型计数（Weighted Model Counting）和MaxSAT相关，但这些范式并未将权重下的选择性枚举作为原生求解器任务处理。我们提出了基于CDCL的WME算法，该算法将权重传播、基于权重的剪枝和权重感知的冲突分析集成到时间回溯与非时间回溯框架中。时间回溯利用隐式阻塞并保持子句数据库紧凑，从而减少内存占用并实现高效传播。相反，带子句学习的非时间回溯支持显式阻塞和重启。我们证明两种方法均可行且互补，突出了权重下剪枝有效性的权衡，并阐明了各自的最佳适用场景。