** Next:** Rewind
** Up:** Reference - Preprocessing
** Previous:** Clustering + Existential Quantification
** Contents**

##

Dependent variable clustering

Equations such as the following:

`x = and(a, b, c, d, ...)`

`x = or(a, b, c, d, ...)`

appear often in many applications, particularly those related to
circuits. In such a case, the BDD corresponding to the equation is
conjoined with all other BDDs containing variable , the variable
appearing on the left side of equals, and then is existentially
quantified out of the expression entirely. For example, the
equations

`x = and(a, b, c, d)`

`y = and(x, e, f, g)`

are replaced by

`y = and(a, b, c, d, e, f, g)`

and is eliminated.

As it currently exists in the tool, this operation is limited to cases
where the BDDs involved all depend on 8 or fewer variables unless the
BDDs are special functions and can be conjoined to a SMURF which
is reasonably small in size.

John Franco
2011-09-15