Least Upper Bounds for the Size of OBDDs using Symmetry Properties.
L. Heinrich-Litan and P. Molitor.
|Published||In IEEE Transactions on Computers, vol.49, no.4, pp.360-368, April 2000.|
The paper investigates reduced ordered binary decision diagrams (OBDD) of
partially symmetric Boolean functions when using variable orders where
symmetric variables are adjacent. We prove upper bounds for the size
of such symmetry ordered OBDDs (SymOBDD). They generalize the upper bounds for
the size of OBDDs of totally symmetric Boolean functions and non-symmetric
functions proven by Heap (1993, 1994) and Wegener (1984). Experimental
results based on these upper bounds show that the nontrivial symmetry sets
of a Boolean function should be located either right up at the beginning
or right up at the end of the variable order to obtain best upper bounds.