Negation and duality in reduced ordered binary decision diagrams

The use of input and output negation in reducing the size of ROBDDs has been well investigated. We consider duality, a fundamental property of Boolean functions, and how it can be used to reduce ROBDD size. Dual markers are added to certain edges in an ROBDD and we show this can be done with effectively no storage overhead and a very small increase in per node processing cost. Using dual markers in conjunction with output inverters is compared to using neither and to output inverters alone. Our preliminary experimental results show that dual markers can reduce the size of the ROBDD, sometimes quite substantially, and even in cases where they offer little reduction, can still lead to increased overall processing speed. The relation of dual markers to input inverters is discussed and a simple technique that allows either to be incorporated in variable ordering optimization methods based on adjacent variable interchange, e.g. sifting, is introduced