Tinisat, using restart policy (Luby's, unit=1024)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 182 (74 SAT + 108 UNSAT)
Time: 657610 seconds / 182.67 hours / 7.61 days
Time on solved instances: 160810 seconds (71723 SAT + 89086 UNSAT)
Instances solved in 10 minutes: 115 (13260 seconds)
Instances solved in 15 minutes: 129 (22956 seconds)
Instances solved in 20 minutes: 137 (31329 seconds)
Instances solved in 30 minutes: 149 (48560 seconds)
Instances solved in 60 minutes: 170 (104980 seconds)
Instances solved in 90 minutes: 180 (147036 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 32 | / | 32 | 59660.01 | ||
engine_unsat_1.0 | 7 | / | 10 | 1730.06 | ||
fvp-sat.3.0 | 17 | / | 20 | 20100.62 | ||
fvp-unsat.1.0 | 4 | / | 4 | 44.36 | ||
fvp-unsat.2.0 | 22 | / | 22 | 820.61 | ||
fvp-unsat.3.0 | 0 | / | 6 | 0 | ||
liveness_sat_1.0 | 7 | / | 10 | 9727.84 | ||
liveness_unsat_1.0 | 4 | / | 12 | 1025.3 | ||
liveness_unsat_2.0 | 3 | / | 9 | 59.26 | ||
npe-1.0 | 4 | / | 6 | 2230.12 | ||
pipe_ooo_unsat_1.0 | 7 | / | 15 | 5268.39 | ||
pipe_ooo_unsat_1.1 | 8 | / | 14 | 3453.16 | ||
pipe_sat_1.0 | 9 | / | 10 | 3014.26 | ||
pipe_sat_1.1 | 10 | / | 10 | 4156.97 | ||
pipe_unsat_1.0 | 8 | / | 13 | 1338.29 | ||
pipe_unsat_1.1 | 12 | / | 14 | 15572.58 | ||
vliw_sat_2.0 | 9 | / | 9 | 9524.54 | ||
vliw_sat_2.1 | 6 | / | 10 | 16243.04 | ||
vliw_sat_4.0 | 10 | / | 10 | 1228.96 | ||
vliw_unsat_2.0 | 2 | / | 9 | 4465.96 | ||
vliw_unsat_3.0 | 0 | / | 2 | 0 | ||
vliw_unsat_4.0 | 1 | / | 4 | 1145.24 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 5578218 | 197673 | 64 | 819.14 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 6416454 | 204891 | 69 | 968.05 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 6840901 | 232797 | 80 | 1071.23 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 6732265 | 211039 | 72 | 1063.52 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 7763083 | 238924 | 84 | 1265.72 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 8417199 | 236689 | 83 | 1317.37 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 8918662 | 271199 | 93 | 1487.03 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 9306309 | 269087 | 93 | 1556.59 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 10618572 | 267708 | 93 | 1758.29 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 11880434 | 276970 | 93 | 1878.72 | UNSAT |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2477615 | 122521 | 51 | 323.53 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 11545693 | 275206 | 93 | 1997.22 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 13502818 | 325430 | 117 | 2222.08 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | 13066204 | 368660 | 125 | 3466.67 | UNSAT |
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 15981374 | 343123 | 123 | 2684.13 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 15840552 | 361880 | 125 | 2910.08 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 17332125 | 337422 | 123 | 2939.82 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | 19271020 | 402065 | 126 | 3485.04 | UNSAT |
1dlx_c_iq59_a.cnf | 623700 | 9457051 | 18721202 | 363735 | 125 | 3358.56 | UNSAT |
1dlx_c_iq60_a.cnf | 651875 | 9927770 | 20351107 | 376044 | 125 | 3650.40 | UNSAT |
1dlx_c_iq61_a.cnf | 673311 | 10435991 | 13878696 | 291765 | 101 | 2813.19 | SAT |
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 2784164 | 130939 | 55 | 363.72 | UNSAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | 21744823 | 398281 | 126 | 4171.76 | UNSAT |
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 13310689 | 269532 | 93 | 2711.37 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | 25883559 | 455570 | 126 | 4844.68 | UNSAT |
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 2985866 | 142561 | 60 | 410.98 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 3537226 | 177175 | 62 | 657.62 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 3663661 | 182687 | 62 | 707.95 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 4232128 | 159401 | 61 | 583.40 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 4306630 | 175417 | 62 | 627.15 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 4912460 | 193087 | 62 | 731.88 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 5699727 | 205615 | 69 | 813.12 | UNSAT |
Total (32 / 32) | 337501436 | 8465093 | 2896 | 59660.01 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_4.cnf | 6944 | 66654 | 45003 | 29672 | 14 | 9.91 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 126104 | 92622 | 37 | 55.29 | UNSAT |
engine_5.cnf | 18788 | 214095 | 707978 | 544405 | 160 | 1297.34 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 17460 | 11227 | 6 | 6.16 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 53823 | 38491 | 19 | 25.49 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 62228 | 43346 | 21 | 49.93 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | |||||
engine_6_nd_case1.cnf | 45435 | 610120 | 227149 | 171352 | 62 | 285.94 | UNSAT |
Total (7 / 10) | 1239745 | 931115 | 319 | 1730.06 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | 304229 | 23312 | 13 | 12.56 | SAT |
pipe_64_4_bug02.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug03.cnf | 35947 | 992674 | 78780 | 1384 | 1 | 2.60 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 89955 | 2028 | 1 | 4.07 | SAT |
pipe_64_4_bug05.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug06.cnf | 35853 | 1012271 | 9260785 | 1229911 | 317 | 1950.03 | SAT |
pipe_64_4_bug07.cnf | 35853 | 1012271 | 4937602 | 647867 | 189 | 706.10 | SAT |
pipe_64_4_bug08.cnf | 35622 | 1003074 | 2468496 | 273972 | 93 | 179.60 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 700206 | 58223 | 29 | 27.15 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 178879 | 10330 | 6 | 7.97 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | 18862067 | 2594457 | 593 | 6605.57 | SAT |
pipe_64_4_bug12.cnf | 35854 | 1012275 | 1584512 | 138970 | 59 | 81.88 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 590897 | 56487 | 28 | 25.15 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 1014173 | 107267 | 45 | 51.80 | SAT |
pipe_64_4_bug15.cnf | 35853 | 1012271 | 3904424 | 380881 | 125 | 283.76 | SAT |
pipe_64_4_bug16.cnf | 35853 | 1012271 | 10230137 | 1301144 | 346 | 2247.16 | SAT |
pipe_64_4_bug17.cnf | 35853 | 1012271 | 11427132 | 1484421 | 381 | 2644.49 | SAT |
pipe_64_4_bug18.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug19.cnf | 35852 | 1012266 | 8600489 | 953737 | 254 | 1229.13 | SAT |
pipe_64_4_bug20.cnf | 35853 | 1012271 | 14010105 | 1859055 | 506 | 4041.60 | SAT |
Total (17 / 20) | 88242868 | 11123446 | 2986 | 20100.62 |
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 | 21694 | 5027 | 3 | 0.43 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 32328 | 9032 | 6 | 1.13 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 492760 | 104391 | 44 | 42.78 | UNSAT |
Total (4 / 4) | 549066 | 119120 | 53 | 44.36 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 3274 | 1321 | 1 | 0.05 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 2531 | 1105 | 1 | 0.05 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 2947 | 1378 | 1 | 0.06 | UNSAT |
3pipe.cnf | 2468 | 27533 | 21130 | 7243 | 5 | 0.65 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 14054 | 6702 | 5 | 0.61 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 20658 | 9697 | 6 | 1.01 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 23128 | 9991 | 6 | 1.09 | UNSAT |
4pipe.cnf | 5237 | 80213 | 71776 | 23564 | 13 | 4.85 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 53178 | 22975 | 13 | 4.79 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 79002 | 32911 | 15 | 8.75 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 72091 | 24453 | 13 | 6.37 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 81756 | 32427 | 14 | 8.69 | UNSAT |
5pipe.cnf | 9471 | 195452 | 114093 | 17027 | 10 | 4.96 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 105114 | 37074 | 18 | 14.83 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 128210 | 45030 | 21 | 21.69 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 140029 | 43885 | 21 | 21.70 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 342000 | 132491 | 57 | 88.56 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 127636 | 38899 | 19 | 19.24 | UNSAT |
6pipe.cnf | 15800 | 394739 | 573247 | 171622 | 62 | 157.11 | UNSAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 392700 | 112020 | 45 | 110.60 | UNSAT |
7pipe.cnf | 23910 | 751118 | 970820 | 253082 | 91 | 342.05 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 44404 | 5178 | 4 | 2.90 | SAT |
Total (22 / 22) | 3383778 | 1030075 | 441 | 820.61 |
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 | 528687 | 91956 | 37 | 500.97 | SAT |
2dlx_cc_ex_bp_f_bug6_liveness.cnf | 331848 | 5706594 | 2780201 | 750822 | 229 | 5118.34 | SAT |
2dlx_cc_ex_bp_f_bug7_liveness.cnf | 375775 | 6617342 | 2074919 | 509253 | 153 | 3326.05 | SAT |
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 | 187159 | 25755 | 14 | 104.09 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 244727 | 38582 | 19 | 156.32 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 361525 | 60046 | 29 | 269.57 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 332500 | 49425 | 25 | 252.50 | SAT |
Total (7 / 10) | 6509718 | 1525839 | 506 | 9727.84 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 118087 | 57647 | 29 | 30.16 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 694709 | 398368 | 126 | 953.92 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 115977 | 54318 | 28 | 36.63 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 41264 | 19892 | 12 | 4.59 | 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) | 970037 | 530225 | 195 | 1025.3 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 45943 | 18352 | 11 | 4.15 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 126254 | 53760 | 28 | 27.57 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 103376 | 47884 | 24 | 27.54 | 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) | 275573 | 119996 | 63 | 59.26 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 3072 | 1067 | 1 | 0.18 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 103191 | 70485 | 30 | 30.33 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 399566 | 123524 | 52 | 272.91 | SAT |
2dlx_cc_mc_ex_bp_f2_no_pe.cnf | 96675 | 1401773 | |||||
9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf | 889302 | 14582074 | 2126608 | 142386 | 60 | 1926.70 | SAT |
9dlx_vliw_at_bp_mc2_no_pe.cnf | 889302 | 14582081 | |||||
Total (4 / 6) | 2632437 | 337462 | 143 | 2230.12 |
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 | 2420 | 1234 | 1 | 0.05 | UNSAT |
3pipe_3_ooo.cnf | 2533 | 32182 | 23728 | 10080 | 6 | 1.06 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 102269 | 40660 | 20 | 10.76 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 375623 | 154701 | 61 | 101.03 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 836084 | 306028 | 108 | 344.15 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 2033204 | 682478 | 204 | 1358.96 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 4064244 | 1116434 | 285 | 3452.38 | UNSAT |
Total (7 / 15) | 7437572 | 2311615 | 685 | 5268.39 |
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 | 3054 | 1423 | 1 | 0.05 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 2566 | 25625 | 23206 | 8944 | 6 | 0.77 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 80692 | 22893 | 13 | 4.28 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 297220 | 89488 | 36 | 39.31 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 633536 | 153346 | 61 | 113.39 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 1475703 | 343024 | 123 | 457.16 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 3334090 | 748359 | 227 | 1776.87 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 2686867 | 474599 | 136 | 1061.33 | UNSAT |
Total (8 / 14) | 8534368 | 1842076 | 603 | 3453.16 |
pipe_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 118040 | 8804672 | 582898 | 114706 | 46 | 369.67 | SAT |
12pipe_bug10.cnf | 118040 | 8804672 | 543551 | 96528 | 40 | 321.78 | SAT |
12pipe_bug2.cnf | 118040 | 8804630 | 455325 | 94514 | 38 | 304.32 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | 989407 | 202704 | 67 | 711.92 | SAT |
12pipe_bug4.cnf | 117504 | 8743027 | 196697 | 32841 | 15 | 108.08 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | 886121 | 182453 | 62 | 569.85 | SAT |
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 16.54 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | |||||
12pipe_bug8.cnf | 117526 | 8760516 | 150360 | 12296 | 7 | 50.48 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | 782608 | 163999 | 62 | 561.62 | SAT |
Total (9 / 10) | 4592444 | 900041 | 337 | 3014.26 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 234678 | 28248 | 14 | 87.96 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | 1043087 | 132987 | 57 | 403.48 | SAT |
12pipe_bug2_q0.cnf | 138918 | 4678718 | 91475 | 3638 | 2 | 20.80 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 1508112 | 183514 | 62 | 609.96 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 64460 | 5160 | 4 | 22.42 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 1494922 | 231795 | 80 | 657.99 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | 459136 | 56037 | 28 | 168.06 | SAT |
12pipe_bug7_q0.cnf | 138918 | 4678760 | 2907004 | 497823 | 147 | 1537.71 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 90588 | 2062 | 2 | 19.27 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | 1451208 | 195922 | 62 | 629.32 | SAT |
Total (10 / 10) | 9344670 | 1337186 | 458 | 4156.97 |
pipe_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 860 | 6693 | 3290 | 1262 | 1 | 0.05 | UNSAT |
03pipe_k.cnf | 2391 | 27405 | 21086 | 7719 | 5 | 0.68 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 74266 | 27109 | 14 | 5.77 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 209433 | 63716 | 29 | 30.54 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 214231 | 26699 | 14 | 13.87 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 1291434 | 369896 | 125 | 646.66 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 1537130 | 288666 | 100 | 475.16 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 1425479 | 110992 | 45 | 165.56 | 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) | 4776349 | 896059 | 333 | 1338.29 |
pipe_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 873 | 6457 | 2819 | 1104 | 1 | 0.04 | UNSAT |
03pipe_q0_k.cnf | 2476 | 25181 | 18884 | 6819 | 5 | 0.49 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 65846 | 22726 | 13 | 3.60 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 223579 | 79336 | 30 | 30.65 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 207104 | 26499 | 14 | 11.63 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 1028379 | 298133 | 106 | 320.52 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 1337991 | 299978 | 107 | 351.33 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1275734 | 94673 | 38 | 119.09 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 3933776 | 645296 | 189 | 1315.96 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | 5970972 | 840900 | 252 | 2112.72 | UNSAT |
12pipe_q0_k.cnf | 136800 | 4216460 | 8977760 | 1227786 | 317 | 4138.86 | UNSAT |
13pipe_q0_k.cnf | 176066 | 5761591 | 14061713 | 1664401 | 443 | 7167.69 | UNSAT |
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (12 / 14) | 37104557 | 5207651 | 1515 | 15572.58 |
vliw_sat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 236038 | 8084666 | 6526376 | 416332 | 126 | 1071.23 | SAT |
9dlx_vliw_at_b_iq6_bug2.cnf | 235928 | 8076545 | 120421 | 59 | 0 | 17.51 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 235402 | 8060882 | 8406989 | 999162 | 254 | 3092.40 | SAT |
9dlx_vliw_at_b_iq6_bug4.cnf | 235277 | 8063780 | 5655082 | 264786 | 93 | 747.18 | SAT |
9dlx_vliw_at_b_iq6_bug5.cnf | 235923 | 8076534 | 8083934 | 862538 | 253 | 2623.11 | SAT |
9dlx_vliw_at_b_iq6_bug6.cnf | 235926 | 8076539 | 695830 | 2629 | 2 | 37.64 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 2560788 | 166652 | 62 | 328.72 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 3635382 | 243665 | 86 | 568.31 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | 6749387 | 397881 | 126 | 1038.44 | SAT |
Total (9 / 9) | 42434189 | 3353704 | 1002 | 9524.54 |
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 | 9252960 | 342225 | 123 | 1330.86 | SAT |
9dlx_vliw_at_b_iq8_bug2.cnf | 409731 | 15576332 | 10478930 | 684537 | 204 | 2578.00 | SAT |
9dlx_vliw_at_b_iq8_bug3.cnf | 410219 | 15596614 | |||||
9dlx_vliw_at_b_iq8_bug4.cnf | 409220 | 15574959 | 13836815 | 1041342 | 254 | 4287.88 | 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 | 1269856 | 4695 | 3 | 80.17 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | 15786065 | 920985 | 254 | 3988.38 | SAT |
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | 19113384 | 839952 | 252 | 3977.75 | SAT |
Total (6 / 10) | 69738010 | 3833736 | 1090 | 16243.04 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 6251550 | 25962 | 14 | 205.22 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 7158232 | 20584 | 13 | 177.22 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 6080670 | 11134 | 6 | 122.93 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 4321289 | 3628 | 2 | 73.41 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 5283713 | 12587 | 7 | 132.08 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 4286042 | 5301 | 4 | 91.07 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 5633919 | 10003 | 6 | 117.66 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 3265284 | 1742 | 1 | 57.41 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 5445662 | 18214 | 11 | 145.30 | SAT |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 4589119 | 8726 | 6 | 106.66 | SAT |
Total (10 / 10) | 52315480 | 117881 | 70 | 1228.96 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 2277461 | 632450 | 189 | 629.56 | UNSAT |
9dlx_vliw_at_b_iq2.cnf | 44095 | 542253 | 6217255 | 1638370 | 437 | 3836.40 | 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) | 8494716 | 2270820 | 626 | 4465.96 |
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 | 5250086 | 697541 | 211 | 1145.24 | 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) | 5250086 | 697541 | 211 | 1145.24 |