next up previous
Next: Conclusions Up: Evaluating Symbolic Traversal Algorithms Previous: Fixed variable order results

Automatic variable reordering results

To make result tables as small as possible we will use the following codes to identify the traversal methods:


Name Reorderings Reordering Time Peak BDD Time
B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD
c-arbiter ?? ?? ?? 5 2 12 13 14 13 - - - ?? ?? ?? 0.3 0.0 951.4 635.3 647.9 586.1 - - - ?? ?? ?? 94056 18431 2054648 1098458 849997 958665 - - - ?? ?? ?? 13.7 9.3 2747.3 926.6 992.6 1047.7 - - -
c-arbiter-xl ?? ?? ?? 8 - - - - - - - - ?? ?? ?? 1.2 - - - - - - - - ?? ?? ?? 1072355 - - - - - - - - ?? ?? ?? 268.8 - - - - - - - -
gals 0 0 0 0 0 3 3 2 2 3 2 2 0.0 0.0 0.0 0.0 0.0 0.5 0.4 0.2 0.2 0.3 0.2 0.2 3673 3697 3668 3668 3813 11786 6414 5487 5097 6896 5622 5458 0.1 0.1 0.1 0.1 0.1 0.8 0.5 0.7 0.4 0.6 0.7 0.4
pcc 4 1 0 1 1 5 8 8 8 8 9 8 0.2 0.0 0.0 0.0 0.0 1.9 9.7 11.1 9.1 37.2 26.0 10.6 50793 7471 4903 5396 5353 38692 80411 66876 68372 159126 110506 85286 11.4 0.4 0.5 0.4 0.7 7.7 16.7 27.2 18.5 52.2 47.3 21.5
muller_
n Reorderings Reordering Time Peak BDD Time
B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD
5 0 0 0 0 0 1 0 0 0 0 0 0 0.0 0.0 0.0 0.0 0.0 0.1 0.0 0.0 0.0 0.0 0.0 0.0 1170 1222 1220 1220 1220 4004 3777 3777 2176 3777 3777 2176 0.0 0.0 0.0 0.0 0.0 0.1 0.0 0.0 0.0 0.0 0.0 0.0
10 0 0 0 0 0 2 3 3 2 3 3 3 0.0 0.0 0.0 0.0 0.0 0.3 0.4 0.4 0.2 0.4 0.4 0.5 4165 4266 3929 3916 3938 8936 7229 7179 6703 9121 7360 8006 0.1 0.0 0.1 0.0 0.0 0.4 0.5 0.9 0.3 0.6 0.9 0.6
15 2 1 1 1 1 4 7 6 6 7 7 7 0.1 0.0 0.0 0.0 0.0 2.1 6.7 3.6 3.8 7.1 8.1 9.0 11465 8221 7919 8230 8240 36224 45096 50078 45647 62005 70629 61296 1.0 0.2 0.2 0.2 0.3 3.1 9.1 15.8 6.4 11.6 20.8 12.8
20 ?? 1 1 1 1 9 10 9 10 10 10 9 ?? 0.1 0.0 0.1 0.1 192.5 119.1 40.8 285.8 143.3 107.7 107.0 ?? 15472 14445 14657 14890 382037 334430 137102 456832 425321 207118 234539 ?? 0.9 1.0 0.7 1.6 250.4 191.9 93.7 344.0 232.9 204.4 153.7
25 3 1 1 1 1 12 13 21 - - - - 0.4 0.1 0.1 0.1 0.1 1406.0 2498.7 1261.0 - - - - 94211 24880 21131 23512 23222 1477401 1999709 844977 - - - - 107.5 2.1 2.0 1.6 4.5 1931.3 ?? 1950.8 - - - -
30 ?? 2 1 1 1 - - - - - - - ?? 0.4 0.1 0.1 0.1 - - - - - - - ?? 35041 28618 34739 34793 - - - - - - - ?? 4.8 4.5 3.3 13.2 - - - - - - -
40 ?? 2 1 2 2 - - - - - - - ?? 0.7 0.3 0.7 0.7 - - - - - - - ?? 72333 50844 69847 66016 - - - - - - - ?? 19.8 16.2 12.3 66.4 - - - - - - -
50 - 2 1 2 2 - - - - - - - - 1.4 0.6 1.3 1.3 - - - - - - - - 124040 79033 119143 113264 - - - - - - - - 58.8 41.4 31.4 233.5 - - - - - - -
60 - 2 1 2 2 - - - - - - - - 2.3 1.1 2.3 2.2 - - - - - - - - 189749 107884 191655 177155 - - - - - - - - 133.1 80.4 70.3 695.3 - - - - - - -
70 - ?? 1 2 2 - - - - - - - - ?? 1.7 3.5 3.5 - - - - - - - - ?? 146516 291131 269729 - - - - - - - - ?? 158.7 148.7 1659.9 - - - - - - -
80 - ?? 1 3 - - - - - - - - - ?? 2.6 8.0 - - - - - - - - - ?? 196450 436100 - - - - - - - - - ?? 302.6 313.9 - - - - - - - -
90 - 3 1 3 - - - - - - - - - 11.4 3.6 11.3 - - - - - - - - - 606186 243723 620684 - - - - - - - - - 1237.6 483.2 537.5 - - - - - - - -
100 - ?? 1 3 - - - - - - - - - ?? 5.0 15.4 - - - - - - - - - ?? 300593 828491 - - - - - - - - - ?? 785.0 927.5 - - - - - - - -
pipeline
n Reorderings Reordering Time Peak BDD Time
B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD
1 0 0 0 0 0 1 0 1 1 0 1 1 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 1479 942 831 857 773 4004 3575 4753 4004 3824 4809 4004 0.1 0.0 0.0 0.0 0.0 0.1 0.0 0.2 0.0 0.1 0.2 0.1
2 2 0 0 0 0 5 6 6 5 6 6 5 0.1 0.0 0.0 0.0 0.0 0.7 0.6 0.7 0.4 0.6 0.6 0.4 10787 1717 1600 1671 1655 18841 23286 18056 16840 24047 19685 17870 1.9 0.1 0.1 0.1 0.1 2.4 1.6 2.7 1.6 1.8 2.3 1.6
4 ?? 0 0 0 0 11 4 4 5 5 4 5 ?? 0.0 0.0 0.0 0.0 273.8 0.3 0.4 0.4 0.8 0.4 0.4 ?? 4813 4560 4542 4124 1119730 24406 16085 17238 22477 16200 18199 ?? 0.4 0.5 0.6 1.2 1306.6 1.1 2.5 1.5 1.7 2.5 1.5
pipelineabs
n Reorderings Reordering Time Peak BDD Time
B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD
1 0 0 0 0 0 1 1 1 0 1 1 0 0.0 0.0 0.0 0.0 0.0 0.1 0.1 0.1 0.0 0.1 0.1 0.0 1878 1721 1617 1629 1679 4710 4005 4007 2820 4004 4004 3203 0.0 0.0 0.0 0.0 0.0 0.1 0.1 0.2 0.0 0.1 0.2 0.0
2 1 0 0 0 0 3 4 4 3 4 4 3 0.0 0.0 0.0 0.0 0.0 0.4 0.6 0.5 0.3 0.6 0.5 0.3 6962 4360 4295 4028 4225 10571 13159 13270 8396 14185 13465 9303 0.6 0.1 0.1 0.1 0.1 0.6 0.9 1.9 0.6 0.9 1.9 0.6
4 ?? 2 2 2 1 9 9 8 8 12 11 11 ?? 0.1 0.1 0.1 0.0 68.0 59.7 16.7 23.3 680.3 196.4 337.2 ?? 13981 10811 11925 10364 204915 169846 88456 107342 801725 534346 565364 ?? 1.0 0.5 1.0 1.9 110.6 83.8 66.3 44.9 1201.0 1000.9 793.9
8 ?? 2 1 2 1 - - - - - - - ?? 0.4 0.1 0.3 0.1 - - - - - - - ?? 41278 27745 41547 30395 - - - - - - - ?? 11.3 2.5 11.9 39.5 - - - - - - -
16 ?? 2 1 2 1 - - - - - - - ?? 1.7 0.8 1.7 0.8 - - - - - - - ?? 126406 80400 158123 100017 - - - - - - - ?? 148.4 14.6 172.2 1096.2 - - - - - - -
stari
n Reorderings Reordering Time Peak BDD Time
B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD
4 3 ?? 0 1 0 8 9 8 9 9 8 11 0.1 ?? 0.0 0.0 0.0 14.3 17.5 6.5 9.5 16.1 6.4 84.0 39477 ?? 4299 6339 3110 134403 105371 63546 68272 104544 64032 360845 28.6 ?? 0.4 1.4 0.8 36.1 46.3 43.9 28.8 43.1 45.3 220.5
8 ?? 3 2 3 1 - - - - - - - ?? 0.2 0.1 0.1 0.0 - - - - - - - ?? 37507 14335 30000 10350 - - - - - - - ?? 11.1 5.8 29.9 25.3 - - - - - - -
12 ?? ?? ?? 3 2 - - - - - - - ?? ?? ?? 0.2 0.1 - - - - - - - ?? ?? ?? 77272 24553 - - - - - - - ?? ?? ?? 187.4 210.9 - - - - - - -
16 ?? ?? 2 4 3 - - - - - - - ?? ?? 0.3 0.8 0.4 - - - - - - - ?? ?? 48590 200435 74089 - - - - - - - ?? ?? 1943.6 985.9 1997.6 - - - - - - -
tree
n Reorderings Reordering Time Peak BDD Time
B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD B C T W D N I H M IHD HHD MHD
5 0 0 0 0 0 2 4 4 2 4 4 3 0.0 0.0 0.0 0.0 0.0 0.2 0.3 0.3 0.1 0.3 0.3 0.2 3638 3333 3004 2674 2836 8624 7258 8554 6076 7668 8332 6314 0.1 0.1 0.1 0.0 0.0 0.4 0.4 0.7 0.2 0.5 0.8 0.3
10 2 2 1 1 1 9 9 9 9 9 9 9 2.3 2.2 1.0 1.0 1.0 31.0 6.2 7.2 8.0 6.3 6.7 6.4 16355 12489 10602 7366 7549 166309 70117 59166 68360 70611 59142 48840 4.8 2.7 1.4 1.1 1.3 42.1 9.8 17.8 11.9 9.8 18.9 9.2
15 2 2 2 1 1 11 10 9 13 - - - 7.1 6.7 6.7 3.1 3.2 175.5 96.4 29.1 1592.0 - - - 43206 30500 37834 14580 14580 504552 377682 377682 2298202 - - - 28.8 10.2 9.3 3.4 4.0 614.7 150.2 120.2 2242.6 - - -
20 ?? 2 ?? 1 1 - - 10 - - - - ?? 0.4 ?? 0.2 0.2 - - 448.4 - - - - ?? 67754 ?? 24194 24194 - - 12061303 - - - - ?? 16.6 ?? 0.7 1.9 - - 3099.5 - - - -
30 3 3 5 1 1 - - - - - - - 104.4 96.5 391.8 23.9 24.1 - - - - - - - 203925 192972 469708 50622 50622 - - - - - - - 1142.0 223.9 490.0 25.4 30.4 - - - - - - -
40 - 3 5 1 1 - - - - - - - - 245.2 877.5 57.2 57.4 - - - - - - - - 431980 717128 86650 86650 - - - - - - - - 749.8 1438.5 60.1 73.1 - - - - - - -
50 - 4 - 1 1 - - - - - - - - 1039.9 - 114.2 114.2 - - - - - - - - 702444 - 132278 132278 - - - - - - - - 2499.7 - 119.8 153.0 - - - - - - -
60 - - - 1 1 - - - - - - - - - - 200.7 202.6 - - - - - - - - - - 187506 187506 - - - - - - - - - - 209.9 275.0 - - - - - - -
70 - - - 1 1 - - - - - - - - - - 5.2 5.2 - - - - - - - - - - 252335 252335 - - - - - - - - - - 18.7 136.9 - - - - - - -

next up previous
Next: Conclusions Up: Evaluating Symbolic Traversal Algorithms Previous: Fixed variable order results
Enric Pastor 2004-05-28