REDUCTION OF OBDDS IN LINEAR-TIME

Ordered binary decision diagrams (OBDDs) play an important role as dat a structure for Boolean functions. They are used, e.g., in the logical synthesis process, for verification and test pattern generation, and as part of CAD tools. For a given ordering of the variables and a give n Boolean function f the reduced OBDD, i.e. the OBDD of minimal size, is unique (up to isomorphisms) and can be computed from any OBDD G for f of size \G\ in time O(\G\ log \G\). A new reduction algorithm which works in optimal linear time O(\G\) is presented.