next up previous contents
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