I am experimenting with compressing positive disjunctive normal form (DNF). When I use binary decision diagrams (BDDs) related algorithms I don't get very good results. For example the algorithms for BDDs that use sharing, it would still show similar branches during printing and/or introduce new prepositional variables, both things are not desired:
Example: Compression (Bad) Input: (p & q & s & t) v (p & r & s & t) v (p & q & s & u) v (p & r & s & u) v w. Output: (p & ((q & s & (t v u)) v (r & s & (t v u)))) v w. - or - Output: (p & ((q & h) v (r & h)) & (h <-> s & (t v u))) v w.
The result should be a single formula, not anymore DNF, which is more compact than the binary decision diagram algorithms which uses only disjunction and conjunction, and the prepositional variables already found in the original DNF. Here is an example of the desired compression:
Example: Compression (Good) Input: (p & q & s & t) v (p & r & s & t) v (p & q & s & u) v (p & r & s & u) v w. Output: (p & (q v r) & s & (t v u)) v w.
Do such algorithms exits? Are they time or space intensive?