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
 A: 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
