Better compression for a positive DNF than via BDD

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?

Bye

-

Meanwhile I found an algorithm by myself. The first thing I did was the implementation of an algorithm that detects common tails in binary decision diagrams.

The first compression worked by detecting:

(A&B v ~A&false)    --> (A&true v ~A&false)& B  % common tail
(A&B&C v ~A&D&C)    -->     (A&B v ~A&D)& C     % common tail


As a next step I tried a further compression. Instead of detecting common tails, I implemented an algorithm that detects common paths in binary decision diagrams.

The second compression worked by detecting:

(A&B1&C1,..&Bn&Cn v ~A&D1&C1&..&Dn&Cn) -->
(A&B1&..&Bn v ~A&D1&..&Dn)& C1&..&Cn    % common path


I then did a little benchmark. We used 100’000 randomly picked Boolean functions and computed their compression. We observed an average size reduction of only 2%.

So for evenly distributed Boolean functions it doesn't seem worth it. Maybe if the Boolean functions have already some shape it might give something.

Bye

P.S.: The Prolog source code:
Ordinary Binary Decision Diagrams
http://www.xlog.ch/jekejeke/principia/shannon.p

Compressed Binary Decision Diagrams
http://www.xlog.ch/jekejeke/principia/shannon4.p

-