dynamic_var_ordering - Deals with the dynamic variable ordering.
dynamic_var_ordering [-d] [-e <method>] [-f <method>] [-h]
Controls the application and the modalities of (dynamic) variable
ordering. Dynamic ordering is a technique to reorder the BDD variables
to reduce the size of the existing BDDs. When no options are specified,
the current status of dynamic ordering is displayed. At most one of the
options -e, -f, and -d should be specified.
Dynamic ordering may be time consuming, but can often reduce the size of
the BDDs dramatically. A good point to invoke dynamic ordering
explicitly (using the -f option) is after the commands
build_model, once the transition relation has been built. It is
possible to save the ordering found using write_order in order to
reuse it (using build_model -i order-file) in the future.
Command options:
- -d
- Disable dynamic ordering from triggering automatically.
- -e <method>
- Enable dynamic ordering to trigger automatically whenever a
certain threshold on the overall BDD size is reached.
<method> must be one of the following:
- sift: Moves each variable throughout the order to
find an optimal position for that variable (assuming all
other variables are fixed). This generally achieves
greater size reductions than the window method, but is slower.
- 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.
- random_pivot: Same as 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.
- sift_converge: The sift method is iterated
until no further improvement is obtained.
- symmetry_sift: This method is an implementation of
symmetric sifting. 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.
- symmetry_sift_converge: The symmetry_sift
method is iterated until no further improvement is obtained.
- window{2,3,4}: Permutes the variables within windows
of "n" adjacent variables, where "n" can be either 2, 3 or 4,
so as to minimize the overall BDD size.
- window{2,3,4}_converge: The window{2,3,4} method
is iterated until no further improvement is obtained.
- group_sift: This method is similar to
symmetry_sift, but uses more general criteria to
create groups.
- group_sift_converge: The group_sift method is
iterated until no further improvement is obtained.
- annealing: This method is an implementation of
simulated annealing for variable ordering. This method is
potentially very slow.
- genetic: This method is an implementation of a
genetic algorithm for variable ordering. This method is
potentially very slow.
- exact: This method implements a dynamic programming
approach to exact reordering. It only stores a BDD
at a 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 boolean variables.
- linear: This method is a combination of
sifting and linear transformations.
- linear_converge: The linear method is
iterated until no further improvement is obtained.
- -f <method>
- Force dynamic ordering to be invoked immediately. The values for
<method> are the same as in option -e.
Last updated on 2010/05/19 15h:56