ALLSAT compressed with wildcards: An invitation for C-programmers

TL;DR

This paper introduces a new wildcard-based compression method for Boolean function models in CNF, aiming to improve efficiency and visualization, with initial promising results compared to existing techniques.

Contribution

It presents a novel wildcard-based compression approach for Boolean functions in CNF, emphasizing visual interpretability and potential for implementation in C.

Findings

Preliminary results show promising comparison with BDDs and ESOP.

Method offers a visual and intuitive way to understand Boolean models.

Further C implementation needed for systematic benchmarking.

Abstract

The model set of a general Boolean function in CNF is calculated in a compressed format, using novel wildcards. This method can be explained in very visual ways. Preliminary comparison with existing methods (BDD's and Mathematica's ESOP command) looks promising but our algorithm begs for a C encoding which would render it comparable in more systematic ways.