Next: Grouping Variables
Up: User's Manual
Previous: Converting BDDs to ZDDs
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: Grouping Variables
Up: User's Manual
Previous: Converting BDDs to ZDDs
Fabio Somenzi
Thu Sep 24 23:44:34 MDT 1998