Extending CDCL-based Model Enumeration with Weights

TL;DR

This paper introduces CDCL-based algorithms for Weighted Model Enumeration, enabling efficient weight-aware enumeration of models with different backtracking strategies and trade-offs.

Contribution

It extends CDCL algorithms to handle weighted enumeration, integrating weight propagation and pruning for the first time in this context.

Findings

Both chronological and non-chronological backtracking are feasible for WME.

Chronological backtracking reduces memory footprint and improves propagation.

Non-chronological backtracking supports explicit blocking and restarts.

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.