

![0_image_0.png](0_image_0.png)

reached leaf node is labeled with the resulting truth value. If v is a BDD, its size [v] is the nmber of its nodes. If n is a node, var ( n ) indicates the variable indexing node n .

BDDs are a canonical representation of Boolean functions. The canonicity follows by imposing a total order < over the set of variables used to label nodes, such that for any node n and respective non-terminal child m , their variables must be ordered, i.e. var(n) < var(m), and requiring that the Bdd contains no isomorphic subgraphs.

BDDs can be combined with the usual boolean transformations (e.g. negation, conjunction, disjunction). Given two BDDs, for instance, the conjunction operator builds and returns the BDD corresponding to the conjunction of its arguments. Substitution can also be represented as BDD transformations. In the following, if v is a variable, and Φ and ψ are BDDs, we indicate with Φ [v/ψ] the BDD resulting from the substitution of v with ψ in Φ . If v1 and v2 are vectors of (the same number of) distinct variables, we indicate with Φ [v1/v2] the parallel substitution in Φ of the variables in vector v1 with the (corresponding) variables in v2.

BDDS also allow for transformations described as quantifications, in the style of Quantified Boolean Formulae (QBF). QBF is a definitional extension to propositional logic, where propositional variables can be universally and existentially quantified. In terms of BDD computations, a quantification corresponds to a tranformation mapping the BDD of Φ and the variable vi being quantified into the BDD of the resulting (propositional) formula. If Φ
is a formula, and vi is one of its variables, the existential quantification of vi in Φ, written 3vi Φ(v 1 , . . ,vn), is equivalent to Φ(v 1 , . . ,vn)[vi/False] V Φ(v 1 , . . ,vn)[vi/True], Analogously, the universal quantification ∀ v i Φ(v 1 , . . , v n ) is equivalent to Φ(v 1 , . . , v n )[v i /Fal se] Λ