Disjoint Partial Enumeration without Blocking Clauses
Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
TL;DR
This work tackles disjoint AllSAT by eliminating blocking clauses and instead integrating CDCL, Chronological Backtracking, and Implicant Shrinking to enumerate disjoint partial models. The authors implement TabularAllSAT and demonstrate through benchmarks that combining these techniques yields superior performance on most instances, avoiding the memory and propagation bottlenecks of blocking clauses. Their approach leverages 2-Watched Literals for efficient shrinking and introduces virtual backtrack reasons to support conflict analysis without dense clause storage. The results suggest practical scalability for disjoint partial enumeration and point to future directions in knowledge compilation comparisons and advanced heuristics.
Abstract
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.