Tinisat, using restart policy (Luby's, unit=64)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 180 (69 SAT + 111 UNSAT)
Time: 662079 seconds / 183.91 hours / 7.66 days
Time on solved instances: 150879 seconds (48847 SAT + 102031 UNSAT)
Instances solved in 10 minutes: 113 (10800 seconds)
Instances solved in 15 minutes: 124 (18771 seconds)
Instances solved in 20 minutes: 137 (32066 seconds)
Instances solved in 30 minutes: 152 (54306 seconds)
Instances solved in 60 minutes: 172 (111330 seconds)
Instances solved in 90 minutes: 177 (132506 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 32 | / | 32 | 60701.87 | ||
engine_unsat_1.0 | 7 | / | 10 | 2310.8 | ||
fvp-sat.3.0 | 15 | / | 20 | 7734.86 | ||
fvp-unsat.1.0 | 4 | / | 4 | 45.69 | ||
fvp-unsat.2.0 | 22 | / | 22 | 628.53 | ||
fvp-unsat.3.0 | 0 | / | 6 | 0 | ||
liveness_sat_1.0 | 6 | / | 10 | 4141.99 | ||
liveness_unsat_1.0 | 4 | / | 12 | 1105.29 | ||
liveness_unsat_2.0 | 3 | / | 9 | 63.52 | ||
npe-1.0 | 4 | / | 6 | 3088.59 | ||
pipe_ooo_unsat_1.0 | 7 | / | 15 | 6108.73 | ||
pipe_ooo_unsat_1.1 | 8 | / | 14 | 2733.26 | ||
pipe_sat_1.0 | 9 | / | 10 | 5450.76 | ||
pipe_sat_1.1 | 10 | / | 10 | 1293.64 | ||
pipe_unsat_1.0 | 9 | / | 13 | 2893.24 | ||
pipe_unsat_1.1 | 11 | / | 14 | 7754.36 | ||
vliw_sat_2.0 | 9 | / | 9 | 9093.65 | ||
vliw_sat_2.1 | 4 | / | 10 | 10711.84 | ||
vliw_sat_4.0 | 10 | / | 10 | 1720.47 | ||
vliw_unsat_2.0 | 3 | / | 9 | 9295.98 | ||
vliw_unsat_3.0 | 2 | / | 2 | 12919.19 | ||
vliw_unsat_4.0 | 1 | / | 4 | 1082.56 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 5392644 | 176834 | 644 | 849.76 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 6369011 | 197704 | 762 | 1003.64 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 6624797 | 185296 | 698 | 1006.67 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 7224254 | 194580 | 742 | 1095.84 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 7862189 | 211446 | 765 | 1242.86 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 8842673 | 205841 | 765 | 1341.07 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 9238870 | 225253 | 828 | 1499.92 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 10418124 | 227440 | 845 | 1611.89 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 10661596 | 249869 | 949 | 1793.81 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 11607934 | 243926 | 910 | 1945.86 | UNSAT |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2451398 | 113079 | 489 | 331.93 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 12550352 | 255101 | 967 | 2069.39 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 13247858 | 277543 | 1020 | 2283.14 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | 13129152 | 307871 | 1022 | 3443.38 | UNSAT |
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 14798371 | 298266 | 1022 | 2693.03 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 17211783 | 318036 | 1022 | 2926.75 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 17846310 | 324236 | 1022 | 3193.88 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | 18795176 | 327582 | 1022 | 3375.91 | UNSAT |
1dlx_c_iq59_a.cnf | 623700 | 9457051 | 19451802 | 344489 | 1116 | 3530.46 | UNSAT |
1dlx_c_iq60_a.cnf | 651875 | 9927770 | 20434525 | 346708 | 1131 | 3865.66 | UNSAT |
1dlx_c_iq61_a.cnf | 673311 | 10435991 | 16813128 | 294908 | 1021 | 3209.37 | SAT |
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 2758754 | 122309 | 508 | 384.70 | UNSAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | 23786272 | 371245 | 1234 | 4404.45 | UNSAT |
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 10292494 | 212208 | 765 | 2395.35 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | 26196093 | 376049 | 1261 | 4832.60 | UNSAT |
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 3126782 | 124178 | 509 | 412.58 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 3053824 | 145032 | 510 | 610.21 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 3810887 | 159462 | 573 | 736.18 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 4077879 | 152365 | 541 | 578.07 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 4221792 | 156388 | 571 | 624.22 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 4871754 | 161401 | 588 | 700.87 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 5017303 | 162213 | 594 | 708.42 | UNSAT |
Total (32 / 32) | 342185781 | 7468858 | 26416 | 60701.87 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_4.cnf | 6944 | 66654 | 49412 | 29423 | 133 | 10.89 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 152406 | 106745 | 447 | 76.46 | UNSAT |
engine_5.cnf | 18788 | 214095 | 820376 | 596104 | 2042 | 1725.94 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 19187 | 11989 | 62 | 7.00 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 56235 | 39045 | 189 | 26.70 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 72827 | 48354 | 238 | 62.14 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | |||||
engine_6_nd_case1.cnf | 45435 | 610120 | 276596 | 206463 | 765 | 401.67 | UNSAT |
Total (7 / 10) | 1447039 | 1038123 | 3876 | 2310.8 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | 780768 | 24527 | 125 | 19.65 | SAT |
pipe_64_4_bug02.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug03.cnf | 35947 | 992674 | 367302 | 1914 | 14 | 4.83 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 533508 | 5721 | 37 | 8.25 | SAT |
pipe_64_4_bug05.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug06.cnf | 35853 | 1012271 | 1896587 | 91097 | 381 | 65.72 | SAT |
pipe_64_4_bug07.cnf | 35853 | 1012271 | 2481449 | 134153 | 510 | 102.69 | SAT |
pipe_64_4_bug08.cnf | 35622 | 1003074 | 3747096 | 287618 | 1021 | 264.71 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 601943 | 14783 | 83 | 12.92 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 689756 | 11977 | 62 | 12.94 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | 6502962 | 503780 | 1660 | 634.70 | SAT |
pipe_64_4_bug12.cnf | 35854 | 1012275 | 1403427 | 76574 | 317 | 48.80 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 7745153 | 635985 | 2045 | 904.07 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 1417737 | 57218 | 253 | 40.23 | SAT |
pipe_64_4_bug15.cnf | 35853 | 1012271 | 12483643 | 1101584 | 3322 | 2128.67 | SAT |
pipe_64_4_bug16.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug17.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug18.cnf | 35853 | 1012271 | 14483331 | 1353399 | 4092 | 3391.87 | SAT |
pipe_64_4_bug19.cnf | 35852 | 1012266 | |||||
pipe_64_4_bug20.cnf | 35853 | 1012271 | 2330263 | 128346 | 509 | 94.81 | SAT |
Total (15 / 20) | 57464925 | 4428676 | 14431 | 7734.86 |
fvp-unsat.1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_mc_ex_bp_f.cnf | 776 | 3725 | 2525 | 775 | 7 | 0.03 | UNSAT |
2dlx_ca_mc_ex_bp_f.cnf | 3250 | 24640 | 21367 | 5693 | 37 | 0.52 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 31177 | 8086 | 55 | 0.95 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 501394 | 97887 | 411 | 44.19 | UNSAT |
Total (4 / 4) | 556463 | 112441 | 510 | 45.69 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 3092 | 1222 | 12 | 0.05 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 2956 | 1289 | 13 | 0.06 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 3290 | 1510 | 13 | 0.07 | UNSAT |
3pipe.cnf | 2468 | 27533 | 23126 | 7921 | 52 | 0.75 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 16431 | 7512 | 50 | 0.70 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 22117 | 9724 | 61 | 1.05 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 24960 | 10580 | 62 | 1.22 | UNSAT |
4pipe.cnf | 5237 | 80213 | 77690 | 24310 | 125 | 5.36 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 62592 | 26274 | 126 | 6.06 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 66805 | 23905 | 125 | 5.58 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 100765 | 38508 | 188 | 11.59 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 110751 | 43143 | 207 | 13.18 | UNSAT |
5pipe.cnf | 9471 | 195452 | 130241 | 15511 | 90 | 5.01 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 106590 | 35610 | 172 | 14.19 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 115811 | 34036 | 160 | 14.61 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 124434 | 34014 | 160 | 15.23 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 234610 | 67525 | 269 | 35.56 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 128445 | 34347 | 164 | 17.34 | UNSAT |
6pipe.cnf | 15800 | 394739 | 480174 | 121794 | 508 | 124.91 | UNSAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 386240 | 89007 | 380 | 82.20 | UNSAT |
7pipe.cnf | 23910 | 751118 | 946288 | 185239 | 698 | 233.54 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 370081 | 52434 | 252 | 40.27 | SAT |
Total (22 / 22) | 3537489 | 865415 | 3887 | 628.53 |
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 | 670939 | 116902 | 507 | 704.67 | SAT |
2dlx_cc_ex_bp_f_bug6_liveness.cnf | 331848 | 5706594 | 1079596 | 184630 | 697 | 1252.02 | SAT |
2dlx_cc_ex_bp_f_bug7_liveness.cnf | 375775 | 6617342 | |||||
2dlx_cc_ex_bp_f_bug8_liveness.cnf | 424320 | 7649214 | |||||
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 | 109446 | 13248 | 72 | 60.09 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 178013 | 22013 | 124 | 105.35 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 1020865 | 193735 | 734 | 993.14 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 971110 | 185645 | 699 | 1026.72 | SAT |
Total (6 / 10) | 4029969 | 716173 | 2833 | 4141.99 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 134280 | 64837 | 254 | 35.58 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 757994 | 409460 | 1370 | 1026.69 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 125296 | 56479 | 253 | 39.72 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 33926 | 14630 | 81 | 3.30 | 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) | 1051496 | 545406 | 1958 | 1105.29 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 45329 | 15586 | 90 | 3.45 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 137945 | 54342 | 253 | 30.00 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 109480 | 48950 | 243 | 30.07 | 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) | 292754 | 118878 | 586 | 63.52 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 3554 | 915 | 9 | 0.14 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 112081 | 74448 | 315 | 33.39 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 69565 | 5493 | 35 | 14.63 | SAT |
2dlx_cc_mc_ex_bp_f2_no_pe.cnf | 96675 | 1401773 | |||||
9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf | 889302 | 14582074 | 2514998 | 198316 | 762 | 3040.43 | SAT |
9dlx_vliw_at_bp_mc2_no_pe.cnf | 889302 | 14582081 | |||||
Total (4 / 6) | 2700198 | 279172 | 1121 | 3088.59 |
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 | 3117 | 1451 | 13 | 0.06 | UNSAT |
3pipe_3_ooo.cnf | 2533 | 32182 | 24794 | 10462 | 62 | 1.12 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 112923 | 44511 | 218 | 12.91 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 368931 | 140473 | 510 | 94.71 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 1035634 | 387269 | 1277 | 529.99 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 2269721 | 756381 | 2219 | 1721.41 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 4015141 | 1073376 | 3196 | 3748.53 | UNSAT |
Total (7 / 15) | 7830261 | 2413923 | 7495 | 6108.73 |
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 | 3397 | 1527 | 13 | 0.06 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 2566 | 25625 | 24429 | 9411 | 61 | 0.88 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 119592 | 40342 | 189 | 9.64 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 264165 | 63385 | 254 | 25.43 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 699270 | 140873 | 510 | 102.90 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 1533371 | 295584 | 1022 | 371.63 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 3266296 | 614594 | 2044 | 1299.71 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 2919471 | 429489 | 1456 | 923.01 | UNSAT |
Total (8 / 14) | 8829991 | 1595205 | 5549 | 2733.26 |
pipe_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 118040 | 8804672 | 1405483 | 256061 | 971 | 1126.96 | SAT |
12pipe_bug10.cnf | 118040 | 8804672 | 697422 | 105682 | 444 | 441.41 | SAT |
12pipe_bug2.cnf | 118040 | 8804630 | 500566 | 79981 | 334 | 340.51 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | 1533458 | 272042 | 1020 | 1253.58 | SAT |
12pipe_bug4.cnf | 117504 | 8743027 | 253460 | 33855 | 158 | 144.99 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | 1280026 | 214739 | 780 | 881.90 | SAT |
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 16.19 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | |||||
12pipe_bug8.cnf | 117526 | 8760516 | 39314 | 128 | 2 | 17.63 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | 1573382 | 280805 | 1021 | 1227.59 | SAT |
Total (9 / 10) | 7288588 | 1243293 | 4730 | 5450.76 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 1029340 | 108605 | 460 | 414.37 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | 126445 | 5063 | 30 | 27.70 | SAT |
12pipe_bug2_q0.cnf | 138918 | 4678718 | 176532 | 10301 | 62 | 43.13 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 241025 | 17852 | 99 | 69.02 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 56387 | 3358 | 28 | 20.41 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 586191 | 56773 | 253 | 210.75 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | 158948 | 13488 | 75 | 52.70 | SAT |
12pipe_bug7_q0.cnf | 138918 | 4678760 | 487871 | 46113 | 221 | 172.12 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 60342 | 95 | 1 | 10.17 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | 693502 | 73544 | 309 | 273.27 | SAT |
Total (10 / 10) | 3616583 | 335192 | 1538 | 1293.64 |
pipe_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 860 | 6693 | 2876 | 1347 | 13 | 0.05 | UNSAT |
03pipe_k.cnf | 2391 | 27405 | 19459 | 5944 | 38 | 0.52 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 81213 | 23600 | 125 | 5.70 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 213834 | 52239 | 252 | 24.32 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 272520 | 22348 | 124 | 12.24 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 1094238 | 241975 | 896 | 412.35 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 1794736 | 330148 | 1043 | 789.88 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 1576206 | 77252 | 317 | 124.32 | UNSAT |
10pipe_k.cnf | 67300 | 3601247 | 4224516 | 459704 | 1533 | 1523.86 | UNSAT |
11pipe_k.cnf | 89315 | 5584003 | |||||
12pipe_k.cnf | 115915 | 8395649 | |||||
13pipe_k.cnf | 147626 | 12295313 | |||||
14pipe_k.cnf | 184980 | 17597059 | |||||
Total (9 / 13) | 9279598 | 1214557 | 4341 | 2893.24 |
pipe_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 873 | 6457 | 3044 | 1314 | 13 | 0.05 | UNSAT |
03pipe_q0_k.cnf | 2476 | 25181 | 21232 | 7973 | 53 | 0.61 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 82436 | 27468 | 126 | 5.22 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 196584 | 59078 | 254 | 20.46 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 244686 | 22295 | 124 | 10.54 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 805513 | 155039 | 562 | 127.87 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 1502900 | 282913 | 1021 | 350.28 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1390659 | 78415 | 324 | 109.67 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 4073702 | 472209 | 1533 | 973.40 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | 6684135 | 925604 | 2811 | 2670.43 | UNSAT |
12pipe_q0_k.cnf | 136800 | 4216460 | 9858690 | 1013608 | 3068 | 3485.83 | UNSAT |
13pipe_q0_k.cnf | 176066 | 5761591 | |||||
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (11 / 14) | 24863581 | 3045916 | 9889 | 7754.36 |
vliw_sat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 236038 | 8084666 | 7332337 | 452399 | 1532 | 1544.49 | SAT |
9dlx_vliw_at_b_iq6_bug2.cnf | 235928 | 8076545 | 120421 | 59 | 0 | 17.41 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 235402 | 8060882 | 7861215 | 456326 | 1532 | 1552.39 | SAT |
9dlx_vliw_at_b_iq6_bug4.cnf | 235277 | 8063780 | 8308422 | 609703 | 2044 | 2307.08 | SAT |
9dlx_vliw_at_b_iq6_bug5.cnf | 235923 | 8076534 | 6101998 | 315212 | 1022 | 992.68 | SAT |
9dlx_vliw_at_b_iq6_bug6.cnf | 235926 | 8076539 | 1591162 | 8813 | 60 | 69.00 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 4860539 | 280124 | 1021 | 730.52 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 3763773 | 64902 | 254 | 231.08 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | 7792074 | 464145 | 1533 | 1649.00 | SAT |
Total (9 / 9) | 47731941 | 2651683 | 8998 | 9093.65 |
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 | 10658066 | 539696 | 1788 | 2650.10 | SAT |
9dlx_vliw_at_b_iq8_bug2.cnf | 409731 | 15576332 | |||||
9dlx_vliw_at_b_iq8_bug3.cnf | 410219 | 15596614 | |||||
9dlx_vliw_at_b_iq8_bug4.cnf | 409220 | 15574959 | |||||
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 | 2850265 | 16087 | 92 | 156.17 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | 13504944 | 864392 | 2557 | 4324.75 | SAT |
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | 16712478 | 634125 | 2045 | 3580.82 | SAT |
Total (4 / 10) | 43725753 | 2054300 | 6482 | 10711.84 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 7244717 | 21846 | 124 | 216.98 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 7010933 | 32333 | 156 | 261.72 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 4881405 | 8807 | 60 | 127.33 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 3998208 | 4502 | 30 | 88.97 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 5142087 | 12717 | 68 | 151.38 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 7550871 | 31675 | 151 | 273.72 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 5106179 | 7721 | 52 | 117.70 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 4986555 | 8887 | 60 | 128.10 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 6445094 | 21743 | 124 | 203.92 | SAT |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 7700679 | 10069 | 61 | 150.65 | SAT |
Total (10 / 10) | 60066728 | 160300 | 886 | 1720.47 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 2708177 | 800266 | 2379 | 1139.77 | UNSAT |
9dlx_vliw_at_b_iq2.cnf | 44095 | 542253 | 5404985 | 1186545 | 3580 | 2702.32 | UNSAT |
9dlx_vliw_at_b_iq3.cnf | 69789 | 968295 | 9861698 | 1762612 | 4809 | 5453.89 | UNSAT |
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 (3 / 9) | 17974860 | 3749423 | 10768 | 9295.98 |
vliw_unsat_3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq8_I3_C24.cnf | 132413 | 1435600 | 40601194 | 1758265 | 4794 | 6232.20 | UNSAT |
9dlx_vliw_at_b_iq8_I3_C24_D.cnf | 132156 | 1434887 | 40923072 | 1887250 | 5117 | 6686.99 | UNSAT |
Total (2 / 2) | 81524266 | 3645515 | 9911 | 12919.19 |
vliw_unsat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_C1.cnf | 96177 | 1814189 | 5441716 | 582451 | 1986 | 1082.56 | 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) | 5441716 | 582451 | 1986 | 1082.56 |