Tinisat, using restart policy (Luby's, unit=256)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 177 (69 SAT + 108 UNSAT)
Time: 668358 seconds / 185.65 hours / 7.74 days
Time on solved instances: 135558 seconds (47015 SAT + 88542 UNSAT)
Instances solved in 10 minutes: 120 (12835 seconds)
Instances solved in 15 minutes: 132 (21575 seconds)
Instances solved in 20 minutes: 140 (30168 seconds)
Instances solved in 30 minutes: 153 (49014 seconds)
Instances solved in 60 minutes: 168 (90463 seconds)
Instances solved in 90 minutes: 174 (117223 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 32 | / | 32 | 59423.57 | ||
engine_unsat_1.0 | 7 | / | 10 | 1763.11 | ||
fvp-sat.3.0 | 14 | / | 20 | 1607.01 | ||
fvp-unsat.1.0 | 4 | / | 4 | 39.22 | ||
fvp-unsat.2.0 | 22 | / | 22 | 749.48 | ||
fvp-unsat.3.0 | 0 | / | 6 | 0 | ||
liveness_sat_1.0 | 7 | / | 10 | 8866.62 | ||
liveness_unsat_1.0 | 4 | / | 12 | 1209.91 | ||
liveness_unsat_2.0 | 3 | / | 9 | 69.46 | ||
npe-1.0 | 3 | / | 6 | 129.22 | ||
pipe_ooo_unsat_1.0 | 7 | / | 15 | 5612.71 | ||
pipe_ooo_unsat_1.1 | 8 | / | 14 | 3266.91 | ||
pipe_sat_1.0 | 10 | / | 10 | 5137.81 | ||
pipe_sat_1.1 | 10 | / | 10 | 3098.81 | ||
pipe_unsat_1.0 | 8 | / | 13 | 1406.52 | ||
pipe_unsat_1.1 | 11 | / | 14 | 9926.54 | ||
vliw_sat_2.0 | 8 | / | 9 | 5088.46 | ||
vliw_sat_2.1 | 5 | / | 10 | 16188.91 | ||
vliw_sat_4.0 | 10 | / | 10 | 1333.31 | ||
vliw_unsat_2.0 | 2 | / | 9 | 3594.27 | ||
vliw_unsat_3.0 | 1 | / | 2 | 5992.52 | ||
vliw_unsat_4.0 | 1 | / | 4 | 1053.29 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 5972718 | 186982 | 227 | 851.98 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 6189263 | 193078 | 238 | 945.10 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 6390931 | 208222 | 252 | 1016.64 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 7177003 | 207670 | 252 | 1116.72 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 7514869 | 196842 | 246 | 1148.27 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 8484816 | 231960 | 254 | 1316.71 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 8764625 | 231606 | 254 | 1414.29 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 10142161 | 254470 | 254 | 1600.00 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 10226340 | 258731 | 254 | 1675.46 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 10987307 | 283242 | 288 | 1905.87 | UNSAT |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2475902 | 129529 | 156 | 324.52 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 12128435 | 283982 | 290 | 2077.07 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 12953392 | 295845 | 313 | 2215.50 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | 12604958 | 334609 | 355 | 3336.09 | UNSAT |
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 15125350 | 327647 | 347 | 2678.16 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 15913104 | 348646 | 379 | 2882.94 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 18125698 | 363675 | 381 | 3210.91 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | 17623434 | 337529 | 362 | 3171.18 | UNSAT |
1dlx_c_iq59_a.cnf | 623700 | 9457051 | 18805837 | 349274 | 379 | 3476.52 | UNSAT |
1dlx_c_iq60_a.cnf | 651875 | 9927770 | 20761550 | 355668 | 380 | 3583.66 | UNSAT |
1dlx_c_iq61_a.cnf | 673311 | 10435991 | 15350967 | 308017 | 317 | 3028.98 | SAT |
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 2847064 | 117411 | 133 | 350.13 | UNSAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | 22313062 | 398714 | 417 | 4364.76 | UNSAT |
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 11275111 | 245088 | 254 | 2549.02 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | 25906264 | 404985 | 427 | 4854.78 | UNSAT |
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 2909498 | 130023 | 156 | 386.32 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 3357331 | 146984 | 182 | 607.89 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 3867464 | 162835 | 189 | 708.18 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 4109659 | 149020 | 186 | 549.23 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 4322127 | 169842 | 203 | 639.49 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 4567248 | 169188 | 203 | 675.80 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 5132181 | 180652 | 220 | 761.40 | UNSAT |
Total (32 / 32) | 334325669 | 7961966 | 8748 | 59423.57 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_4.cnf | 6944 | 66654 | 45661 | 28623 | 45 | 9.82 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 140106 | 100746 | 126 | 65.63 | UNSAT |
engine_5.cnf | 18788 | 214095 | 685138 | 510347 | 509 | 1224.13 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 18218 | 11673 | 23 | 6.56 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 54832 | 38263 | 61 | 25.62 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 65823 | 46028 | 62 | 54.01 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | |||||
engine_6_nd_case1.cnf | 45435 | 610120 | 266098 | 201130 | 251 | 377.34 | UNSAT |
Total (7 / 10) | 1275876 | 936810 | 1077 | 1763.11 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | 3659795 | 281591 | 285 | 208.99 | SAT |
pipe_64_4_bug02.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug03.cnf | 35947 | 992674 | 214349 | 2155 | 6 | 4.55 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 219824 | 1988 | 5 | 5.08 | SAT |
pipe_64_4_bug05.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug06.cnf | 35853 | 1012271 | 3132504 | 221622 | 253 | 164.61 | SAT |
pipe_64_4_bug07.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug08.cnf | 35622 | 1003074 | 471745 | 11739 | 23 | 10.26 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 885139 | 62394 | 90 | 33.58 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 957234 | 59946 | 84 | 32.37 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | 719970 | 39834 | 61 | 22.89 | SAT |
pipe_64_4_bug12.cnf | 35854 | 1012275 | 562563 | 26579 | 44 | 17.83 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 1202055 | 91408 | 125 | 49.36 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 4891027 | 543712 | 510 | 552.55 | SAT |
pipe_64_4_bug15.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug16.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug17.cnf | 35853 | 1012271 | 3850133 | 370967 | 381 | 318.53 | SAT |
pipe_64_4_bug18.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug19.cnf | 35852 | 1012266 | 878422 | 51456 | 69 | 28.66 | SAT |
pipe_64_4_bug20.cnf | 35853 | 1012271 | 2826946 | 227283 | 253 | 157.75 | SAT |
Total (14 / 20) | 24471706 | 1992674 | 2189 | 1607.01 |
fvp-unsat.1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_mc_ex_bp_f.cnf | 776 | 3725 | 2276 | 675 | 2 | 0.02 | UNSAT |
2dlx_ca_mc_ex_bp_f.cnf | 3250 | 24640 | 20034 | 4739 | 12 | 0.41 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 32354 | 8427 | 15 | 0.93 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 472894 | 88286 | 124 | 37.86 | UNSAT |
Total (4 / 4) | 527558 | 102127 | 153 | 39.22 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 3105 | 1090 | 3 | 0.04 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 3458 | 1645 | 5 | 0.07 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 3217 | 1421 | 4 | 0.07 | UNSAT |
3pipe.cnf | 2468 | 27533 | 21210 | 7475 | 14 | 0.66 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 14556 | 6602 | 14 | 0.57 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 20171 | 9898 | 20 | 1.04 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 28536 | 12497 | 25 | 1.50 | UNSAT |
4pipe.cnf | 5237 | 80213 | 76321 | 24753 | 41 | 5.41 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 55540 | 22749 | 37 | 4.75 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 55624 | 20056 | 30 | 4.51 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 99173 | 42577 | 62 | 12.46 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 86588 | 30189 | 50 | 7.95 | UNSAT |
5pipe.cnf | 9471 | 195452 | 118948 | 15332 | 29 | 4.67 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 109470 | 37881 | 61 | 15.57 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 112900 | 36740 | 60 | 16.02 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 118790 | 36392 | 60 | 16.32 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 300301 | 102209 | 126 | 63.51 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 131994 | 34753 | 59 | 17.34 | UNSAT |
6pipe.cnf | 15800 | 394739 | 648435 | 209060 | 252 | 225.29 | UNSAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 374073 | 97612 | 125 | 91.56 | UNSAT |
7pipe.cnf | 23910 | 751118 | 857586 | 178788 | 219 | 217.80 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 388083 | 62812 | 91 | 42.37 | SAT |
Total (22 / 22) | 3628079 | 992531 | 1387 | 749.48 |
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_bug5_liveness.cnf | 292249 | 4906188 | 648887 | 128780 | 155 | 659.12 | SAT |
2dlx_cc_ex_bp_f_bug6_liveness.cnf | 331848 | 5706594 | 653097 | 94376 | 125 | 597.18 | SAT |
2dlx_cc_ex_bp_f_bug7_liveness.cnf | 375775 | 6617342 | |||||
2dlx_cc_ex_bp_f_bug8_liveness.cnf | 424320 | 7649214 | 3303152 | 783491 | 750 | 6750.85 | SAT |
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 | 114683 | 13117 | 27 | 57.02 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 125073 | 14586 | 29 | 73.14 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 344967 | 53214 | 72 | 247.82 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 533243 | 97200 | 125 | 481.49 | SAT |
Total (7 / 10) | 5723102 | 1184764 | 1283 | 8866.62 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 142432 | 72824 | 101 | 41.54 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 770535 | 436699 | 466 | 1126.50 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 120763 | 56543 | 77 | 38.30 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 33788 | 16165 | 29 | 3.57 | 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) | 1067518 | 582231 | 673 | 1209.91 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 48511 | 19319 | 30 | 4.43 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 152449 | 66660 | 93 | 38.14 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 105081 | 47713 | 62 | 26.89 | 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) | 306041 | 133692 | 185 | 69.46 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 5300 | 2292 | 6 | 0.28 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 140869 | 97059 | 125 | 55.19 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 187495 | 39104 | 61 | 73.75 | 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) | 333664 | 138455 | 192 | 129.22 |
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 | 2905 | 1246 | 3 | 0.06 | UNSAT |
3pipe_3_ooo.cnf | 2533 | 32182 | 27142 | 12791 | 26 | 1.44 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 113134 | 51504 | 69 | 15.78 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 357100 | 141334 | 172 | 86.90 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 902369 | 320078 | 335 | 379.53 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 1958032 | 646178 | 588 | 1254.59 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 3866119 | 1102960 | 1020 | 3874.41 | UNSAT |
Total (7 / 15) | 7226801 | 2276091 | 2213 | 5612.71 |
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 | 3439 | 1482 | 4 | 0.06 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 2566 | 25625 | 25119 | 10888 | 21 | 1.00 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 109872 | 41621 | 62 | 9.63 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 274895 | 70592 | 96 | 28.71 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 756270 | 197314 | 248 | 161.03 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 1473568 | 318770 | 332 | 400.85 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 3046996 | 621385 | 563 | 1293.64 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 3047135 | 580872 | 510 | 1371.99 | UNSAT |
Total (8 / 14) | 8737294 | 1842924 | 1836 | 3266.91 |
pipe_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 118040 | 8804672 | 274028 | 41450 | 62 | 151.14 | SAT |
12pipe_bug10.cnf | 118040 | 8804672 | 1737879 | 361177 | 381 | 1510.45 | SAT |
12pipe_bug2.cnf | 118040 | 8804630 | 98687 | 9527 | 19 | 48.55 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | 1424591 | 279138 | 285 | 1049.96 | SAT |
12pipe_bug4.cnf | 117504 | 8743027 | 102327 | 8503 | 16 | 45.85 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | 137985 | 16394 | 30 | 69.21 | SAT |
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 16.61 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | 965770 | 194422 | 241 | 731.57 | SAT |
12pipe_bug8.cnf | 117526 | 8760516 | 72435 | 713 | 2 | 21.96 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | 1548372 | 330039 | 348 | 1492.51 | SAT |
Total (10 / 10) | 6367551 | 1241363 | 1384 | 5137.81 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 160205 | 10495 | 21 | 41.55 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | 2254643 | 342461 | 370 | 1136.29 | SAT |
12pipe_bug2_q0.cnf | 138918 | 4678718 | 127302 | 6562 | 14 | 29.59 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 342329 | 36962 | 61 | 123.39 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 324307 | 33064 | 57 | 118.73 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 689361 | 76397 | 108 | 264.32 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | 286769 | 29013 | 47 | 95.82 | SAT |
12pipe_bug7_q0.cnf | 138918 | 4678760 | 1303783 | 188686 | 232 | 590.05 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 60604 | 267 | 1 | 11.20 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | 1598914 | 219518 | 253 | 687.87 | SAT |
Total (10 / 10) | 7148217 | 943425 | 1164 | 3098.81 |
pipe_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 860 | 6693 | 3803 | 1464 | 4 | 0.06 | UNSAT |
03pipe_k.cnf | 2391 | 27405 | 20395 | 7196 | 14 | 0.61 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 66978 | 20989 | 32 | 4.17 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 212982 | 67436 | 93 | 32.00 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 245062 | 25944 | 44 | 12.64 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 924423 | 228631 | 253 | 348.09 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 1791406 | 372518 | 381 | 857.73 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 1513533 | 100093 | 126 | 151.22 | 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) | 4778582 | 824271 | 947 | 1406.52 |
pipe_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 873 | 6457 | 2915 | 1242 | 3 | 0.04 | UNSAT |
03pipe_q0_k.cnf | 2476 | 25181 | 21073 | 7992 | 14 | 0.58 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 76284 | 27992 | 45 | 5.19 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 187656 | 47089 | 62 | 14.04 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 230087 | 28017 | 45 | 12.30 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 814732 | 181989 | 220 | 150.97 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 1542475 | 316445 | 331 | 392.02 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1364306 | 92060 | 125 | 119.64 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 4390328 | 764009 | 722 | 1754.86 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | 6288942 | 819680 | 765 | 2210.03 | UNSAT |
12pipe_q0_k.cnf | 136800 | 4216460 | 9607685 | 1401327 | 1148 | 5266.87 | UNSAT |
13pipe_q0_k.cnf | 176066 | 5761591 | |||||
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (11 / 14) | 24526483 | 3687842 | 3480 | 9926.54 |
vliw_sat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 236038 | 8084666 | |||||
9dlx_vliw_at_b_iq6_bug2.cnf | 235928 | 8076545 | 120421 | 59 | 0 | 17.14 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 235402 | 8060882 | 7514487 | 469850 | 507 | 1448.11 | SAT |
9dlx_vliw_at_b_iq6_bug4.cnf | 235277 | 8063780 | 5229283 | 248168 | 254 | 674.22 | SAT |
9dlx_vliw_at_b_iq6_bug5.cnf | 235923 | 8076534 | 6187111 | 307420 | 317 | 884.91 | SAT |
9dlx_vliw_at_b_iq6_bug6.cnf | 235926 | 8076539 | 1356857 | 12166 | 24 | 67.08 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 3542938 | 157384 | 189 | 352.47 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 2574456 | 43940 | 62 | 154.43 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | 7505226 | 481235 | 508 | 1490.10 | SAT |
Total (8 / 9) | 34030779 | 1720222 | 1861 | 5088.46 |
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 | 10417771 | 507509 | 509 | 2127.79 | SAT |
9dlx_vliw_at_b_iq8_bug2.cnf | 409731 | 15576332 | 15232251 | 846331 | 765 | 3917.31 | SAT |
9dlx_vliw_at_b_iq8_bug3.cnf | 410219 | 15596614 | 15344761 | 946771 | 891 | 4482.21 | SAT |
9dlx_vliw_at_b_iq8_bug4.cnf | 409220 | 15574959 | 18771931 | 1112815 | 1020 | 5590.80 | 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 | 976033 | 1438 | 4 | 70.80 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | |||||
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | |||||
Total (5 / 10) | 60742747 | 3414864 | 3189 | 16188.91 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 6449351 | 15996 | 29 | 168.88 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 5740700 | 12029 | 24 | 144.76 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 6624938 | 8317 | 15 | 115.00 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 4248379 | 2487 | 6 | 71.06 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 6133256 | 27767 | 45 | 208.49 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 4083117 | 4179 | 10 | 82.98 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 5229590 | 6389 | 14 | 101.10 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 6211489 | 10916 | 21 | 134.21 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 5644103 | 15376 | 29 | 156.65 | SAT |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 5551719 | 15440 | 29 | 150.18 | SAT |
Total (10 / 10) | 55916642 | 118896 | 222 | 1333.31 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 2283041 | 593628 | 520 | 599.21 | UNSAT |
9dlx_vliw_at_b_iq2.cnf | 44095 | 542253 | 5872068 | 1413375 | 1149 | 2995.06 | 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) | 8155109 | 2007003 | 1669 | 3594.27 |
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 | 38074205 | 1890571 | 1533 | 5992.52 | UNSAT |
Total (1 / 2) | 38074205 | 1890571 | 1533 | 5992.52 |
vliw_unsat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_C1.cnf | 96177 | 1814189 | 5384336 | 648764 | 594 | 1053.29 | 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) | 5384336 | 648764 | 594 | 1053.29 |