Mark Liffiton

lastname -at- eecs -dot- -domain-

CAMUS Results - Benz Benchmarks

These benchmarks come from an automotive product configuration domain. More information is available at the benchmarks' website:
http://www-sr.informatik.uni-tuebingen.de/~sinz/DC/

The original benchmarks contain duplicate clauses, which create a potentially exponential number of spurious, duplicate MUSes. We removed all duplicate clauses before using these benchmarks. Further, the original files contain unused variables, and these were filtered out as well, resulting in lower variable counts than the original formulas although they are functionally unchanged.

Runs that reached the 600 second timeout are indicated by "--". In these cases, either the number of MCSes 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.

Runtimes (sec)MCS sizesMUS sizes
NameVarsClausesMCSesMUSesTotal#MCSesMinMax#MUSesMinMax
C168_FW_SZ_107 1583 5939 -- >17152 1 11
C168_FW_SZ_128 1583 4777 -- >9382 1 16
C168_FW_SZ_41 1583 4727 -- >9030 1 12
C168_FW_SZ_66 1583 4751 -- >11475 1 13
C168_FW_SZ_75 1583 4744 -- >18688 1 19
C168_FW_UT_2463 1804 6756 -- >20334 1 13
C168_FW_UT_2468 1804 6754 -- >16364 1 13
C168_FW_UT_2469 1804 6767 -- >25354 1 13
C168_FW_UT_714 1804 6754 -- >20677 1 17
C168_FW_UT_851 1804 6758 0.141 0.001 0.142 30 1 8 102 8 16
C168_FW_UT_852 1804 6756 0.135 0.001 0.136 30 1 8 102 8 16
C168_FW_UT_854 1804 6753 0.138 0.001 0.139 30 1 8 102 8 16
C168_FW_UT_855 1804 6752 0.136 0.001 0.137 30 1 8 102 8 16
C170_FR_RZ_32 1528 4067 0.129 0.264 0.393 242 1 2 32768 227 228
C170_FR_SZ_58 1528 4083 0.198 5.38 5.578 177 1 8 218692 46 63
C170_FR_SZ_92 1528 4195 0.062 0 0.062 131 1 1 1 131 131
C170_FR_SZ_95 1528 4068 0.116 -- 175 1 3 >11257888 10 66
C170_FR_SZ_96 1528 4068 2.26 -- 2605 1 22 >467220 67 80
C202_FS_RZ_44 1556 5399 3.07 -- 2658 1 48 >7643816 28 54
C202_FS_SZ_104 1556 5405 4.79 -- 3593 1 61 >4525742 70 94
C202_FS_SZ_121 1556 5387 0.037 0.001 0.038 24 1 2 4 22 24
C202_FS_SZ_122 1556 5385 0.037 0 0.037 33 1 1 1 33 33
C202_FS_SZ_74 1556 5561 -- >27494 1 22
C202_FS_SZ_84 1556 5479 -- >11083 1 10
C202_FS_SZ_95 1556 5388 452 -- 59307 1 51 >5785322 35 56
C202_FS_SZ_97 1556 5452 11 -- 7823 1 46 >4687651 99 125
C202_FW_RZ_57 1561 7434 0.177 0.001 0.178 213 1 1 1 213 213
C202_FW_SZ_100 1561 7484 -- >21332 1 20
C202_FW_SZ_103 1561 9024 -- >4752 1 9
C202_FW_SZ_118 1561 7562 0.25 -- 257 1 2 >8388540 130 132
C202_FW_SZ_123 1561 7437 0.065 0.001 0.066 38 1 2 4 36 38
C202_FW_SZ_124 1561 7435 0.043 0 0.043 33 1 1 1 33 33
C202_FW_SZ_61 1561 7490 -- >8620 1 10
C202_FW_SZ_77 1561 7611 -- >11536 1 17
C202_FW_SZ_87 1561 7696 -- >14741 1 9
C202_FW_SZ_96 1561 7599 -- >14471 1 12
C202_FW_SZ_98 1561 7438 -- >7820 1 14
C202_FW_UT_2814 1820 9957 -- >8563 1 13
C202_FW_UT_2815 1820 9957 -- >8563 1 13
C208_FA_RZ_43 1516 4254 4.48 -- 4317 1 20 >117297 9 28
C208_FA_RZ_64 1516 4246 0.102 0 0.102 212 1 1 1 212 212
C208_FA_SZ_120 1516 4247 0.031 0 0.031 34 1 2 2 34 34
C208_FA_SZ_121 1516 4247 0.03 0 0.03 32 1 2 2 32 32
C208_FA_SZ_87 1516 4255 0.16 0.432 0.592 139 1 12 12884 18 27
C208_FA_UT_3254 1805 6153 0.166 0.214 0.38 155 1 4 17408 40 74
C208_FA_UT_3255 1805 6156 0.196 0.582 0.778 155 1 6 52736 40 74
C208_FC_RZ_65 1513 4491 -- >14291 1 18
C208_FC_RZ_70 1513 4468 0.11 0 0.11 212 1 1 1 212 212
C208_FC_SZ_107 1513 4554 -- >14650 1 17
C208_FC_SZ_127 1513 4469 0.026 0.001 0.027 34 1 1 1 34 34
C208_FC_SZ_128 1513 4469 0.028 0 0.028 32 1 1 1 32 32
C210_FS_RZ_23 1608 4911 -- >18402 1 22
C210_FS_RZ_38 1607 4900 63.9 -- 12715 1 141 >636225 46 58
C210_FS_RZ_40 1607 4891 0.126 0.001 0.127 212 1 2 15 140 173
C210_FS_SZ_103 1607 4915 -- >32098 1 27
C210_FS_SZ_107 1607 4902 108 -- 16511 1 141 >701928 49 64
C210_FS_SZ_123 1607 5062 0.286 -- 363 1 3 >8214647 112 234
C210_FS_SZ_129 1607 4894 0.03 0 0.03 33 1 1 1 33 33
C210_FS_SZ_130 1607 4894 0.028 0 0.028 31 1 1 1 31 31
C210_FS_SZ_55 1608 4917 -- >16262 1 21
C210_FS_SZ_78 1607 5071 -- >12999 1 19
C210_FW_RZ_30 1629 6407 -- >9594 1 15
C210_FW_RZ_57 1628 6390 179 -- 20007 1 213 >409094 48 58
C210_FW_RZ_59 1628 6381 0.152 0.001 0.153 212 1 2 15 140 173
C210_FW_SZ_106 1628 6405 -- >6111 1 15
C210_FW_SZ_111 1628 6393 255 -- 23625 1 179 >793636 43 51
C210_FW_SZ_128 1628 6401 -- >9884 1 23
C210_FW_SZ_129 1628 6595 0.597 -- 584 1 5 >4665615 238 281
C210_FW_SZ_135 1628 6384 0.041 0 0.041 33 1 1 1 33 33
C210_FW_SZ_136 1628 6384 0.038 0 0.038 31 1 1 1 31 31
C210_FW_SZ_80 1628 6560 -- >7123 1 13
C210_FW_SZ_90 1628 6977 -- >15686 1 12
C210_FW_SZ_91 1628 6709 -- >9869 1 10
C210_FW_UT_8630 1891 8511 -- >4193 1 11
C210_FW_UT_8634 1891 8504 -- >5899 1 11
C220_FV_RZ_12 1530 4017 0.133 0.935 1.068 150 1 6 80272 11 35
C220_FV_RZ_13 1530 4014 0.097 0.084 0.181 76 1 6 6772 10 27
C220_FV_RZ_14 1530 4013 0.038 0 0.038 20 1 3 80 11 18
C220_FV_SZ_114 1530 4305 5.79 -- 5654 1 55 >3115198 320 364
C220_FV_SZ_121 1530 4035 0.074 0 0.074 102 1 3 9 58 65
C220_FV_SZ_39 1530 4788 -- >32715 1 21
C220_FV_SZ_46 1530 4014 2.38 -- 1533 1 52 >7133318 40 71
C220_FV_SZ_55 1530 5281 8.93 -- 3974 1 22 >391876 664 670
C220_FV_SZ_65 1530 4014 0.32 2.05 2.37 198 1 26 103442 23 40