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, the introduction of a large number of blocking clauses affects memory consumption and drastically slows 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）和模型收缩方法（蕴含项收缩），无需阻塞子句即可枚举不相交的部分模型。实验清楚地证明了我们新颖方法的优势。