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

TL;DR

This paper introduces an algorithm called A-I-I that efficiently enumerates all G-independent order ideals in a poset, and extends to a polynomial-time method for enumerating models of any Boolean 2-CNF, with practical advantages over existing tools.

Contribution

The paper presents a novel algorithm, A-I-I, capable of enumerating G-independent order ideals and Boolean 2-CNF models in a compressed format, improving efficiency and parallelizability.

Findings

A-I-I outperforms Mathematica's BooleanConvert and SatisfiabilityCount in many cases.

A-I-I can be parallelized for better performance.

The algorithm extends to polynomial-time enumeration of Boolean 2-CNF models.

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.