CAMUS Results - Benz Benchmarks Using PCSes

These are the instances from the full set of automotive product configuration benchmarks that timed out in the first phase of CAMUS (finding MCSes). Here, we use these instances to illustrate relaxing the completeness criterion of CAMUS in order to deal with such intractable instances.

The idea behind this approach is to truncate MCSes found in the complete CAMUS algorithm to form PCSes instead. By controlling how much truncation is done, we can alter the number of PCSes found, and thus the number of MUSes and total runtime as well. Each of the three tables below contains results for running the algorithm with a limit set on the size of each PCS, from 1 to 3. (The Max PCS size is often above this limit due to the specifics of the algorithm; the limit is a fairly strict guide, but it is broken at times.) When the algorithm is run with a PCS size limit of 1, it always produces a single, exact MUS.

Runs that reached the 600 second timeout are indicated by "--". In these cases, either the number of PCSes or MUSes generated is preceded by a ">" indicating that this is the number found before the timeout was reached. If the MUS computation timed out, the Min and Max MUS sizes are the smallest and largest of those found before timing out - they are upper and lower bounds, respectively.

These data were generated on an older machine (2.2GHz Opteron) with an older, unreleased version of CAMUS.

Size Limit = 1

Runtimes (sec)PCS sizesMUS sizes
NameVarsClausesPCSesMUSesTotal#PCSesMinMaxMUSesMinMax
C168_FW_SZ_107 1583 5939 2.98 0.001 2.981 92 1 1 1 92 92
C168_FW_SZ_128 1583 4777 2.46 0.001 2.461 118 1 1 1 118 118
C168_FW_SZ_41 1583 4727 0.721 0 0.721 40 1 1 1 40 40
C168_FW_SZ_66 1583 4751 0.316 0 0.316 19 1 1 1 19 19
C168_FW_SZ_75 1583 4744 0.463 0 0.463 57 1 1 1 57 57
C168_FW_UT_2463 1804 6756 1.31 0.001 1.311 62 1 1 1 62 62
C168_FW_UT_2468 1804 6754 1.67 0.001 1.671 57 1 1 1 57 57
C168_FW_UT_2469 1804 6767 1.06 0.001 1.061 38 1 1 1 38 38
C168_FW_UT_714 1804 6754 0.077 0 0.077 9 1 1 1 9 9
C202_FS_SZ_74 1556 5561 0.504 0.001 0.505 182 1 1 1 182 182
C202_FS_SZ_84 1556 5479 9.22 0.001 9.221 234 1 1 1 234 234
C202_FW_SZ_100 1561 7484 0.825 0.001 0.826 27 1 1 1 27 27
C202_FW_SZ_103 1561 9024 25.2 0.001 25.201 292 1 1 1 292 292
C202_FW_SZ_61 1561 7490 1.72 0 1.72 44 1 1 1 44 44
C202_FW_SZ_77 1561 7611 0.882 0.001 0.883 184 1 1 1 184 184
C202_FW_SZ_87 1561 7696 31.1 0.002 31.102 398 1 1 1 398 398
C202_FW_SZ_96 1561 7599 13.1 0.001 13.101 236 1 1 1 236 236
C202_FW_SZ_98 1561 7438 0.814 0.001 0.815 29 1 1 1 29 29
C202_FW_UT_2814 1820 9957 7.06 0.001 7.061 47 1 1 1 47 47
C202_FW_UT_2815 1820 9957 6.98 0.001 6.981 47 1 1 1 47 47
C208_FC_RZ_65 1513 4491 0.167 0 0.167 12 1 1 1 12 12
C208_FC_SZ_107 1513 4554 0.68 0.001 0.681 70 1 1 1 70 70
C210_FS_RZ_23 1608 4911 0.523 0 0.523 39 1 1 1 39 39
C210_FS_SZ_103 1607 4915 0.886 0.001 0.887 57 1 1 1 57 57
C210_FS_SZ_55 1608 4917 0.729 0.001 0.73 59 1 1 1 59 59
C210_FS_SZ_78 1607 5071 0.588 0 0.588 187 1 1 1 187 187
C210_FW_RZ_30 1629 6407 0.804 0 0.804 45 1 1 1 45 45
C210_FW_SZ_106 1628 6405 1.99 0.001 1.991 74 1 1 1 74 74
C210_FW_SZ_128 1628 6401 0.385 0 0.385 30 1 1 1 30 30
C210_FW_SZ_80 1628 6560 0.56 0 0.56 174 1 1 1 174 174
C210_FW_SZ_90 1628 6977 17.2 0.001 17.201 299 1 1 1 299 299
C210_FW_SZ_91 1628 6709 16.3 0.001 16.301 302 1 1 1 302 302
C210_FW_UT_8630 1891 8511 1.3 0.001 1.301 35 1 1 1 35 35
C210_FW_UT_8634 1891 8504 2.97 0 2.97 42 1 1 1 42 42
C220_FV_SZ_39 1530 4788 11.8 0.001 11.801 309 1 1 1 309 309

Size Limit = 2

Runtimes (sec)PCS sizesMUS sizes
NameVarsClausesPCSesMUSesTotal#PCSesMinMaxMUSesMinMax
C168_FW_SZ_107 1583 5939 29.6 0.057 29.657 434 1 3 2136 47 122
C168_FW_SZ_128 1583 4777 3.02 191 194.02 245 1 3 6268144 99 129
C168_FW_SZ_41 1583 4727 2.9 0.004 2.904 122 1 3 118 27 47
C168_FW_SZ_66 1583 4751 4.16 0.007 4.167 189 1 3 248 16 49
C168_FW_SZ_75 1583 4744 2.39 0.014 2.404 141 1 3 824 49 67
C168_FW_UT_2463 1804 6756 6.14 0.044 6.184 198 1 2 1152 40 65
C168_FW_UT_2468 1804 6754 5.66 0.434 6.094 157 1 3 13184 42 61
C168_FW_UT_2469 1804 6767 5.43 0.056 5.486 159 1 2 1792 38 51
C168_FW_UT_714 1804 6754 0.397 0.001 0.398 19 1 2 2 9 19
C202_FS_SZ_74 1556 5561 0.408 0.001 0.409 182 1 2 16 150 182
C202_FS_SZ_84 1556 5479 32.6 -- 685 1 3 >1308604 233 237
C202_FW_SZ_100 1561 7484 3.78 0.007 3.787 117 1 3 267 27 67
C202_FW_SZ_103 1561 9024 115 -- 919 1 5 >127632 262 264
C202_FW_SZ_61 1561 7490 12.3 0.01 12.31 214 1 4 314 21 52
C202_FW_SZ_77 1561 7611 0.826 0.002 0.828 185 1 2 64 156 185
C202_FW_SZ_87 1561 7696 101 -- 1207 1 4 >85584 564 571
C202_FW_SZ_96 1561 7599 35.2 -- 611 1 2 >43800 321 322
C202_FW_SZ_98 1561 7438 1.66 0.002 1.662 75 1 3 123 7 29
C202_FW_UT_2814 1820 9957 43.1 0.073 43.173 473 1 4 1198 27 77
C202_FW_UT_2815 1820 9957 43 0.074 43.074 473 1 4 1198 27 77
C208_FC_RZ_65 1513 4491 0.335 0.001 0.336 37 1 2 48 12 21
C208_FC_SZ_107 1513 4554 1.74 0.014 1.754 136 1 3 400 47 74
C210_FS_RZ_23 1608 4911 3.19 0.251 3.441 133 1 3 15406 32 51
C210_FS_SZ_103 1607 4915 1.9 -- 145 1 3 >14213475 50 74
C210_FS_SZ_55 1608 4917 2.43 0.766 3.196 143 1 3 42608 41 67
C210_FS_SZ_78 1607 5071 1.17 0.004 1.174 225 1 3 48 173 185
C210_FW_RZ_30 1629 6407 8.03 1.16 9.19 173 1 3 58842 37 59
C210_FW_SZ_106 1628 6405 11.2 -- 241 1 4 >4249594 64 86
C210_FW_SZ_128 1628 6401 1.03 0.582 1.612 84 1 2 28672 23 36
C210_FW_SZ_80 1628 6560 2.53 0.003 2.533 255 1 2 16 175 185
C210_FW_SZ_90 1628 6977 35.1 -- 880 1 3 >37962 460 465
C210_FW_SZ_91 1628 6709 34.5 -- 594 1 2 >2315168 320 328
C210_FW_UT_8630 1891 8511 15.8 0.299 16.099 161 1 3 16016 36 79
C210_FW_UT_8634 1891 8504 6.08 0.386 6.466 93 1 2 20480 27 53
C220_FV_SZ_39 1530 4788 12.6 -- 784 1 3 >13548 633 633

Size Limit = 3

Runtimes (sec)PCS sizesMUS sizes
NameVarsClausesPCSesMUSesTotal#PCSesMinMaxMUSesMinMax
C168_FW_SZ_107 1583 5939 124 -- 1040 1 7 >14598284 104 128
C168_FW_SZ_128 1583 4777 7.32 -- 335 1 4 >22838876 107 136
C168_FW_SZ_41 1583 4727 10.1 0.41 10.51 263 1 6 4500 26 62
C168_FW_SZ_66 1583 4751 13.1 18.4 31.5 499 1 7 434035 16 59
C168_FW_SZ_75 1583 4744 6.69 7.17 13.86 231 1 7 418463 48 74
C168_FW_UT_2463 1804 6756 38.1 -- 1607 1 5 >836022 40 79
C168_FW_UT_2468 1804 6754 9.28 46.9 56.18 473 1 4 409509 36 73
C168_FW_UT_2469 1804 6767 30.9 483 513.9 1336 1 6 403392 35 66
C168_FW_UT_714 1804 6754 0.38 0 0.38 19 1 3 3 9 19
C202_FS_SZ_74 1556 5561 0.388 0.002 0.39 183 1 3 60 150 183
C202_FS_SZ_84 1556 5479 138 -- 2147 1 7 >4067088 243 261
C202_FW_SZ_100 1561 7484 13.9 31.3 45.2 320 1 6 1105768 27 79
C202_FW_SZ_103 1561 9024 273 -- 1234 1 10 >4181804 257 276
C202_FW_SZ_61 1561 7490 31.7 1.83 33.53 755 1 6 43238 19 69
C202_FW_SZ_77 1561 7611 0.727 0.003 0.73 187 1 3 144 156 187
C202_FW_SZ_87 1561 7696 -- >0
C202_FW_SZ_96 1561 7599 339 -- 1810 1 5 >5610029 238 354
C202_FW_SZ_98 1561 7438 9.38 0.836 10.216 314 1 5 37718 7 43
C202_FW_UT_2814 1820 9957 267 125 392 2275 1 7 4869852 20 75
C202_FW_UT_2815 1820 9957 262 125 387 2275 1 7 4869852 20 75
C208_FC_RZ_65 1513 4491 1.12 0.041 1.161 77 1 3 2494 12 25
C208_FC_SZ_107 1513 4554 4.5 1.27 5.77 279 1 5 32718 44 82
C210_FS_RZ_23 1608 4911 3.59 10.9 14.49 195 1 5 474404 31 52
C210_FS_SZ_103 1607 4915 6.42 -- 260 1 5 >15615479 54 78
C210_FS_SZ_55 1608 4917 4.93 388 392.93 246 1 8 14589828 41 77
C210_FS_SZ_78 1607 5071 1.35 0.032 1.382 267 1 5 432 170 194
C210_FW_RZ_30 1629 6407 10.8 -- 266 1 6 >16859897 38 66
C210_FW_SZ_106 1628 6405 29.8 -- 403 1 7 >18406484 59 91
C210_FW_SZ_128 1628 6401 2.66 19.9 22.56 197 1 5 493568 23 41
C210_FW_SZ_80 1628 6560 2.74 0.034 2.774 265 1 5 440 171 185
C210_FW_SZ_90 1628 6977 101 -- 983 1 5 >1679408 414 423
C210_FW_SZ_91 1628 6709 112 -- 1057 1 6 >2476166 470 486
C210_FW_UT_8630 1891 8511 65.7 259 324.7 985 1 7 4192496 34 69
C210_FW_UT_8634 1891 8504 68.9 167 235.9 760 1 6 5207976 26 84
C220_FV_SZ_39 1530 4788 30 -- 1433 1 7 >2738674 281 305