ALLSAT compressed with wildcards. Part 1: Converting CNF's to orthogonal DNF's. (arXiv:1608.08472v2 [cs.AI] UPDATED)

For most branching 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.

from cs.AI updates on arXiv.org http://ift.tt/2cpCOv1
via IFTTT