A basic algorithm for enumerating disjoint propositional models (disjoint AllSAT) is based on adding blocking clauses incrementally, ruling out previously found models. On the one hand, blocking clauses have the potential to reduce the number of generated models exponentially, as they can handle partial models. On the other hand, they need exponential space and slow down unit propagation. We propose a new approach that allows for enumerating disjoint partial models with no need for blocking clauses by integrating: Conflict-Driven Clause-Learning (CDCL), Chronological Backtracking (CB), and methods for shrinking models (Implicant Shrinking). Experiments clearly show the benefits of our novel approach.

翻译：一种基本的枚举不相交命题模型（不相交AllSAT）算法基于逐步添加阻塞子句，以排除先前找到的模型。一方面，阻塞子句有潜力指数级减少生成的模型数量，因为它们能够处理部分模型。另一方面，它们需要指数级空间并减缓单元传播。我们提出了一种新方法，通过集成冲突驱动子句学习（CDCL）、时序回溯（CB）以及模型缩减方法（蕴含项缩减），能够在无需阻塞子句的情况下枚举不相交部分模型。实验明显展示了我们新方法的优势。