Tinisat, using Siege restart policy (16000, 1)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 178 (72 SAT + 106 UNSAT)
Time: 673787 seconds / 187.16 hours / 7.80 days
Time on solved instances: 148187 seconds (56181 SAT + 92006 UNSAT)
Instances solved in 10 minutes: 118 (11435 seconds)
Instances solved in 15 minutes: 125 (16765 seconds)
Instances solved in 20 minutes: 136 (28366 seconds)
Instances solved in 30 minutes: 148 (45292 seconds)
Instances solved in 60 minutes: 167 (95788 seconds)
Instances solved in 90 minutes: 177 (140963 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 32 | / | 32 | 68009.87 | ||
engine_unsat_1.0 | 7 | / | 10 | 1499.93 | ||
fvp-sat.3.0 | 17 | / | 20 | 11786.93 | ||
fvp-unsat.1.0 | 4 | / | 4 | 66.61 | ||
fvp-unsat.2.0 | 22 | / | 22 | 883.75 | ||
fvp-unsat.3.0 | 1 | / | 6 | 79.73 | ||
liveness_sat_1.0 | 4 | / | 10 | 1694.95 | ||
liveness_unsat_1.0 | 4 | / | 12 | 1349.67 | ||
liveness_unsat_2.0 | 3 | / | 9 | 74.96 | ||
npe-1.0 | 4 | / | 6 | 4057.05 | ||
pipe_ooo_unsat_1.0 | 7 | / | 15 | 4840.45 | ||
pipe_ooo_unsat_1.1 | 8 | / | 14 | 3189.11 | ||
pipe_sat_1.0 | 9 | / | 10 | 939.01 | ||
pipe_sat_1.1 | 10 | / | 10 | 8056.37 | ||
pipe_unsat_1.0 | 8 | / | 13 | 1712.08 | ||
pipe_unsat_1.1 | 10 | / | 14 | 9130.27 | ||
vliw_sat_2.0 | 9 | / | 9 | 7534.2 | ||
vliw_sat_2.1 | 6 | / | 10 | 14114.89 | ||
vliw_sat_4.0 | 10 | / | 10 | 2028.97 | ||
vliw_unsat_2.0 | 2 | / | 9 | 6306.46 | ||
vliw_unsat_3.0 | 0 | / | 2 | 0 | ||
vliw_unsat_4.0 | 1 | / | 4 | 831.88 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2819579 | 212849 | 13 | 508.26 | UNSAT |
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 2991577 | 184013 | 11 | 462.84 | UNSAT |
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 3048864 | 158818 | 9 | 444.58 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 4206580 | 239402 | 14 | 834.91 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 4050775 | 242312 | 15 | 873.07 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 4213382 | 208866 | 13 | 645.65 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 5840566 | 292760 | 18 | 1007.02 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 5562390 | 267251 | 16 | 950.19 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 5903459 | 263202 | 16 | 972.71 | UNSAT |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 6320468 | 252584 | 15 | 985.81 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 6136506 | 275472 | 17 | 1159.63 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 7474997 | 312759 | 19 | 1400.24 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 8338313 | 286248 | 17 | 1339.70 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 8169125 | 315587 | 19 | 1559.88 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 8392181 | 277238 | 17 | 1412.58 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 10267009 | 317955 | 19 | 1765.02 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 10203738 | 276714 | 17 | 1629.76 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 11735640 | 358758 | 22 | 2059.18 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 12066541 | 365169 | 22 | 2213.07 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 13089232 | 407841 | 25 | 2533.64 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 14254724 | 356004 | 22 | 2424.52 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | 14440676 | 454343 | 28 | 4062.27 | UNSAT |
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 15214245 | 374096 | 23 | 2663.89 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 16361927 | 435049 | 27 | 3169.76 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 16924568 | 408944 | 25 | 3268.18 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | 18782646 | 450878 | 28 | 3629.50 | UNSAT |
1dlx_c_iq59_a.cnf | 623700 | 9457051 | 19500677 | 424694 | 26 | 3808.87 | UNSAT |
1dlx_c_iq60_a.cnf | 651875 | 9927770 | 22402582 | 508584 | 31 | 4530.82 | UNSAT |
1dlx_c_iq61_a.cnf | 673311 | 10435991 | 13179344 | 311296 | 19 | 2765.12 | SAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | 24159685 | 469788 | 29 | 4633.90 | UNSAT |
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 15034171 | 323791 | 20 | 3115.46 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | 27686996 | 482509 | 30 | 5179.84 | UNSAT |
Total (32 / 32) | 358773163 | 10515774 | 642 | 68009.87 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_6_nd_case1.cnf | 45435 | 610120 | 237986 | 184262 | 11 | 307.64 | UNSAT |
engine_4.cnf | 6944 | 66654 | 40947 | 26266 | 1 | 8.17 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 126011 | 95359 | 5 | 55.00 | UNSAT |
engine_5.cnf | 18788 | 214095 | 612092 | 478327 | 29 | 1043.38 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 17902 | 11593 | 0 | 5.98 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 54505 | 39110 | 2 | 25.51 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 63830 | 45757 | 2 | 54.25 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | |||||
Total (7 / 10) | 1153273 | 880674 | 50 | 1499.93 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | 94238 | 4981 | 0 | 3.24 | SAT |
pipe_64_4_bug02.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug03.cnf | 35947 | 992674 | 178537 | 32079 | 2 | 12.30 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 97771 | 16072 | 1 | 6.93 | SAT |
pipe_64_4_bug05.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug06.cnf | 35853 | 1012271 | 687679 | 125235 | 7 | 51.33 | SAT |
pipe_64_4_bug07.cnf | 35853 | 1012271 | 13651646 | 1725016 | 107 | 3160.82 | SAT |
pipe_64_4_bug08.cnf | 35622 | 1003074 | 413401 | 67453 | 4 | 27.18 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 628294 | 107759 | 6 | 48.32 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 435810 | 63676 | 3 | 26.27 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | 2561925 | 408167 | 25 | 252.80 | SAT |
pipe_64_4_bug12.cnf | 35854 | 1012275 | 269087 | 54063 | 3 | 20.03 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 472928 | 104684 | 6 | 40.81 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 1093103 | 193646 | 12 | 91.74 | SAT |
pipe_64_4_bug15.cnf | 35853 | 1012271 | 793816 | 138092 | 8 | 60.34 | SAT |
pipe_64_4_bug16.cnf | 35853 | 1012271 | 2697522 | 424696 | 26 | 307.04 | SAT |
pipe_64_4_bug17.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug18.cnf | 35853 | 1012271 | 1172276 | 195354 | 12 | 95.28 | SAT |
pipe_64_4_bug19.cnf | 35852 | 1012266 | 17864630 | 2639824 | 164 | 7224.07 | SAT |
pipe_64_4_bug20.cnf | 35853 | 1012271 | 3164553 | 476104 | 29 | 358.43 | SAT |
Total (17 / 20) | 46277216 | 6776901 | 415 | 11786.93 |
fvp-unsat.1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_mc_ex_bp_f.cnf | 776 | 3725 | 2284 | 670 | 0 | 0.02 | UNSAT |
2dlx_ca_mc_ex_bp_f.cnf | 3250 | 24640 | 22149 | 4918 | 0 | 0.44 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 31454 | 8668 | 0 | 1.08 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 580516 | 142746 | 8 | 65.07 | UNSAT |
Total (4 / 4) | 636403 | 157002 | 8 | 66.61 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 3014 | 1170 | 0 | 0.05 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 2509 | 1089 | 0 | 0.05 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 2895 | 1371 | 0 | 0.06 | UNSAT |
3pipe.cnf | 2468 | 27533 | 19265 | 6566 | 0 | 0.54 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 11702 | 5455 | 0 | 0.44 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 16688 | 7435 | 0 | 0.70 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 22712 | 10182 | 0 | 1.10 | UNSAT |
4pipe.cnf | 5237 | 80213 | 85556 | 27322 | 1 | 6.40 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 45173 | 18670 | 1 | 3.82 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 68431 | 29764 | 1 | 7.57 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 73873 | 28184 | 1 | 7.03 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 101874 | 46330 | 2 | 14.97 | UNSAT |
5pipe.cnf | 9471 | 195452 | 107927 | 19119 | 1 | 6.17 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 115663 | 44129 | 2 | 22.54 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 143403 | 53312 | 3 | 32.64 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 125051 | 35070 | 2 | 18.08 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 323425 | 129636 | 8 | 92.15 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 143339 | 44432 | 2 | 26.09 | UNSAT |
6pipe.cnf | 15800 | 394739 | 571716 | 169475 | 10 | 154.76 | UNSAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 466916 | 130980 | 8 | 167.69 | UNSAT |
7pipe.cnf | 23910 | 751118 | 967130 | 219323 | 13 | 251.28 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 475078 | 88546 | 5 | 69.62 | SAT |
Total (22 / 22) | 3893340 | 1117560 | 60 | 883.75 |
fvp-unsat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_01.cnf | 40347 | 1224040 | 730788 | 160212 | 10 | 79.73 | SAT |
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 (1 / 6) | 730788 | 160212 | 10 | 79.73 |
liveness_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2dlx_cc_ex_bp_f_bug9_liveness.cnf | 477782 | 8813656 | |||||
2dlx_cc_ex_bp_f_bug10_liveness.cnf | 536469 | 10122798 | |||||
2dlx_cc_ex_bp_f_bug1_liveness.cnf | 171648 | 2614464 | 84951 | 9397 | 0 | 41.51 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 272882 | 48687 | 3 | 188.89 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 272540 | 45002 | 2 | 194.82 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 1093742 | 266048 | 16 | 1269.73 | SAT |
2dlx_cc_ex_bp_f_bug5_liveness.cnf | 292249 | 4906188 | |||||
2dlx_cc_ex_bp_f_bug6_liveness.cnf | 331848 | 5706594 | |||||
2dlx_cc_ex_bp_f_bug7_liveness.cnf | 375775 | 6617342 | |||||
2dlx_cc_ex_bp_f_bug8_liveness.cnf | 424320 | 7649214 | |||||
Total (4 / 10) | 1724115 | 369134 | 21 | 1694.95 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 138127 | 73320 | 4 | 44.32 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 807507 | 486332 | 30 | 1270.88 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 109402 | 50252 | 3 | 31.53 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 31197 | 14405 | 0 | 2.94 | 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) | 1086233 | 624309 | 37 | 1349.67 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 44026 | 18182 | 1 | 4.20 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 145694 | 65425 | 4 | 37.36 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 116497 | 56144 | 3 | 33.40 | 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) | 306217 | 139751 | 8 | 74.96 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 20150 | 11874 | 0 | 2.12 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 157381 | 107970 | 6 | 61.06 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 667085 | 288648 | 18 | 856.69 | SAT |
2dlx_cc_mc_ex_bp_f2_no_pe.cnf | 96675 | 1401773 | |||||
9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf | 889302 | 14582074 | 2995899 | 260973 | 16 | 3137.18 | SAT |
9dlx_vliw_at_bp_mc2_no_pe.cnf | 889302 | 14582081 | |||||
Total (4 / 6) | 3840515 | 669465 | 40 | 4057.05 |
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 | 2570 | 1394 | 0 | 0.06 | UNSAT |
3pipe_3_ooo.cnf | 2533 | 32182 | 21938 | 9308 | 0 | 0.93 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 116812 | 51688 | 3 | 16.05 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 304922 | 115077 | 7 | 63.93 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 1144317 | 485000 | 30 | 684.98 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 1905051 | 680147 | 42 | 1271.43 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 3417152 | 970252 | 60 | 2803.07 | UNSAT |
Total (7 / 15) | 6912762 | 2312866 | 142 | 4840.45 |
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 | 3236 | 1517 | 0 | 0.05 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 2566 | 25625 | 24661 | 9545 | 0 | 0.81 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 83707 | 28557 | 1 | 5.43 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 263808 | 89141 | 5 | 40.04 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 759316 | 227853 | 14 | 197.67 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 1354849 | 316958 | 19 | 407.42 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 3110833 | 661559 | 41 | 1414.02 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 2792196 | 506535 | 31 | 1123.67 | UNSAT |
Total (8 / 14) | 8392606 | 1841665 | 111 | 3189.11 |
pipe_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 118040 | 8804672 | 38089 | 1346 | 0 | 19.27 | SAT |
12pipe_bug10.cnf | 118040 | 8804672 | 110029 | 14965 | 0 | 64.95 | SAT |
12pipe_bug2.cnf | 118040 | 8804630 | 162211 | 17446 | 1 | 65.82 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | 55443 | 4257 | 0 | 23.80 | SAT |
12pipe_bug4.cnf | 117504 | 8743027 | 555543 | 96007 | 6 | 301.10 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | 226810 | 40435 | 2 | 122.00 | SAT |
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 16.18 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | |||||
12pipe_bug8.cnf | 117526 | 8760516 | 629990 | 96012 | 6 | 307.70 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | 35742 | 1114 | 0 | 18.19 | SAT |
Total (9 / 10) | 1819334 | 271582 | 15 | 939.01 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 1306106 | 222012 | 13 | 602.77 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | 2490679 | 416441 | 26 | 1232.97 | SAT |
12pipe_bug2_q0.cnf | 138918 | 4678718 | 88102 | 5195 | 0 | 27.98 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 412343 | 46406 | 2 | 161.36 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 555323 | 97850 | 6 | 304.74 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 130884 | 9539 | 0 | 37.28 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | 526951 | 60670 | 3 | 178.74 | SAT |
12pipe_bug7_q0.cnf | 138918 | 4678760 | 6198452 | 1331309 | 83 | 5348.07 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 171962 | 16083 | 1 | 50.27 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | 253559 | 29810 | 1 | 112.19 | SAT |
Total (10 / 10) | 12134361 | 2235315 | 135 | 8056.37 |
pipe_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 860 | 6693 | 2930 | 1220 | 0 | 0.05 | UNSAT |
03pipe_k.cnf | 2391 | 27405 | 18991 | 7160 | 0 | 0.60 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 85368 | 28165 | 1 | 6.30 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 205115 | 58551 | 3 | 23.28 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 268343 | 35681 | 2 | 20.31 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 1088738 | 267263 | 16 | 354.76 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 1864115 | 482545 | 30 | 1111.09 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 1364064 | 118718 | 7 | 195.69 | UNSAT |
10pipe_k.cnf | 67300 | 3601247 | |||||
11pipe_k.cnf | 89315 | 5584003 | |||||
12pipe_k.cnf | 115915 | 8395649 | |||||
13pipe_k.cnf | 147626 | 12295313 | |||||
14pipe_k.cnf | 184980 | 17597059 | |||||
Total (8 / 13) | 4897664 | 999303 | 59 | 1712.08 |
pipe_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 873 | 6457 | 2794 | 1086 | 0 | 0.04 | UNSAT |
03pipe_q0_k.cnf | 2476 | 25181 | 18978 | 7308 | 0 | 0.54 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 64855 | 22265 | 1 | 3.51 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 203140 | 70204 | 4 | 23.95 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 206820 | 38004 | 2 | 17.53 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 982775 | 278074 | 17 | 259.48 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 2041004 | 598732 | 37 | 1007.55 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1120540 | 116722 | 7 | 146.14 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 4535198 | 1069133 | 66 | 2748.25 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | 6804332 | 1457331 | 91 | 4923.28 | UNSAT |
12pipe_q0_k.cnf | 136800 | 4216460 | |||||
13pipe_q0_k.cnf | 176066 | 5761591 | |||||
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (10 / 14) | 15980436 | 3658859 | 225 | 9130.27 |
vliw_sat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 236038 | 8084666 | 8438018 | 821841 | 51 | 2467.04 | SAT |
9dlx_vliw_at_b_iq6_bug2.cnf | 235928 | 8076545 | 120421 | 59 | 0 | 17.16 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 235402 | 8060882 | 7396090 | 729824 | 45 | 2099.08 | SAT |
9dlx_vliw_at_b_iq6_bug4.cnf | 235277 | 8063780 | 1270442 | 6840 | 0 | 52.30 | SAT |
9dlx_vliw_at_b_iq6_bug5.cnf | 235923 | 8076534 | 4723294 | 428141 | 26 | 1049.41 | SAT |
9dlx_vliw_at_b_iq6_bug6.cnf | 235926 | 8076539 | 1582905 | 53251 | 3 | 123.31 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 2172375 | 165977 | 10 | 312.78 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 2162049 | 99206 | 6 | 222.40 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | 6282700 | 457062 | 28 | 1190.72 | SAT |
Total (9 / 9) | 34148294 | 2762201 | 169 | 7534.2 |
vliw_sat_2.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq8_bug1.cnf | 410707 | 15613033 | |||||
9dlx_vliw_at_b_iq8_bug10.cnf | 408558 | 15554750 | 11101967 | 677873 | 42 | 2642.05 | SAT |
9dlx_vliw_at_b_iq8_bug2.cnf | 409731 | 15576332 | 8309130 | 517616 | 32 | 1987.91 | SAT |
9dlx_vliw_at_b_iq8_bug3.cnf | 410219 | 15596614 | 10182222 | 553842 | 34 | 2097.00 | SAT |
9dlx_vliw_at_b_iq8_bug4.cnf | 409220 | 15574959 | 13750817 | 972925 | 60 | 4111.57 | 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 | 1894723 | 18187 | 1 | 135.53 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | |||||
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | 15423788 | 702206 | 43 | 3140.83 | SAT |
Total (6 / 10) | 60662647 | 3442649 | 212 | 14114.89 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 6871992 | 46122 | 2 | 284.25 | SAT |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 8521585 | 49471 | 3 | 242.00 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 8242265 | 56847 | 3 | 354.18 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 6189255 | 17318 | 1 | 118.74 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 4447142 | 2098 | 0 | 57.75 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 6246054 | 43329 | 2 | 229.49 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 7459833 | 29041 | 1 | 190.47 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 7811661 | 44263 | 2 | 219.33 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 6125501 | 19414 | 1 | 115.87 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 6166611 | 38239 | 2 | 216.89 | SAT |
Total (10 / 10) | 68081899 | 346142 | 17 | 2028.97 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 2974372 | 966459 | 60 | 1359.58 | UNSAT |
9dlx_vliw_at_b_iq2.cnf | 44095 | 542253 | 6829005 | 1946952 | 121 | 4946.88 | 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) | 9803377 | 2913411 | 181 | 6306.46 |
vliw_unsat_3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq8_I3_C24.cnf | 132413 | 1435600 | |||||
9dlx_vliw_at_b_iq8_I3_C24_D.cnf | 132156 | 1434887 | |||||
Total (0 / 2) | 0 |
vliw_unsat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_C1.cnf | 96177 | 1814189 | 4763392 | 617600 | 38 | 831.88 | 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) | 4763392 | 617600 | 38 | 831.88 |