next up previous index
Next: Grouping Variables Up: User's Manual Previous: Converting BDDs to ZDDs

Variable Reordering for BDDs and ADDs

  

The CUDD package provides a rich set of dynamic  reordering algorithms. Some of them are slight variations of existing techniques [16, 6, 2, 10, 15, 11]; some others have been developed specifically for this package [14, 13].

Reordering affects a unique  table. This means that BDDs and ADDs, which share the same unique table are simultaneously reordered. ZDDs, on the other hand, are reordered separately. In the following we discuss the reordering of BDDs and ADDs. Reordering for ZDDs is the subject of Section 3.14.

Reordering of the variables can be invoked directly by the application by calling Cudd_ReduceHeap . Or it can be automatically triggered by the package when the number of nodes has reached a given threshold . (The threshold is initialized and automatically adjusted after each reordering by the package.) To enable automatic dynamic reordering (also called asynchronous  dynamic reordering in this document) the application must call Cudd_AutodynEnable . Automatic dynamic reordering can subsequently be disabled by calling Cudd_AutodynDisable .

All reordering methods are available in both the case of direct call to Cudd_ReduceHeap  and the case of automatic invocation. For many methods, the reordering procedure is iterated until no further improvement is obtained. We call these methods the converging  methods. When constraints are imposed on the relative position of variables (see Section 3.13) the reordering methods apply inside the groups. The groups  themselves are reordered by sifting . Each method is identified by a constant of the enumerated type Cudd_ReorderingType  defined in cudd.h  (the external header  file of the CUDD package):

CUDD_REORDER_NONE :
This method causes no reordering.
CUDD_REORDER_SAME :
If passed to Cudd_AutodynEnable , this method leaves the current method for automatic reordering unchanged. If passed to Cudd_ReduceHeap , this method causes the current method for automatic reordering to be used.
CUDD_REORDER_RANDOM :
Pairs of variables are randomly chosen, and swapped in the order. The swap is performed by a series of swaps of adjacent variables. The best order among those obtained by the series of swaps is retained. The number of pairs chosen for swapping  equals the number of variables in the diagram.
CUDD_REORDER_RANDOM_PIVOT :
Same as CUDD_REORDER_RANDOM, but the two variables are chosen so that the first is above the variable with the largest number of nodes, and the second is below that variable. In case there are several variables tied for the maximum number of nodes, the one closest to the root is used.
CUDD_REORDER_SIFT :
This method is an implementation of Rudell's sifting  algorithm [16]. A simplified description of sifting is as follows: Each variable is considered in turn. A variable is moved up and down in the order so that it takes all possible positions. The best position is identified and the variable is returned to that position.

In reality, things are a bit more complicated. For instance, there is a limit on the number of variables that will be sifted. This limit can be read with Cudd_ReadSiftMaxVar  and set with Cudd_SetSiftMaxVar . In addition, if the diagram grows too much while moving a variable up or down, that movement is terminated before the variable has reached one end of the order. The maximum ratio by which the diagram is allowed to grow while a variable is being sifted can be read with Cudd_ReadMaxGrowth  and set with Cudd_SetMaxGrowth .

CUDD_REORDER_SIFT_CONVERGE :
This is the converging  variant of CUDD_REORDER_SIFT.
CUDD_REORDER_SYMM_SIFT :
This method is an implementation of symmetric  sifting [14]. It is similar to sifting, with one addition: Variables that become adjacent during sifting are tested for symmetry . If they are symmetric, they are linked in a group. Sifting then continues with a group being moved, instead of a single variable. After symmetric sifting has been run, Cudd_SymmProfile  can be called to report on the symmetry groups found. (Both positive and negative symmetries are reported.)
CUDD_REORDER_SYMM_SIFT_CONV :
This is the converging  variant of CUDD_REORDER_SYMM_SIFT.
CUDD_REORDER_GROUP_SIFT :
This method is an implementation of group  sifting [13]. It is similar to symmetric sifting, but aggregation  is not restricted to symmetric variables.
CUDD_REORDER_GROUP_SIFT_CONV :
This method repeats until convergence the combination of CUDD_REORDER_GROUP_SIFT and CUDD_REORDER_WINDOW4.
CUDD_REORDER_WINDOW2 :
This method implements the window  permutation approach of Fujita [8] and Ishiura [10]. The size of the window is 2.
CUDD_REORDER_WINDOW3 :
Similar to CUDD_REORDER_WINDOW2, but with a window of size 3.
CUDD_REORDER_WINDOW4 :
Similar to CUDD_REORDER_WINDOW2, but with a window of size 4.
CUDD_REORDER_WINDOW2_CONV :
This is the converging  variant of CUDD_REORDER_WINDOW2.
CUDD_REORDER_WINDOW3_CONV :
This is the converging variant of CUDD_REORDER_WINDOW3.
CUDD_REORDER_WINDOW4_CONV :
This is the converging variant of CUDD_REORDER_WINDOW4.
CUDD_REORDER_ANNEALING :
This method is an implementation of simulated annealing  for variable ordering, vaguely resemblant of the algorithm of [2]. This method is potentially very slow.
CUDD_REORDER_GENETIC: 
This method is an implementation of a genetic  algorithm for variable ordering, inspired by the work of Drechsler [6]. This method is potentially very slow.
CUDD_REORDER_EXACT :
This method implements a dynamic programming approach to exact  reordering [9, 7, 10], with improvements described in [11]. It only stores one BDD at the time. Therefore, it is relatively efficient in terms of memory. Compared to other reordering strategies, it is very slow, and is not recommended for more than 16 variables.

So far we have described methods whereby the package selects an order automatically. A given order of the variables can also be imposed by calling Cudd_ShuffleHeap .


next up previous index
Next: Grouping Variables Up: User's Manual Previous: Converting BDDs to ZDDs

Fabio Somenzi
Tue May 12 18:47:58 MDT 1998