ALLSAT compressed with wildcards. Part 1: Converting CNF's to orthogonal DNF's.
Marcel Wild · arXiv (Cornell University) · 2016
For most algorithms in Boolean logic branching means variable-wise branching. We present the apparently novel technique of clause-wise branching, which is used to solve the ALLSAT problem for arbitrary Boolean functions in CNF format. Specifically, it converts a CNF into an orthogonal DNF, i.e. into an exclusive sum of products. Our method is enhanced by two ingredients: The use of a good SAT-solver and wildcards beyond the common don't-care symbol.