Disjoint Partial Enumeration without Blocking Clauses

A basic algorithm for enumerating disjoint propositional models (disjointAllSAT) is based on adding blocking clauses incrementally, ruling outpreviously found models. On the one hand, blocking clauses have the potentialto reduce the number of generated models exponentially, as they can handlepartial models. On the other hand, the introduction of a large number ofblocking clauses affects memory consumption and drastically slows down unitpropagation. We propose a new approach that allows for enumerating disjoint partial modelswith no need for blocking clauses by integrating: Conflict-DrivenClause-Learning (CDCL), Chronological Backtracking (CB), and methods forshrinking models (Implicant Shrinking). Experiments clearly show the benefitsof our novel approach.