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

##

Clustering + Existential Quantification

This preprocessing function conjoins BDDs so that at least one
variable can be existentially quantified away from the entire
collection. This operation repeatedly finds the variable that occurs
in the least number of BDDs, conjoins those BDDs, and, if the number
of variables in the result is less than a hard-wired constant (called
MAX_EXQUANTIFY_VARLENGTH in the code), existentially quantifies that
variable away from the resulting BDD. The operation ends when the
lowest number of BDDs a variable occurs in is greater than some
hard-wired constant (right now called MAX_EXQUANTIFY_CLAUSES in the
source code).

John Franco
2011-09-15