Dual edge operations in reduced ordered binary decision diagrams

The use of input and output negation in reducing the size of ROBDDs has been well investigated. Here we consider duality, a fundamental property of Boolean functions, and how it can be used to further reduce ROBDD size. We show how to introduce dual edge markers into a ROBDD package with effectively no storage overhead and a very small increase in per node processing cost. Our 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. We consider the variable reordering problem and sifting in particular. We show that dual markers can not be used directly in sifting, but show that there is substantial advantage in applying sifting to an ROBDD with output negations, followed by a second phase where dual markers are used to reduce the size of the ROBDD