ALLSAT compressed with wildcards: From CNF's to orthogonal DNF's by imposing the clauses one by one

TL;DR

This paper introduces a novel method for converting Boolean CNF formulas into orthogonal DNF forms by sequentially imposing clauses, leveraging wildcards and parallelization to improve compression, especially for formulas with few large clauses.

Contribution

The paper presents a new clause-imposition technique for CNF to orthogonal DNF conversion that enables parallel processing and enhanced compression using wildcards, extending to superclauses.

Findings

Efficient for CNFs with few large clauses

Wildcards improve output compression

Parallelization potential enhances performance

Abstract

We present a novel technique for converting a Boolean CNF into an orthogonal DNF, aka exclusive sum of products. Our method (which will be pitted against a hardwired command from Mathematica) zooms in on the models of the CNF by imposing its clauses one by one. Clausal Imposition invites parallelization, and wildcards beyond the common don't-care symbol compress the output. The method is most efficient for few but large clauses. Generalizing clauses one can in fact impose superclauses. By definition, superclauses are obtained from clauses by substituting each positive litereal by an arbitrary conjunction of positive literals.