BerkMin
22 groups, 251 instances, 2-hour cutoff
Instances solved: 185 (70 SAT + 115 UNSAT)
Time: 715885 seconds / 198.86 hours / 8.29 days
Time on solved instances: 240685 seconds (116717 SAT + 123968 UNSAT)
Instances solved in 10 minutes: 99 (8567 seconds)
Instances solved in 15 minutes: 115 (20409 seconds)
Instances solved in 20 minutes: 121 (26886 seconds)
Instances solved in 30 minutes: 139 (53532 seconds)
Instances solved in 60 minutes: 161 (109588 seconds)
Instances solved in 90 minutes: 172 (159644 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 29 | / | 32 | 74797.02 | ||
engine_unsat_1.0 | 8 | / | 10 | 6924.38 | ||
fvp-sat.3.0 | 20 | / | 20 | 12673.21 | ||
fvp-unsat.1.0 | 4 | / | 4 | 41.68 | ||
fvp-unsat.2.0 | 22 | / | 22 | 437.57 | ||
fvp-unsat.3.0 | 1 | / | 6 | 2790.7 | ||
liveness_sat_1.0 | 5 | / | 10 | 9252.39 | ||
liveness_unsat_1.0 | 4 | / | 12 | 831.14 | ||
liveness_unsat_2.0 | 3 | / | 9 | 48.94 | ||
npe-1.0 | 3 | / | 6 | 212.38 | ||
pipe_ooo_unsat_1.0 | 8 | / | 15 | 6230.63 | ||
pipe_ooo_unsat_1.1 | 9 | / | 14 | 7431.44 | ||
pipe_sat_1.0 | 10 | / | 10 | 32313.91 | ||
pipe_sat_1.1 | 10 | / | 10 | 5565.12 | ||
pipe_unsat_1.0 | 10 | / | 13 | 9157.06 | ||
pipe_unsat_1.1 | 12 | / | 14 | 9744.46 | ||
vliw_sat_2.0 | 9 | / | 9 | 24183.27 | ||
vliw_sat_2.1 | 1 | / | 10 | 622.01 | ||
vliw_sat_4.0 | 10 | / | 10 | 18517.35 | ||
vliw_unsat_2.0 | 5 | / | 9 | 11406.46 | ||
vliw_unsat_3.0 | 0 | / | 2 | 0 | ||
vliw_unsat_4.0 | 2 | / | 4 | 7503.72 |
dlx_iq_unsat_1.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq42_a.cnf | 7195972 | 177995 | 8 | 1104.480 | UNSAT |
1dlx_c_iq43_a.cnf | 7153579 | 174671 | 8 | 1154.910 | UNSAT |
1dlx_c_iq44_a.cnf | 7233951 | 167421 | 7 | 1260.680 | UNSAT |
1dlx_c_iq45_a.cnf | 7945334 | 192929 | 8 | 1391.840 | UNSAT |
1dlx_c_iq46_a.cnf | 9530159 | 196249 | 7 | 1719.770 | UNSAT |
1dlx_c_iq47_a.cnf | 9923102 | 195467 | 8 | 1740.620 | UNSAT |
1dlx_c_iq48_a.cnf | 10659628 | 198425 | 8 | 1889.040 | UNSAT |
1dlx_c_iq49_a.cnf | 11441420 | 213200 | 8 | 2324.150 | UNSAT |
1dlx_c_iq50_a.cnf | 12528536 | 226463 | 9 | 2374.970 | UNSAT |
1dlx_c_iq51_a.cnf | 13759934 | 247024 | 9 | 2711.940 | UNSAT |
1dlx_c_iq33_a.cnf | 2768772 | 97161 | 8 | 329.270 | UNSAT |
1dlx_c_iq52_a.cnf | 16340791 | 234185 | 8 | 2971.580 | UNSAT |
1dlx_c_iq53_a.cnf | 15548547 | 281220 | 9 | 3304.410 | UNSAT |
1dlx_c_iq54_a.cnf | |||||
1dlx_c_iq55_a.cnf | 19151300 | 277579 | 9 | 3954.130 | UNSAT |
1dlx_c_iq56_a.cnf | 18765586 | 338814 | 10 | 4306.950 | UNSAT |
1dlx_c_iq57_a.cnf | 21059016 | 328189 | 10 | 4782.700 | UNSAT |
1dlx_c_iq58_a.cnf | 22495864 | 349636 | 10 | 5243.700 | UNSAT |
1dlx_c_iq59_a.cnf | 22864798 | 376616 | 11 | 5711.400 | UNSAT |
1dlx_c_iq60_a.cnf | 26236252 | 362637 | 11 | 6040.880 | UNSAT |
1dlx_c_iq61_a.cnf | 25748310 | 339466 | 10 | 6371.740 | SAT |
1dlx_c_iq34_a.cnf | 3004827 | 104871 | 8 | 364.520 | UNSAT |
1dlx_c_iq62_a.cnf | |||||
1dlx_c_iq63_a.cnf | 24485292 | 332984 | 10 | 6964.640 | SAT |
1dlx_c_iq64_a.cnf | |||||
1dlx_c_iq35_a.cnf | 3794205 | 113208 | 8 | 470.910 | UNSAT |
1dlx_c_iq36_a.cnf | 7673204 | 118146 | 7 | 1394.250 | UNSAT |
1dlx_c_iq37_a.cnf | 9415222 | 131298 | 7 | 1774.050 | UNSAT |
1dlx_c_iq38_a.cnf | 4632216 | 131464 | 8 | 634.630 | UNSAT |
1dlx_c_iq39_a.cnf | 5281767 | 138791 | 7 | 734.600 | UNSAT |
1dlx_c_iq40_a.cnf | 5919575 | 152494 | 7 | 852.590 | UNSAT |
1dlx_c_iq41_a.cnf | 6199943 | 151638 | 7 | 917.670 | UNSAT |
Total (29 / 32) | 358757102 | 6350241 | 245 | 74797.02 |
engine_unsat_1.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
engine_4.cnf | 56269 | 36436 | 39 | 7.920 | UNSAT |
engine_4_nd.cnf | 199145 | 146628 | 144 | 40.950 | UNSAT |
engine_5.cnf | 1007017 | 771381 | 235 | 601.520 | UNSAT |
engine_5_case1.cnf | 29843 | 22771 | 11 | 8.970 | UNSAT |
engine_5_nd.cnf | 5749705 | 4654551 | 1382 | 5746.730 | UNSAT |
engine_5_nd_case1.cnf | 72735 | 56094 | 20 | 23.040 | UNSAT |
engine_6.cnf | |||||
engine_6_case1.cnf | 86029 | 68151 | 11 | 54.020 | UNSAT |
engine_6_nd.cnf | |||||
engine_6_nd_case1.cnf | 493078 | 419390 | 49 | 441.230 | UNSAT |
Total (8 / 10) | 7693821 | 6175402 | 1891 | 6924.38 |
fvp-sat.3.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 280696 | 19247 | 2 | 31.430 | SAT |
pipe_64_4_bug02.cnf | 9717796 | 1277977 | 81 | 2111.290 | SAT |
pipe_64_4_bug03.cnf | 12035 | 725 | 1 | 3.110 | SAT |
pipe_64_4_bug04.cnf | 39744 | 1604 | 1 | 9.370 | SAT |
pipe_64_4_bug05.cnf | 5785416 | 760879 | 49 | 1226.870 | SAT |
pipe_64_4_bug06.cnf | 5895955 | 846931 | 54 | 1109.400 | SAT |
pipe_64_4_bug07.cnf | 6382440 | 909116 | 58 | 1297.580 | SAT |
pipe_64_4_bug08.cnf | 344637 | 19387 | 2 | 39.780 | SAT |
pipe_64_4_bug09.cnf | 577519 | 45707 | 3 | 60.140 | SAT |
pipe_64_4_bug10.cnf | 146498 | 7512 | 1 | 20.130 | SAT |
pipe_64_4_bug11.cnf | 2548599 | 340231 | 22 | 399.120 | SAT |
pipe_64_4_bug12.cnf | 639859 | 46114 | 3 | 67.270 | SAT |
pipe_64_4_bug13.cnf | 1401904 | 128954 | 9 | 149.610 | SAT |
pipe_64_4_bug14.cnf | 397402 | 20163 | 2 | 44.350 | SAT |
pipe_64_4_bug15.cnf | 9797068 | 1334830 | 85 | 2104.750 | SAT |
pipe_64_4_bug16.cnf | 4064510 | 498580 | 32 | 766.370 | SAT |
pipe_64_4_bug17.cnf | 5961992 | 814923 | 52 | 1235.750 | SAT |
pipe_64_4_bug18.cnf | 5156486 | 639605 | 41 | 811.670 | SAT |
pipe_64_4_bug19.cnf | 2708035 | 346465 | 22 | 393.980 | SAT |
pipe_64_4_bug20.cnf | 4767987 | 639024 | 41 | 791.240 | SAT |
Total (20 / 20) | 66626578 | 8697974 | 561 | 12673.21 |
fvp-unsat.1.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_mc_ex_bp_f.cnf | 2251 | 618 | 6 | 0.010 | UNSAT |
2dlx_ca_mc_ex_bp_f.cnf | 24863 | 4378 | 12 | 0.320 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 40633 | 11178 | 22 | 1.050 | UNSAT |
9vliw_bp_mc.cnf | 2106153 | 78267 | 30 | 40.300 | UNSAT |
Total (4 / 4) | 2173900 | 94441 | 70 | 41.68 |
fvp-unsat.2.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 3944 | 1228 | 5 | 0.030 | UNSAT |
2pipe_1_ooo.cnf | 2342 | 1172 | 6 | 0.030 | UNSAT |
2pipe_2_ooo.cnf | 2714 | 1298 | 6 | 0.040 | UNSAT |
3pipe.cnf | 27451 | 7467 | 18 | 0.480 | UNSAT |
3pipe_1_ooo.cnf | 13031 | 6352 | 16 | 0.390 | UNSAT |
3pipe_2_ooo.cnf | 18726 | 8608 | 19 | 0.630 | UNSAT |
3pipe_3_ooo.cnf | 22206 | 9744 | 22 | 0.760 | UNSAT |
4pipe.cnf | 106099 | 21231 | 19 | 2.800 | UNSAT |
4pipe_1_ooo.cnf | 58457 | 26545 | 26 | 3.420 | UNSAT |
4pipe_2_ooo.cnf | 54502 | 22606 | 21 | 3.310 | UNSAT |
4pipe_3_ooo.cnf | 70512 | 27555 | 22 | 4.350 | UNSAT |
4pipe_4_ooo.cnf | 77375 | 27882 | 20 | 5.040 | UNSAT |
5pipe.cnf | 230894 | 16169 | 8 | 4.290 | UNSAT |
5pipe_1_ooo.cnf | 109835 | 44046 | 18 | 10.470 | UNSAT |
5pipe_2_ooo.cnf | 107762 | 38373 | 15 | 10.040 | UNSAT |
5pipe_3_ooo.cnf | 117212 | 41795 | 17 | 11.930 | UNSAT |
5pipe_4_ooo.cnf | 225310 | 85934 | 28 | 24.360 | UNSAT |
5pipe_5_ooo.cnf | 115593 | 35449 | 13 | 12.240 | UNSAT |
6pipe.cnf | 765554 | 128571 | 24 | 50.930 | UNSAT |
6pipe_6_ooo.cnf | 344042 | 109757 | 16 | 57.360 | UNSAT |
7pipe.cnf | 1311063 | 283785 | 28 | 169.210 | UNSAT |
7pipe_bug.cnf | 794211 | 91521 | 9 | 65.460 | SAT |
Total (22 / 22) | 4578835 | 1037088 | 376 | 437.57 |
fvp-unsat.3.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_01.cnf | |||||
pipe_64_02.cnf | |||||
pipe_64_04.cnf | 11099896 | 1595388 | 103 | 2790.700 | UNSAT |
pipe_64_08.cnf | |||||
pipe_64_16.cnf | |||||
pipe_64_32.cnf | |||||
Total (1 / 6) | 11099896 | 1595388 | 103 | 2790.7 |
liveness_sat_1.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
2dlx_cc_ex_bp_f_bug5_liveness.cnf | 2933018 | 748220 | 17 | 4782.400 | SAT |
2dlx_cc_ex_bp_f_bug6_liveness.cnf | |||||
2dlx_cc_ex_bp_f_bug7_liveness.cnf | |||||
2dlx_cc_ex_bp_f_bug8_liveness.cnf | |||||
2dlx_cc_ex_bp_f_bug9_liveness.cnf | |||||
2dlx_cc_ex_bp_f_bug10_liveness.cnf | |||||
2dlx_cc_ex_bp_f_bug1_liveness.cnf | 515110 | 97797 | 5 | 415.860 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 365329 | 62623 | 4 | 288.030 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 1793818 | 435427 | 11 | 2402.340 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 1136072 | 254967 | 7 | 1363.760 | SAT |
Total (5 / 10) | 6743347 | 1599034 | 44 | 9252.39 |
liveness_unsat_1.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 154328 | 77374 | 48 | 21.150 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 1557163 | 909913 | 174 | 772.660 | UNSAT |
1dlx_c_ex_liveness.cnf | 171086 | 82115 | 30 | 35.010 | UNSAT |
1dlx_c_liveness.cnf | 41813 | 18487 | 22 | 2.320 | UNSAT |
2dlx_ca_bp_f_liveness.cnf | |||||
2dlx_ca_ex_bp_f_liveness.cnf | |||||
2dlx_ca_ex_liveness.cnf | |||||
2dlx_ca_liveness.cnf | |||||
2dlx_cc_bp_f_liveness.cnf | |||||
2dlx_cc_ex_bp_f_liveness.cnf | |||||
2dlx_cc_ex_liveness.cnf | |||||
2dlx_cc_liveness.cnf | |||||
Total (4 / 12) | 1924390 | 1087889 | 274 | 831.14 |
liveness_unsat_2.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 46693 | 16480 | 20 | 2.280 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 196627 | 87044 | 38 | 27.270 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 131742 | 62702 | 23 | 19.390 | UNSAT |
2dlx_ca_bp_u_f_liveness.cnf | |||||
2dlx_ca_ex_bp_u_f_liveness.cnf | |||||
2dlx_ca_ex_d_liveness.cnf | |||||
2dlx_cc_bp_u_f_liveness.cnf | |||||
2dlx_cc_ex_bp_u_f_liveness.cnf | |||||
2dlx_cc_ex_d_liveness.cnf | |||||
Total (3 / 9) | 375062 | 166226 | 81 | 48.94 |
npe-1.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 544 | 47 | 1 | 0.010 | SAT |
1dlx_c_no_pe.cnf | 230181 | 162434 | 296 | 24.920 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 381300 | 107125 | 7 | 187.450 | SAT |
2dlx_cc_mc_ex_bp_f2_no_pe.cnf | |||||
9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf | |||||
9dlx_vliw_at_bp_mc2_no_pe.cnf | |||||
Total (3 / 6) | 612025 | 269606 | 304 | 212.38 |
pipe_ooo_unsat_1.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
10pipe_10_ooo.cnf | |||||
11pipe_11_ooo.cnf | |||||
12pipe_12_ooo.cnf | |||||
13pipe_13_ooo.cnf | |||||
14pipe_14_ooo.cnf | |||||
15pipe_15_ooo.cnf | |||||
16pipe_16_ooo.cnf | |||||
2pipe_2_ooo.cnf | 2786 | 1384 | 7 | 0.040 | UNSAT |
3pipe_3_ooo.cnf | 27480 | 12719 | 26 | 1.030 | UNSAT |
4pipe_4_ooo.cnf | 96284 | 37332 | 30 | 7.040 | UNSAT |
5pipe_5_ooo.cnf | 287825 | 101522 | 36 | 37.220 | UNSAT |
6pipe_6_ooo.cnf | 805160 | 301387 | 52 | 172.970 | UNSAT |
7pipe_7_ooo.cnf | 2176848 | 851290 | 80 | 814.060 | UNSAT |
8pipe_8_ooo.cnf | 4960036 | 1856263 | 103 | 2598.620 | UNSAT |
9pipe_9_ooo.cnf | 4115975 | 1446053 | 52 | 2599.650 | UNSAT |
Total (8 / 15) | 12472394 | 4607950 | 386 | 6230.63 |
pipe_ooo_unsat_1.1
CNF | Decisions | Conflicts | Restarts | Time | Sol |
10pipe_10_ooo_q0_T0.cnf | 16476937 | 2692738 | 86 | 5600.210 | UNSAT |
11pipe_11_ooo_q0_T0.cnf | |||||
12pipe_12_ooo_q0_T0.cnf | |||||
13pipe_13_ooo_q0_T0.cnf | |||||
14pipe_14_ooo_q0_T0.cnf | |||||
15pipe_15_ooo_q0_T0.cnf | |||||
2pipe_2_ooo_q0_T0.cnf | 4354 | 1737 | 8 | 0.050 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 32108 | 9029 | 21 | 0.610 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 103046 | 22642 | 24 | 3.390 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 301603 | 47724 | 22 | 14.530 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 755819 | 103658 | 25 | 54.420 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 1855147 | 238276 | 32 | 196.720 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 4419711 | 647958 | 50 | 745.860 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 4896882 | 513530 | 27 | 815.650 | UNSAT |
Total (9 / 14) | 28845607 | 4277292 | 295 | 7431.44 |
pipe_sat_1.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 4831032 | 2128107 | 44 | 7222.150 | SAT |
12pipe_bug10.cnf | 388014 | 46530 | 1 | 249.930 | SAT |
12pipe_bug2.cnf | 338142 | 40425 | 1 | 214.840 | SAT |
12pipe_bug3.cnf | 4599730 | 1889821 | 39 | 6523.020 | SAT |
12pipe_bug4.cnf | 914571 | 153325 | 4 | 673.170 | SAT |
12pipe_bug5.cnf | 3807003 | 1656104 | 35 | 5203.800 | SAT |
12pipe_bug6.cnf | 452 | 40 | 1 | 3.790 | SAT |
12pipe_bug7.cnf | 4051629 | 1948800 | 40 | 5947.630 | SAT |
12pipe_bug8.cnf | 17256 | 1054 | 1 | 12.960 | SAT |
12pipe_bug9.cnf | 4350063 | 1869240 | 39 | 6262.620 | SAT |
Total (10 / 10) | 23297892 | 9733446 | 205 | 32313.91 |
pipe_sat_1.1
CNF | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 63619 | 4532 | 1 | 29.170 | SAT |
12pipe_bug1_q0.cnf | 304685 | 23283 | 1 | 147.460 | SAT |
12pipe_bug2_q0.cnf | 342257 | 26867 | 1 | 167.030 | SAT |
12pipe_bug3_q0.cnf | 268586 | 24946 | 1 | 144.450 | SAT |
12pipe_bug4_q0.cnf | 237913 | 14701 | 2 | 96.480 | SAT |
12pipe_bug5_q0.cnf | 2892236 | 329481 | 8 | 1730.160 | SAT |
12pipe_bug6_q0.cnf | 108162 | 7226 | 1 | 48.320 | SAT |
12pipe_bug7_q0.cnf | 2549606 | 283885 | 7 | 1505.800 | SAT |
12pipe_bug8_q0.cnf | 10920 | 676 | 1 | 5.820 | SAT |
12pipe_bug9_q0.cnf | 2843561 | 323160 | 7 | 1690.430 | SAT |
Total (10 / 10) | 9621545 | 1038757 | 30 | 5565.12 |
pipe_unsat_1.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 3468 | 1399 | 8 | 0.040 | UNSAT |
03pipe_k.cnf | 22987 | 7961 | 17 | 0.530 | UNSAT |
04pipe_k.cnf | 93106 | 25692 | 23 | 3.270 | UNSAT |
05pipe_k.cnf | 243498 | 44525 | 18 | 10.980 | UNSAT |
06pipe_k.cnf | 381865 | 28187 | 7 | 12.460 | UNSAT |
07pipe_k.cnf | 1675238 | 386730 | 36 | 271.510 | UNSAT |
08pipe_k.cnf | 2881023 | 555634 | 30 | 506.610 | UNSAT |
09pipe_k.cnf | 3158415 | 118383 | 6 | 202.320 | UNSAT |
10pipe_k.cnf | 9554261 | 1432480 | 32 | 2682.420 | UNSAT |
11pipe_k.cnf | 16927538 | 2370986 | 51 | 5466.920 | UNSAT |
12pipe_k.cnf | |||||
13pipe_k.cnf | |||||
14pipe_k.cnf | |||||
Total (10 / 13) | 34941399 | 4971977 | 228 | 9157.06 |
pipe_unsat_1.1
CNF | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 3792 | 1293 | 5 | 0.040 | UNSAT |
03pipe_q0_k.cnf | 24049 | 6312 | 14 | 0.390 | UNSAT |
04pipe_q0_k.cnf | 84172 | 15549 | 16 | 2.060 | UNSAT |
05pipe_q0_k.cnf | 255168 | 32799 | 15 | 8.900 | UNSAT |
06pipe_q0_k.cnf | 427805 | 25183 | 7 | 15.790 | UNSAT |
07pipe_q0_k.cnf | 1061437 | 86101 | 11 | 66.120 | UNSAT |
08pipe_q0_k.cnf | 1811419 | 112051 | 10 | 138.460 | UNSAT |
09pipe_q0_k.cnf | 3002400 | 79843 | 5 | 289.970 | UNSAT |
10pipe_q0_k.cnf | 5243509 | 235504 | 9 | 656.820 | UNSAT |
11pipe_q0_k.cnf | 8651593 | 290846 | 8 | 1271.050 | UNSAT |
12pipe_q0_k.cnf | 14292081 | 419761 | 10 | 2545.670 | UNSAT |
13pipe_q0_k.cnf | 20597692 | 519970 | 12 | 4749.190 | UNSAT |
14pipe_q0_k.cnf | |||||
15pipe_q0_k.cnf | |||||
Total (12 / 14) | 55455117 | 1825212 | 122 | 9744.46 |
vliw_sat_2.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 10619427 | 803569 | 20 | 3892.980 | SAT |
9dlx_vliw_at_b_iq6_bug2.cnf | 86242 | 923 | 1 | 68.600 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 6174591 | 516201 | 13 | 2379.740 | SAT |
9dlx_vliw_at_b_iq6_bug4.cnf | 11211740 | 919401 | 21 | 4260.680 | SAT |
9dlx_vliw_at_b_iq6_bug5.cnf | 12643099 | 1025787 | 24 | 4692.560 | SAT |
9dlx_vliw_at_b_iq6_bug6.cnf | 733694 | 35132 | 3 | 357.420 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 5451217 | 444824 | 12 | 1663.110 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 7136117 | 597539 | 15 | 2680.690 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 10945291 | 930463 | 21 | 4187.490 | SAT |
Total (9 / 9) | 65001418 | 5273839 | 130 | 24183.27 |
vliw_sat_2.1
CNF | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq8_bug1.cnf | |||||
9dlx_vliw_at_b_iq8_bug10.cnf | |||||
9dlx_vliw_at_b_iq8_bug2.cnf | |||||
9dlx_vliw_at_b_iq8_bug3.cnf | |||||
9dlx_vliw_at_b_iq8_bug4.cnf | |||||
9dlx_vliw_at_b_iq8_bug5.cnf | |||||
9dlx_vliw_at_b_iq8_bug6.cnf | |||||
9dlx_vliw_at_b_iq8_bug7.cnf | 726016 | 29937 | 3 | 622.010 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | |||||
9dlx_vliw_at_b_iq8_bug9.cnf | |||||
Total (1 / 10) | 726016 | 29937 | 3 | 622.01 |
vliw_sat_4.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug1.cnf | 5383465 | 143444 | 5 | 2957.080 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 1606489 | 15853 | 2 | 1085.900 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 1722056 | 14077 | 3 | 1206.640 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 2723276 | 31674 | 3 | 1720.640 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 3893464 | 73367 | 3 | 2198.530 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 5048678 | 159602 | 6 | 2869.850 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 966048 | 6208 | 2 | 719.330 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 2189689 | 21693 | 2 | 1453.120 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 3848466 | 83817 | 3 | 2324.830 | SAT |
9vliw_m_9stages_iq3_C1_bug9.cnf | 3194660 | 54471 | 4 | 1981.430 | SAT |
Total (10 / 10) | 30576291 | 604206 | 33 | 18517.35 |
vliw_unsat_2.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 3633371 | 199044 | 51 | 112.540 | UNSAT |
9dlx_vliw_at_b_iq2.cnf | 10253447 | 357412 | 46 | 428.760 | UNSAT |
9dlx_vliw_at_b_iq3.cnf | 20402798 | 512304 | 38 | 1104.630 | UNSAT |
9dlx_vliw_at_b_iq4.cnf | 44138768 | 835052 | 38 | 3252.160 | UNSAT |
9dlx_vliw_at_b_iq5.cnf | 72408152 | 976284 | 29 | 6508.370 | UNSAT |
9dlx_vliw_at_b_iq6.cnf | |||||
9dlx_vliw_at_b_iq7.cnf | |||||
9dlx_vliw_at_b_iq8.cnf | |||||
9dlx_vliw_at_b_iq9.cnf | |||||
Total (5 / 9) | 150836536 | 2880096 | 202 | 11406.46 |
vliw_unsat_3.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq8_I3_C24.cnf | |||||
9dlx_vliw_at_b_iq8_I3_C24_D.cnf | |||||
Total (0 / 2) | 0 |
vliw_unsat_4.0
CNF | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_C1.cnf | 4784887 | 479450 | 20 | 829.600 | UNSAT |
9vliw_m_9stages_iq1_C1.cnf | 20732556 | 2358649 | 51 | 6674.120 | UNSAT |
9vliw_m_9stages_iq2_C1.cnf | |||||
9vliw_m_9stages_iq3_C1.cnf | |||||
Total (2 / 4) | 25517443 | 2838099 | 71 | 7503.72 |