Enumerating models of DNF faster: breaking the dependency on the formula size
Florent Capelli, Yann Strozecki
TL;DR
The paper advances the study of enumerating DNF models by aiming for delays tied to model size rather than formula size, and provides substantial results for two key subclasses: a constant-delay amortized algorithm for fixed-size (k-)DNF terms and a quadratic-delay method for monotone DNFs. It develops and analyzes three classical enumeration approaches (union of terms, flashlight/backtrack, and Gray-code per-term enumeration), and then introduces amortized analyses to achieve sublinear average delay in the formula size, with gamma = log_3(2). For k-DNF, a backtracking technique with careful precomputation yields delays of 2^{O(k)}, and for monotone DNFs, polynomial-space methods achieve average delays of O(n^2) or even O(log(mn)) under refined representations. These results illuminate the boundary between strong polynomial delay and ordinary polynomial delay in DNF enumeration and suggest broader applicability to similar union-based enumeration problems.
Abstract
In this article, we study the problem of enumerating the models of DNF formulas. The aim is to provide enumeration algorithms with a delay that depends polynomially on the size of each model and not on the size of the formula, which can be exponentially larger. We succeed for two subclasses of DNF formulas: we provide a constant delay algorithm for $k$-DNF with fixed $k$ by an appropriate amortization method and we give a quadratic delay algorithm for monotone formulas. We then focus on the \emph{average delay} of enumeration algorithms and show how to obtain a sublinear delay in the formula size.