source: vis_dev/vis-2.3/share/help/dynamic_var_orderingCmd.txt @ 41

Last change on this file since 41 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 5.4 KB
Line 
1
2  dynamic_var_ordering - control the application of dynamic variable ordering
3     _________________________________________________________________
4
5   dynamic_var_ordering [-d] [-e <method>] [-f <method>] [-h]
6
7   Control  the application of dynamic variable ordering to the flattened
8   network. Dynamic ordering is a technique to reorder the MDD variables to
9   reduce the size of the existing MDDs. When no options are specified, the
10   current status of dynamic ordering is displayed. At most one of the options
11   -e, -f, and -d should be specified. The commands flatten_hierarchy and
12   static_order must be invoked before this command.
13
14   Dynamic ordering may be time consuming, but can often reduce the size of the
15   MDDs dramatically. The good points to invoke dynamic ordering explicitly
16   (using  the -f option) are after the commands build_partition_mdds and
17   print_img_info. If dynamic ordering finds a good ordering, then you may wish
18   to save this ordering (using write_order) and reuse it (using static_order
19   -s) in the future. A common sequence used to get a good ordering is the
20   following:
21
22  init_verify
23  print_img_info
24  dynamic_var_ordering -f sift
25  write_order
26  flatten_hierarchy
27  static_order -s input_and_latch -f
28  build_partition_mdds
29  print_img_info
30  dynamic_var_ordering -f sift
31 
32
33   For many large examples, there is no single best variable order, or that
34   order is hard to find. For example, the best ordering during partitioning of
35   the network may be different from the best ordering during a model check. In
36   that case you can use automatic reordering, using the -e option. This will
37   trigger reordering whenever the total size of the MDD increases by a certain
38   factor. Often, the init command is replaced by the following sequence:
39  flatten_hierarchy
40  static_order
41  dynamic_var_ordering -e sift
42  build_partition_mdds
43 
44
45   Command options:
46
47   -d
48          Disable dynamic ordering from triggering automatically.
49
50   -e <method>
51          Enable dynamic ordering to trigger automatically whenever a certain
52          threshold on the overall MDD size is reached. "Method" must be one of
53          the following:
54
55          window: Permutes the variables within windows of three adjacent
56          variables so as to minimize the overall MDD size. This process is
57          repeated until no more reduction in size occurs.
58
59          sift: Moves each variable throughout the order to find an optimal
60          position for that variable (assuming all other variables are fixed).
61          This generally achieves greater size reductions than the window
62          method, but is slower.
63
64          The following methods are only available if VIS has been linked with
65          the Bdd package from the University of Colorado (cuBdd).
66
67          random: Pairs of variables are randomly chosen, and swapped in the
68          order.  The  swap is performed by a series of swaps of adjacent
69          variables. The best order among those obtained by the series of swaps
70          is retained. The number of pairs chosen for swapping equals the
71          number of variables in the diagram.
72
73          random_pivot: Same as random, but the two variables are chosen so
74          that the first is above the variable with the largest number of
75          nodes, and the second is below that variable. In case there are
76          several variables tied for the maximum number of nodes, the one
77          closest to the root is used.
78
79          sift_converge:  The  sift  method  is iterated until no further
80          improvement is obtained.
81
82          symmetry_sift: This method is an implementation of symmetric sifting.
83          It is similar to sifting, with one addition: Variables that become
84          adjacent  during  sifting  are tested for symmetry. If they are
85          symmetric, they are linked in a group. Sifting then continues with a
86          group being moved, instead of a single variable.
87
88          symmetry_sift_converge: The symmetry_sift method is iterated until no
89          further improvement is obtained.
90
91          window{2,3,4}: Permutes the variables within windows of n adjacent
92          variables, where "n" can be either 2, 3 or 4, so as to minimize the
93          overall MDD size.
94
95          window{2,3,4}_converge: The window{2,3,4} method is iterated until no
96          further improvement is obtained.
97
98          group_sift: This method is similar to symmetry_sift, but uses more
99          general criteria to create groups.
100
101          group_sift_converge: The group_sift method is iterated until no
102          further improvement is obtained.
103
104          lazy_sift: This method is similar to group_sift, but the creation of
105          groups takes into account the pairing of present and next state
106          variables.
107
108          annealing: This method is an implementation of simulated annealing
109          for variable ordering. This method is potentially very slow.
110
111          genetic: This method is an implementation of a genetic algorithm for
112          variable ordering. This method is potentially very slow.
113
114   -f <method>
115          Force dynamic ordering to be invoked immediately. The values for
116          method are the same as in option -e.
117
118   -h
119          Print the command usage.
120
121   -v <#>
122          Verbosity level. Default is 0. For values greater than 0, statistics
123          pertaining to reordering will be printed whenever reordering occurs.
124     _________________________________________________________________
125
126   Last updated on 20100410 00h02
Note: See TracBrowser for help on using the repository browser.