Tinisat, using restart policy (Luby's, unit=32)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 180 (70 SAT + 110 UNSAT)
Time: 663486 seconds / 184.30 hours / 7.68 days
Time on solved instances: 152286 seconds (51890 SAT + 100396 UNSAT)
Instances solved in 10 minutes: 114 (10754 seconds)
Instances solved in 15 minutes: 125 (18657 seconds)
Instances solved in 20 minutes: 135 (29107 seconds)
Instances solved in 30 minutes: 151 (51275 seconds)
Instances solved in 60 minutes: 168 (96119 seconds)
Instances solved in 90 minutes: 177 (133865 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 32 | / | 32 | 64798.03 | ||
engine_unsat_1.0 | 7 | / | 10 | 2397.64 | ||
fvp-sat.3.0 | 14 | / | 20 | 3307.93 | ||
fvp-unsat.1.0 | 4 | / | 4 | 37.38 | ||
fvp-unsat.2.0 | 22 | / | 22 | 469.3 | ||
fvp-unsat.3.0 | 0 | / | 6 | 0 | ||
liveness_sat_1.0 | 7 | / | 10 | 9806.83 | ||
liveness_unsat_1.0 | 4 | / | 12 | 1348.96 | ||
liveness_unsat_2.0 | 3 | / | 9 | 63.53 | ||
npe-1.0 | 3 | / | 6 | 305.07 | ||
pipe_ooo_unsat_1.0 | 7 | / | 15 | 6017.97 | ||
pipe_ooo_unsat_1.1 | 8 | / | 14 | 2981.83 | ||
pipe_sat_1.0 | 10 | / | 10 | 5696.35 | ||
pipe_sat_1.1 | 10 | / | 10 | 3875.28 | ||
pipe_unsat_1.0 | 9 | / | 13 | 3505.45 | ||
pipe_unsat_1.1 | 11 | / | 14 | 8993.14 | ||
vliw_sat_2.0 | 9 | / | 9 | 11192.47 | ||
vliw_sat_2.1 | 5 | / | 10 | 9564.96 | ||
vliw_sat_4.0 | 10 | / | 10 | 1488.98 | ||
vliw_unsat_2.0 | 2 | / | 9 | 3875.04 | ||
vliw_unsat_3.0 | 2 | / | 2 | 11407.67 | ||
vliw_unsat_4.0 | 1 | / | 4 | 1152.52 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 5877959 | 176034 | 1148 | 870.80 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 6666426 | 172163 | 1116 | 956.94 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 6893109 | 195614 | 1277 | 1086.49 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 7297763 | 194646 | 1277 | 1165.29 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 7971549 | 208155 | 1403 | 1315.98 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 8452049 | 216574 | 1467 | 1401.25 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 9408807 | 213314 | 1435 | 1523.58 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 9365161 | 220453 | 1513 | 1603.57 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 10925804 | 241438 | 1586 | 1834.55 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 12249187 | 256928 | 1722 | 2065.15 | UNSAT |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2604080 | 119934 | 892 | 369.11 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 13073802 | 281178 | 1913 | 2364.61 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 13502404 | 262963 | 1785 | 2353.97 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | 13382909 | 309591 | 2044 | 3797.73 | UNSAT |
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 15368621 | 286898 | 1946 | 2778.67 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 16236612 | 300910 | 2043 | 2999.96 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 17515480 | 313059 | 2045 | 3281.89 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | 19752348 | 330382 | 2046 | 3602.17 | UNSAT |
1dlx_c_iq59_a.cnf | 623700 | 9457051 | 19245125 | 330586 | 2046 | 3750.61 | UNSAT |
1dlx_c_iq60_a.cnf | 651875 | 9927770 | 21078489 | 344952 | 2046 | 4024.72 | UNSAT |
1dlx_c_iq61_a.cnf | 673311 | 10435991 | 19607987 | 300566 | 2043 | 3798.72 | SAT |
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 2839179 | 120279 | 892 | 391.80 | UNSAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | 24263137 | 369060 | 2140 | 4603.74 | UNSAT |
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 12374397 | 234230 | 1533 | 2890.91 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | 27450420 | 393484 | 2308 | 5407.92 | UNSAT |
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 3179339 | 128237 | 976 | 446.49 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 3417288 | 138507 | 1020 | 655.87 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 3730812 | 142237 | 1021 | 718.89 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 4238705 | 140802 | 1021 | 607.71 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 4567307 | 139347 | 1021 | 639.04 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 4935925 | 146857 | 1021 | 690.30 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 5313559 | 163926 | 1025 | 799.60 | UNSAT |
Total (32 / 32) | 352785739 | 7393304 | 48771 | 64798.03 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_4.cnf | 6944 | 66654 | 54025 | 33204 | 263 | 13.55 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 157071 | 107214 | 779 | 78.74 | UNSAT |
engine_5.cnf | 18788 | 214095 | 859222 | 595076 | 3580 | 1784.08 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 19590 | 11951 | 125 | 7.04 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 60385 | 41340 | 348 | 30.78 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 75702 | 49877 | 418 | 68.38 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | |||||
engine_6_nd_case1.cnf | 45435 | 610120 | 282286 | 205952 | 1384 | 415.07 | UNSAT |
Total (7 / 10) | 1508281 | 1044614 | 6897 | 2397.64 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | |||||
pipe_64_4_bug02.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug03.cnf | 35947 | 992674 | 162562 | 1466 | 23 | 3.89 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 429112 | 4467 | 60 | 7.36 | SAT |
pipe_64_4_bug05.cnf | 35853 | 1012271 | 3880737 | 302068 | 2043 | 310.45 | SAT |
pipe_64_4_bug06.cnf | 35853 | 1012271 | 2853828 | 201442 | 1339 | 175.19 | SAT |
pipe_64_4_bug07.cnf | 35853 | 1012271 | 8012382 | 739750 | 4094 | 1280.70 | SAT |
pipe_64_4_bug08.cnf | 35622 | 1003074 | 21538 | 36 | 1 | 2.00 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 25900 | 56 | 1 | 2.19 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 25552 | 37 | 1 | 2.01 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | 8534770 | 766996 | 4094 | 1289.52 | SAT |
pipe_64_4_bug12.cnf | 35854 | 1012275 | 2402807 | 103282 | 765 | 87.01 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 658782 | 21487 | 204 | 17.31 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 25291 | 38 | 1 | 2.03 | SAT |
pipe_64_4_bug15.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug16.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug17.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug18.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug19.cnf | 35852 | 1012266 | 25665 | 53 | 1 | 2.04 | SAT |
pipe_64_4_bug20.cnf | 35853 | 1012271 | 2615515 | 159747 | 1022 | 126.23 | SAT |
Total (14 / 20) | 29674441 | 2300925 | 13649 | 3307.93 |
fvp-unsat.1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_mc_ex_bp_f.cnf | 776 | 3725 | 2543 | 739 | 13 | 0.03 | UNSAT |
2dlx_ca_mc_ex_bp_f.cnf | 3250 | 24640 | 20323 | 5680 | 62 | 0.51 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 34086 | 9000 | 100 | 1.11 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 477168 | 82748 | 611 | 35.73 | UNSAT |
Total (4 / 4) | 534120 | 98167 | 786 | 37.38 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 2938 | 1066 | 16 | 0.04 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 2766 | 1210 | 19 | 0.05 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 3133 | 1412 | 22 | 0.06 | UNSAT |
3pipe.cnf | 2468 | 27533 | 20805 | 7599 | 86 | 0.72 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 15806 | 6257 | 65 | 0.59 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 23500 | 10164 | 117 | 1.14 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 23423 | 9038 | 100 | 1.05 | UNSAT |
4pipe.cnf | 5237 | 80213 | 80798 | 25041 | 250 | 6.17 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 56859 | 22797 | 220 | 5.06 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 74383 | 26652 | 253 | 6.70 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 76519 | 23385 | 227 | 6.22 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 88729 | 29030 | 254 | 8.17 | UNSAT |
5pipe.cnf | 9471 | 195452 | 131655 | 14135 | 126 | 4.67 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 104141 | 31560 | 254 | 12.43 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 123345 | 33414 | 268 | 15.02 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 120410 | 30881 | 254 | 13.96 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 236519 | 64407 | 509 | 35.57 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 121361 | 30269 | 254 | 15.50 | UNSAT |
6pipe.cnf | 15800 | 394739 | 453483 | 88171 | 640 | 73.44 | UNSAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 404756 | 85444 | 636 | 81.42 | UNSAT |
7pipe.cnf | 23910 | 751118 | 876368 | 130092 | 998 | 171.05 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 144616 | 14526 | 131 | 10.27 | SAT |
Total (22 / 22) | 3186313 | 686550 | 5699 | 469.3 |
fvp-unsat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_01.cnf | 40347 | 1224040 | |||||
pipe_64_02.cnf | 41774 | 1269338 | |||||
pipe_64_04.cnf | 35853 | 1012270 | |||||
pipe_64_08.cnf | 50879 | 1622874 | |||||
pipe_64_16.cnf | 64262 | 2291120 | |||||
pipe_64_32.cnf | 95179 | 4396018 | |||||
Total (0 / 6) | 0 |
liveness_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2dlx_cc_ex_bp_f_bug10_liveness.cnf | 536469 | 10122798 | |||||
2dlx_cc_ex_bp_f_bug1_liveness.cnf | 171648 | 2614464 | 51759 | 4197 | 58 | 27.70 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 269774 | 37289 | 315 | 181.81 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 308913 | 41364 | 348 | 223.60 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 926809 | 165982 | 1053 | 924.31 | SAT |
2dlx_cc_ex_bp_f_bug5_liveness.cnf | 292249 | 4906188 | 970078 | 169184 | 1085 | 1074.18 | SAT |
2dlx_cc_ex_bp_f_bug6_liveness.cnf | 331848 | 5706594 | 3446640 | 783725 | 4094 | 6896.44 | SAT |
2dlx_cc_ex_bp_f_bug7_liveness.cnf | 375775 | 6617342 | 467753 | 59192 | 507 | 478.79 | SAT |
2dlx_cc_ex_bp_f_bug8_liveness.cnf | 424320 | 7649214 | |||||
2dlx_cc_ex_bp_f_bug9_liveness.cnf | 477782 | 8813656 | |||||
Total (7 / 10) | 6441726 | 1260933 | 7460 | 9806.83 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 126183 | 57404 | 502 | 32.59 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 849622 | 456894 | 2778 | 1277.44 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 119574 | 50080 | 420 | 35.21 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 36745 | 16979 | 160 | 3.72 | UNSAT |
2dlx_ca_bp_f_liveness.cnf | 202253 | 4313014 | |||||
2dlx_ca_ex_bp_f_liveness.cnf | 421107 | 8754014 | |||||
2dlx_ca_ex_liveness.cnf | 318771 | 7410689 | |||||
2dlx_ca_liveness.cnf | 115049 | 2148917 | |||||
2dlx_cc_bp_f_liveness.cnf | 267364 | 6003507 | |||||
2dlx_cc_ex_bp_f_liveness.cnf | 600698 | 11589474 | |||||
2dlx_cc_ex_liveness.cnf | 352057 | 7935053 | |||||
2dlx_cc_liveness.cnf | 122395 | 2149255 | |||||
Total (4 / 12) | 1132124 | 581357 | 3860 | 1348.96 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 48473 | 17780 | 172 | 4.25 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 150477 | 61072 | 508 | 36.85 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 93478 | 37805 | 316 | 22.43 | UNSAT |
2dlx_ca_bp_u_f_liveness.cnf | 121388 | 2001843 | |||||
2dlx_ca_ex_bp_u_f_liveness.cnf | 223527 | 3922017 | |||||
2dlx_ca_ex_d_liveness.cnf | 235853 | 5459971 | |||||
2dlx_cc_bp_u_f_liveness.cnf | 144071 | 2411213 | |||||
2dlx_cc_ex_bp_u_f_liveness.cnf | 258649 | 4520142 | |||||
2dlx_cc_ex_d_liveness.cnf | 266476 | 6144987 | |||||
Total (3 / 9) | 292428 | 116657 | 996 | 63.53 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 10949 | 4359 | 60 | 0.53 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 133536 | 87201 | 637 | 47.57 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 462936 | 112583 | 828 | 256.97 | SAT |
2dlx_cc_mc_ex_bp_f2_no_pe.cnf | 96675 | 1401773 | |||||
9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf | 889302 | 14582074 | |||||
9dlx_vliw_at_bp_mc2_no_pe.cnf | 889302 | 14582081 | |||||
Total (3 / 6) | 607421 | 204143 | 1525 | 305.07 |
pipe_ooo_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
10pipe_10_ooo.cnf | 67050 | 2862719 | |||||
11pipe_11_ooo.cnf | 88289 | 4187694 | |||||
12pipe_12_ooo.cnf | 113768 | 5954744 | |||||
13pipe_13_ooo.cnf | 143311 | 8409838 | |||||
14pipe_14_ooo.cnf | 179056 | 11185426 | |||||
15pipe_15_ooo.cnf | 219755 | 14874914 | |||||
16pipe_16_ooo.cnf | 266498 | 19470237 | |||||
2pipe_2_ooo.cnf | 918 | 8109 | 3034 | 1375 | 21 | 0.06 | UNSAT |
3pipe_3_ooo.cnf | 2533 | 32182 | 28579 | 12474 | 126 | 1.48 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 116431 | 42700 | 369 | 12.63 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 360261 | 127936 | 970 | 79.97 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 961477 | 323022 | 2045 | 418.13 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 2397013 | 816706 | 4349 | 2019.08 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 3959655 | 1005437 | 5592 | 3486.62 | UNSAT |
Total (7 / 15) | 7826450 | 2329650 | 13472 | 6017.97 |
pipe_ooo_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
10pipe_10_ooo_q0_T0.cnf | 81932 | 2080755 | |||||
11pipe_11_ooo_q0_T0.cnf | 110150 | 3003049 | |||||
12pipe_12_ooo_q0_T0.cnf | 144721 | 4206416 | |||||
13pipe_13_ooo_q0_T0.cnf | 185924 | 5911016 | |||||
14pipe_14_ooo_q0_T0.cnf | 236250 | 7676928 | |||||
15pipe_15_ooo_q0_T0.cnf | 294982 | 10067733 | |||||
2pipe_2_ooo_q0_T0.cnf | 895 | 6561 | 3610 | 1574 | 26 | 0.06 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 2566 | 25625 | 25744 | 9750 | 109 | 0.89 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 97905 | 27912 | 253 | 6.08 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 307369 | 76610 | 548 | 33.10 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 709129 | 144271 | 1021 | 106.45 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 1566884 | 290422 | 1978 | 364.59 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 3265062 | 594702 | 3580 | 1253.84 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 3266613 | 522211 | 3069 | 1216.82 | UNSAT |
Total (8 / 14) | 9242316 | 1667452 | 10584 | 2981.83 |
pipe_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 118040 | 8804672 | 1334994 | 208363 | 1403 | 943.37 | SAT |
12pipe_bug10.cnf | 118040 | 8804672 | 1856332 | 284727 | 1917 | 1355.11 | SAT |
12pipe_bug2.cnf | 118040 | 8804630 | 323883 | 40171 | 338 | 193.66 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | 1512672 | 254744 | 1698 | 1271.70 | SAT |
12pipe_bug4.cnf | 117504 | 8743027 | 90204 | 6306 | 67 | 46.87 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | 1340185 | 210297 | 1404 | 972.61 | SAT |
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 16.86 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | 1139397 | 180078 | 1179 | 818.95 | SAT |
12pipe_bug8.cnf | 117526 | 8760516 | 26788 | 71 | 2 | 17.29 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | 131144 | 8871 | 98 | 59.93 | SAT |
Total (10 / 10) | 7761076 | 1193628 | 8106 | 5696.35 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 249453 | 17951 | 173 | 76.90 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | 2872024 | 342855 | 2046 | 1382.10 | SAT |
12pipe_bug2_q0.cnf | 138918 | 4678718 | 229584 | 15581 | 147 | 67.72 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 2711073 | 301642 | 2043 | 1242.91 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 141594 | 10257 | 119 | 47.71 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 358084 | 35050 | 285 | 133.99 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | 349183 | 30088 | 254 | 124.27 | SAT |
12pipe_bug7_q0.cnf | 138918 | 4678760 | 1445972 | 165898 | 1053 | 651.02 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 25957 | 45 | 1 | 9.96 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | 385788 | 35113 | 285 | 138.70 | SAT |
Total (10 / 10) | 8768712 | 954480 | 6406 | 3875.28 |
pipe_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 860 | 6693 | 3162 | 1226 | 20 | 0.05 | UNSAT |
03pipe_k.cnf | 2391 | 27405 | 21355 | 7305 | 81 | 0.68 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 71989 | 20049 | 189 | 4.71 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 184814 | 40081 | 336 | 17.68 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 286905 | 22172 | 218 | 12.30 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 960693 | 176472 | 1149 | 249.27 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 1640538 | 272416 | 1819 | 597.91 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 1683437 | 79744 | 573 | 136.89 | UNSAT |
10pipe_k.cnf | 67300 | 3601247 | 4579337 | 571842 | 3461 | 2485.96 | UNSAT |
11pipe_k.cnf | 89315 | 5584003 | |||||
12pipe_k.cnf | 115915 | 8395649 | |||||
13pipe_k.cnf | 147626 | 12295313 | |||||
14pipe_k.cnf | 184980 | 17597059 | |||||
Total (9 / 13) | 9432230 | 1191307 | 7846 | 3505.45 |
pipe_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 873 | 6457 | 3400 | 1278 | 20 | 0.05 | UNSAT |
03pipe_q0_k.cnf | 2476 | 25181 | 22463 | 8310 | 93 | 0.67 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 73343 | 23372 | 227 | 4.24 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 179605 | 41314 | 348 | 12.61 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 233880 | 22701 | 220 | 10.89 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 879004 | 184299 | 1212 | 167.10 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 1498082 | 213727 | 1441 | 252.03 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1439026 | 76486 | 547 | 110.99 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 4133022 | 521419 | 3069 | 1191.97 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | 6803720 | 789214 | 4131 | 2327.71 | UNSAT |
12pipe_q0_k.cnf | 136800 | 4216460 | 10898164 | 1245298 | 6901 | 4914.88 | UNSAT |
13pipe_q0_k.cnf | 176066 | 5761591 | |||||
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (11 / 14) | 26163709 | 3127418 | 18209 | 8993.14 |
vliw_sat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 236038 | 8084666 | 7973171 | 611655 | 3707 | 2527.13 | SAT |
9dlx_vliw_at_b_iq6_bug2.cnf | 235928 | 8076545 | 120670 | 57 | 1 | 17.16 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 235402 | 8060882 | 8409189 | 500402 | 3068 | 1993.37 | SAT |
9dlx_vliw_at_b_iq6_bug4.cnf | 235277 | 8063780 | 4733785 | 154122 | 1022 | 528.82 | SAT |
9dlx_vliw_at_b_iq6_bug5.cnf | 235923 | 8076534 | 10155579 | 782137 | 4094 | 3181.85 | SAT |
9dlx_vliw_at_b_iq6_bug6.cnf | 235926 | 8076539 | 1313158 | 2323 | 30 | 50.70 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 4931064 | 326550 | 2045 | 982.04 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 4489690 | 192235 | 1276 | 632.38 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | 5436077 | 373673 | 2173 | 1279.02 | SAT |
Total (9 / 9) | 47562383 | 2943154 | 17416 | 11192.47 |
vliw_sat_2.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq8_bug1.cnf | 410707 | 15613033 | 10884386 | 544762 | 3259 | 2939.03 | SAT |
9dlx_vliw_at_b_iq8_bug10.cnf | 408558 | 15554750 | |||||
9dlx_vliw_at_b_iq8_bug2.cnf | 409731 | 15576332 | 6460668 | 147275 | 1021 | 818.68 | SAT |
9dlx_vliw_at_b_iq8_bug3.cnf | 410219 | 15596614 | |||||
9dlx_vliw_at_b_iq8_bug4.cnf | 409220 | 15574959 | 12840856 | 695902 | 4093 | 3962.35 | SAT |
9dlx_vliw_at_b_iq8_bug5.cnf | 410693 | 15615653 | |||||
9dlx_vliw_at_b_iq8_bug6.cnf | 410553 | 15598521 | |||||
9dlx_vliw_at_b_iq8_bug7.cnf | 410729 | 15606974 | 2572151 | 8731 | 94 | 153.79 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | 8553938 | 324897 | 2045 | 1691.11 | SAT |
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | |||||
Total (5 / 10) | 41311999 | 1721567 | 10512 | 9564.96 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 6064544 | 22613 | 220 | 236.31 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 4681271 | 10683 | 123 | 150.14 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 6274425 | 11959 | 125 | 174.57 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 3327664 | 2781 | 36 | 76.90 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 5710694 | 16378 | 156 | 187.37 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 4620905 | 7980 | 92 | 133.09 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 5449328 | 13250 | 126 | 160.90 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 4070162 | 8026 | 92 | 120.43 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 4564989 | 10454 | 122 | 151.55 | SAT |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 3547174 | 5713 | 62 | 97.72 | SAT |
Total (10 / 10) | 48311156 | 109837 | 1154 | 1488.98 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 2147687 | 515687 | 3069 | 561.61 | UNSAT |
9dlx_vliw_at_b_iq2.cnf | 44095 | 542253 | 6028822 | 1287637 | 7163 | 3313.43 | UNSAT |
9dlx_vliw_at_b_iq3.cnf | 69789 | 968295 | |||||
9dlx_vliw_at_b_iq4.cnf | 106013 | 1598301 | |||||
9dlx_vliw_at_b_iq5.cnf | 151669 | 2465731 | |||||
9dlx_vliw_at_b_iq6.cnf | 209724 | 3634677 | |||||
9dlx_vliw_at_b_iq7.cnf | 306095 | 6069108 | |||||
9dlx_vliw_at_b_iq8.cnf | 371419 | 7170909 | |||||
9dlx_vliw_at_b_iq9.cnf | 482093 | 9676386 | |||||
Total (2 / 9) | 8176509 | 1803324 | 10232 | 3875.04 |
vliw_unsat_3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq8_I3_C24.cnf | 132413 | 1435600 | 42315623 | 1657915 | 8190 | 6117.27 | UNSAT |
9dlx_vliw_at_b_iq8_I3_C24_D.cnf | 132156 | 1434887 | 41435397 | 1446929 | 8185 | 5290.40 | UNSAT |
Total (2 / 2) | 83751020 | 3104844 | 16375 | 11407.67 |
vliw_unsat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_C1.cnf | 96177 | 1814189 | 5436913 | 577630 | 3517 | 1152.52 | UNSAT |
9vliw_m_9stages_iq1_C1.cnf | 154309 | 3230738 | |||||
9vliw_m_9stages_iq2_C1.cnf | 230662 | 5267084 | |||||
9vliw_m_9stages_iq3_C1.cnf | 333336 | 8122058 | |||||
Total (1 / 4) | 5436913 | 577630 | 3517 | 1152.52 |