Compression with wildcards: All models of a Boolean 2-CNF

TL;DR

Compression with wildcards introduces All-Independent-Ideals (A-I-I), a compressed enumeration framework for Boolean $2$-CNFs that represents the model set as a disjoint union of 012-rows. The method first reduces general $2$-CNFs to Horn form via Horn-renaming, then to acyclic Horn instances that A-I-I can handle, yielding polynomial-total-time enumeration with complexity $O(R w^3)$ in the compressed representation. Empirical results show competitive compression relative to general tools and highlight parallelization benefits, memory considerations, and the practical utility of outputting partial results. The paper also discusses extending the approach with wildcards beyond don’t-cares for homogeneous cases and situates the algorithm within the broader All-SAT landscape through a survey of alternative methods and strategies.

Abstract

Let $W$ be a finite set which simultaneously serves as the universe of any poset $(W,\preceq)$ and as the vertex set of any graph $G$. Our algorithm, abbreviated A-I-I, enumerates (in a compressed format using don't-care symbols) all $G$-independent order ideals of $(W,\preceq)$. For many instances the high-end Mathematica implementation of A-I-I compares favorably to the hardwired Mathematica commands {\tt BooleanConvert} and {\tt SatisfiabilityCount}. The A-I-I can be parallelized and adapts to a polynomial total time algorithm that enumerates the modelset of any Boolean 2-CNF.