Φ(v 1 , . . , v n )[v i /True]. In QBF, quantifiers can be arbitrarily applied and nested. In general, a QBF formula has an equivalent propositional formula, but the conversion is subject to an exponential blow-up.

The time complexity of the algorithm for computing a truth-functional boolean transformation fi < op> f2 is O ( fi | · | f2 |). As far as quantifications are concerned, the time complexity is quadratic in the size of the BDD being quantified, and linear in the number of variables being quantified, i.e. O ( \ / | 2 ) (Bryant, 1992, 1986).

BDD packages are efficient implementations of such data structures and algorithms (Brace et al., 1990; Somenzi, 1997; Yang et al., 1998; Coudert et al., 1993). Basically, a BDD package deals with a single multi-rooted DAG, where each node represents a boolean function.

Memory efficiency is obtained by using a "unique table", and by sharing common subgraphs between BDDs. The unique table is used to guarantee that at each time there are no isomorphic subgraphs and no redundant nodes in the multi-rooted DAG. Before creating a new node, the unique table is checked to see if the node is already present, and only if this is not the case a new node is created and stored in the unique table. The unique table allows to perform the equivalence check between two BDDs in constant time (since two equivalent functions always share the same subgraph) (Brace et al., 1990; Somenzi, 1997).

Time efficiency is obtained by maintaining a "computed table", which keeps track of the results of recently computed transformations, thus avoiding the recomputation.

A critical computational factor with BDDs is the order of the variables used. (Figure 6 shows an example of the impact of a change in the variable ordering on the size of a BDD.)
For a certain class of boolean functions, the size of the corresponding BDD is exponential in the number of variables for any possible variable ordering (Bryant, 1991). In many practical cases, however, finding a good variable ordering is rather easy.  Beside affecting the memory used to represent a Boolean function, finding a good variable ordering can have a big impact on computation times, since the complexity of the transformation algorithms depends on the size of the operands. Most BDD packages provide heuristic algorithms for finding good variable orderings, which can be called to try to reduce the overall size of the stored BDDs.

The reordering algorithms can also be activated dynamically by the package, during a BDD computation, when the total number of nodes in the package reaches a predefined threshold (dynamic reoredering).

## 5.2  Symbolic Representation Of Planning Domains

A planning domain ( P, S, A, R ) can be represented symbolically using Bdds, as follows. A set of (distinct) BDD variables, called state variables, is devoted to the representation of the states S of the domain. Each of these variables has a direct association with a proposition of the domain in P used in the description of the domain. For instance, for the BTUC
domain, each of In 1 , Defused and Clogged is associated with a unique BDD variable. In the following we write x for the vector of state variables. Because the particular order is irrelevant but for performance issues, in the rest of this section we will not distinguish a proposition and the corresponding BDD variable.

A state is a set of propositions of P (specifically, the propositions which are intended to hold in it). For each state s, there is a corresponding assignment to the state variables x , i.e. the assignment where each variable corresponding to a proposition p E s is assigned