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