Tinisat, using restart policy (Luby's, unit=2048)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 180 (73 SAT + 107 UNSAT)
Time: 654185 seconds / 181.72 hours / 7.57 days
Time on solved instances: 142985 seconds (56277 SAT + 86708 UNSAT)
Instances solved in 10 minutes: 115 (10848 seconds)
Instances solved in 15 minutes: 131 (22911 seconds)
Instances solved in 20 minutes: 136 (28404 seconds)
Instances solved in 30 minutes: 151 (50315 seconds)
Instances solved in 60 minutes: 172 (105638 seconds)
Instances solved in 90 minutes: 178 (131253 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 32 | / | 32 | 61799.14 | ||
engine_unsat_1.0 | 7 | / | 10 | 1705.73 | ||
fvp-sat.3.0 | 17 | / | 20 | 10271.86 | ||
fvp-unsat.1.0 | 4 | / | 4 | 37.07 | ||
fvp-unsat.2.0 | 22 | / | 22 | 1134 | ||
fvp-unsat.3.0 | 0 | / | 6 | 0 | ||
liveness_sat_1.0 | 7 | / | 10 | 14685.57 | ||
liveness_unsat_1.0 | 4 | / | 12 | 977.7 | ||
liveness_unsat_2.0 | 3 | / | 9 | 72.7 | ||
npe-1.0 | 4 | / | 6 | 4494.86 | ||
pipe_ooo_unsat_1.0 | 7 | / | 15 | 5217.04 | ||
pipe_ooo_unsat_1.1 | 8 | / | 14 | 3796.62 | ||
pipe_sat_1.0 | 10 | / | 10 | 4435.39 | ||
pipe_sat_1.1 | 10 | / | 10 | 3293.73 | ||
pipe_unsat_1.0 | 8 | / | 13 | 2142.38 | ||
pipe_unsat_1.1 | 11 | / | 14 | 11633.49 | ||
vliw_sat_2.0 | 9 | / | 9 | 8804.11 | ||
vliw_sat_2.1 | 4 | / | 10 | 3270.42 | ||
vliw_sat_4.0 | 10 | / | 10 | 1331.32 | ||
vliw_unsat_2.0 | 2 | / | 9 | 2656.95 | ||
vliw_unsat_3.0 | 0 | / | 2 | 0 | ||
vliw_unsat_4.0 | 1 | / | 4 | 1225.09 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 5687702 | 217833 | 45 | 866.50 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 6213436 | 246729 | 52 | 1042.10 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 6957262 | 229547 | 46 | 1014.80 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 7502080 | 250822 | 52 | 1197.44 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 8189443 | 270120 | 58 | 1372.98 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 9177908 | 252978 | 52 | 1432.29 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 9416858 | 279380 | 60 | 1564.18 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 10069279 | 283773 | 60 | 1690.63 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 10695947 | 279417 | 60 | 1723.30 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 11777013 | 286717 | 60 | 1907.02 | UNSAT |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2410192 | 120843 | 29 | 311.85 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 13084297 | 363684 | 62 | 2269.44 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 13447963 | 311061 | 61 | 2215.91 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | 13960220 | 378445 | 62 | 3589.35 | UNSAT |
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 15045554 | 349065 | 62 | 2653.66 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 15555823 | 366578 | 62 | 3041.01 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 17481328 | 381102 | 62 | 3164.18 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | 18670429 | 364029 | 62 | 3212.83 | UNSAT |
1dlx_c_iq59_a.cnf | 623700 | 9457051 | 18966333 | 391255 | 62 | 3644.81 | UNSAT |
1dlx_c_iq60_a.cnf | 651875 | 9927770 | 20134452 | 374152 | 62 | 3710.57 | UNSAT |
1dlx_c_iq61_a.cnf | 673311 | 10435991 | 14461110 | 293838 | 60 | 2800.01 | SAT |
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 2775987 | 146795 | 30 | 383.97 | UNSAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | 23433691 | 438731 | 76 | 4437.00 | UNSAT |
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 13956895 | 275565 | 59 | 2935.42 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | 26181519 | 454590 | 77 | 4927.99 | UNSAT |
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 3238516 | 166041 | 32 | 459.18 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 4047736 | 201491 | 43 | 724.88 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 4070187 | 218978 | 45 | 823.94 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 4185431 | 190199 | 38 | 611.94 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 4363609 | 165519 | 31 | 604.09 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 4817632 | 172932 | 34 | 674.45 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 5385768 | 208779 | 44 | 791.42 | UNSAT |
Total (32 / 32) | 345361600 | 8930988 | 1700 | 61799.14 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_4.cnf | 6944 | 66654 | 45833 | 29716 | 9 | 10.18 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 129559 | 95206 | 24 | 56.57 | UNSAT |
engine_5.cnf | 18788 | 214095 | 692374 | 536604 | 93 | 1271.02 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 17090 | 10735 | 4 | 5.57 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 51057 | 36862 | 11 | 23.67 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 65706 | 46396 | 13 | 52.89 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | |||||
engine_6_nd_case1.cnf | 45435 | 610120 | 225053 | 173609 | 34 | 285.83 | UNSAT |
Total (7 / 10) | 1226672 | 929128 | 188 | 1705.73 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | 213938 | 14834 | 5 | 10.22 | SAT |
pipe_64_4_bug02.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug03.cnf | 35947 | 992674 | 133085 | 9184 | 3 | 7.08 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 71141 | 3353 | 1 | 5.03 | SAT |
pipe_64_4_bug05.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug06.cnf | 35853 | 1012271 | 10959151 | 1620120 | 251 | 2892.95 | SAT |
pipe_64_4_bug07.cnf | 35853 | 1012271 | 2977254 | 460565 | 78 | 376.07 | SAT |
pipe_64_4_bug08.cnf | 35622 | 1003074 | 1192627 | 104933 | 27 | 53.53 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 238876 | 14927 | 5 | 10.87 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 414637 | 31172 | 9 | 17.91 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | 844352 | 89267 | 21 | 46.12 | SAT |
pipe_64_4_bug12.cnf | 35854 | 1012275 | 1418205 | 198043 | 41 | 104.59 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 1482069 | 179658 | 36 | 100.70 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 1174594 | 128403 | 29 | 65.32 | SAT |
pipe_64_4_bug15.cnf | 35853 | 1012271 | 3403382 | 425830 | 72 | 320.63 | SAT |
pipe_64_4_bug16.cnf | 35853 | 1012271 | 1364509 | 187589 | 37 | 100.19 | SAT |
pipe_64_4_bug17.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug18.cnf | 35853 | 1012271 | 9952023 | 1534105 | 235 | 2699.21 | SAT |
pipe_64_4_bug19.cnf | 35852 | 1012266 | 9773047 | 1304319 | 189 | 2013.96 | SAT |
pipe_64_4_bug20.cnf | 35853 | 1012271 | 6708795 | 1054389 | 157 | 1447.48 | SAT |
Total (17 / 20) | 52321685 | 7360691 | 1196 | 10271.86 |
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 | 21897 | 5036 | 2 | 0.45 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 31282 | 8829 | 3 | 1.01 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 465847 | 90802 | 22 | 35.59 | UNSAT |
Total (4 / 4) | 521310 | 105337 | 27 | 37.07 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 3014 | 1170 | 0 | 0.04 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 2509 | 1089 | 0 | 0.04 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 2895 | 1371 | 0 | 0.06 | UNSAT |
3pipe.cnf | 2468 | 27533 | 20243 | 6909 | 2 | 0.59 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 14656 | 7136 | 2 | 0.61 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 19692 | 9397 | 3 | 0.92 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 24196 | 10908 | 4 | 1.19 | UNSAT |
4pipe.cnf | 5237 | 80213 | 78264 | 30579 | 9 | 6.86 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 51898 | 20673 | 6 | 4.38 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 74950 | 29928 | 9 | 7.69 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 70404 | 26149 | 7 | 6.66 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 120105 | 52332 | 14 | 17.57 | UNSAT |
5pipe.cnf | 9471 | 195452 | 112147 | 17496 | 6 | 5.41 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 122567 | 43458 | 13 | 20.73 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 133714 | 43384 | 13 | 23.09 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 137984 | 42090 | 13 | 22.35 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 256354 | 83279 | 21 | 51.00 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 139438 | 43477 | 13 | 23.68 | UNSAT |
6pipe.cnf | 15800 | 394739 | 442329 | 108151 | 28 | 75.43 | UNSAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 422241 | 119837 | 29 | 136.34 | UNSAT |
7pipe.cnf | 23910 | 751118 | 1310996 | 372217 | 62 | 724.83 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 67878 | 8207 | 3 | 4.53 | SAT |
Total (22 / 22) | 3628474 | 1079237 | 257 | 1134 |
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 | 1457120 | 372727 | 62 | 2015.03 | SAT |
2dlx_cc_ex_bp_f_bug6_liveness.cnf | 331848 | 5706594 | 2519456 | 692024 | 124 | 4676.36 | SAT |
2dlx_cc_ex_bp_f_bug7_liveness.cnf | 375775 | 6617342 | 2861215 | 787391 | 126 | 5764.46 | 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 | 241077 | 37088 | 12 | 136.30 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 224082 | 40347 | 12 | 159.14 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 1439909 | 397955 | 65 | 1826.07 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 144682 | 18917 | 6 | 108.21 | SAT |
Total (7 / 10) | 8887541 | 2346449 | 407 | 14685.57 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 142231 | 75371 | 18 | 47.86 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 679368 | 389658 | 62 | 881.04 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 130495 | 61798 | 14 | 44.49 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 38905 | 19647 | 6 | 4.31 | 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) | 990999 | 546474 | 100 | 977.7 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 50275 | 22130 | 6 | 5.13 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 147933 | 65861 | 15 | 35.31 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 111471 | 52049 | 14 | 32.26 | 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) | 309679 | 140040 | 35 | 72.7 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 13871 | 7992 | 2 | 1.20 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 142295 | 97690 | 24 | 50.35 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 341937 | 102885 | 27 | 225.46 | SAT |
2dlx_cc_mc_ex_bp_f2_no_pe.cnf | 96675 | 1401773 | |||||
9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf | 889302 | 14582074 | 3497913 | 334690 | 62 | 4217.85 | SAT |
9dlx_vliw_at_bp_mc2_no_pe.cnf | 889302 | 14582081 | |||||
Total (4 / 6) | 3996016 | 543257 | 115 | 4494.86 |
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 | 24333 | 10756 | 4 | 1.09 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 99940 | 39331 | 12 | 10.23 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 296567 | 109480 | 28 | 61.04 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 670307 | 223104 | 45 | 206.05 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 2452792 | 920516 | 128 | 2141.73 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 3669833 | 980082 | 141 | 2796.84 | UNSAT |
Total (7 / 15) | 7216342 | 2284663 | 358 | 5217.04 |
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 | 25881 | 9787 | 3 | 0.87 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 84448 | 26690 | 8 | 5.21 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 292547 | 89058 | 21 | 39.23 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 687708 | 193625 | 40 | 149.66 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 1405129 | 288771 | 60 | 350.32 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 3310541 | 826395 | 126 | 2146.44 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 2740086 | 513318 | 92 | 1104.84 | UNSAT |
Total (8 / 14) | 8549576 | 1949161 | 350 | 3796.62 |
pipe_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 118040 | 8804672 | 38089 | 1346 | 0 | 19.12 | SAT |
12pipe_bug10.cnf | 118040 | 8804672 | 1940470 | 425957 | 72 | 1779.80 | SAT |
12pipe_bug2.cnf | 118040 | 8804630 | 82387 | 8014 | 2 | 35.21 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | 1112912 | 239428 | 49 | 798.74 | SAT |
12pipe_bug4.cnf | 117504 | 8743027 | 484447 | 81965 | 21 | 257.30 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | 77547 | 5053 | 2 | 33.25 | SAT |
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 16.36 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | 1756881 | 407023 | 68 | 1438.37 | SAT |
12pipe_bug8.cnf | 117526 | 8760516 | 115534 | 10242 | 4 | 38.85 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | 35742 | 1114 | 0 | 18.39 | SAT |
Total (10 / 10) | 5649486 | 1180142 | 218 | 4435.39 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 889084 | 129522 | 29 | 409.55 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | 470000 | 69145 | 16 | 193.98 | SAT |
12pipe_bug2_q0.cnf | 138918 | 4678718 | 578486 | 70466 | 17 | 205.34 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 1482350 | 264670 | 57 | 698.20 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 490482 | 78370 | 20 | 225.12 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 1262806 | 200898 | 43 | 573.31 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | 139207 | 10324 | 4 | 38.10 | SAT |
12pipe_bug7_q0.cnf | 138918 | 4678760 | 125455 | 6547 | 2 | 28.17 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 113110 | 7615 | 2 | 26.95 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | 1821257 | 332945 | 62 | 895.01 | SAT |
Total (10 / 10) | 7372237 | 1170502 | 252 | 3293.73 |
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 | 19692 | 6386 | 2 | 0.55 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 70845 | 24463 | 6 | 5.25 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 243611 | 88031 | 21 | 46.10 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 193775 | 27935 | 8 | 13.91 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 1140493 | 333647 | 62 | 543.37 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 2216709 | 578793 | 100 | 1382.33 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 1324519 | 93463 | 23 | 150.82 | 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) | 5212574 | 1153938 | 222 | 2142.38 |
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 | 16610 | 6012 | 2 | 0.43 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 66809 | 21217 | 6 | 3.53 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 192427 | 61797 | 14 | 20.48 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 208476 | 33688 | 10 | 14.25 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 792062 | 172564 | 34 | 127.96 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 1612307 | 444928 | 77 | 618.85 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1159904 | 99712 | 25 | 122.22 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 3889712 | 603296 | 107 | 1226.22 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | 6457648 | 1200590 | 187 | 3531.78 | UNSAT |
12pipe_q0_k.cnf | 136800 | 4216460 | 9601674 | 1602371 | 250 | 5967.73 | UNSAT |
13pipe_q0_k.cnf | 176066 | 5761591 | |||||
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (11 / 14) | 24000423 | 4247261 | 712 | 11633.49 |
vliw_sat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 236038 | 8084666 | 3874865 | 170645 | 33 | 397.39 | SAT |
9dlx_vliw_at_b_iq6_bug2.cnf | 235928 | 8076545 | 120421 | 59 | 0 | 17.27 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 235402 | 8060882 | 7582735 | 590540 | 104 | 1766.58 | SAT |
9dlx_vliw_at_b_iq6_bug4.cnf | 235277 | 8063780 | 9706044 | 1084467 | 159 | 3397.46 | SAT |
9dlx_vliw_at_b_iq6_bug5.cnf | 235923 | 8076534 | 5541883 | 346235 | 62 | 887.35 | SAT |
9dlx_vliw_at_b_iq6_bug6.cnf | 235926 | 8076539 | 900576 | 4461 | 2 | 41.85 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 3044374 | 157029 | 30 | 315.89 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 4318487 | 257708 | 54 | 648.55 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | 6592141 | 519045 | 92 | 1331.77 | SAT |
Total (9 / 9) | 41681526 | 3130189 | 536 | 8804.11 |
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 | 7621180 | 338191 | 62 | 1258.40 | SAT |
9dlx_vliw_at_b_iq8_bug2.cnf | 409731 | 15576332 | |||||
9dlx_vliw_at_b_iq8_bug3.cnf | 410219 | 15596614 | 6653131 | 196565 | 40 | 812.79 | SAT |
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 | 665035 | 2486 | 1 | 65.27 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | 8054555 | 323901 | 61 | 1133.96 | SAT |
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | |||||
Total (4 / 10) | 22993901 | 861143 | 164 | 3270.42 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 6522663 | 24489 | 6 | 192.13 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 4640087 | 7965 | 2 | 97.19 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 5634313 | 9273 | 3 | 116.51 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 5331248 | 5319 | 2 | 91.25 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 6987623 | 22103 | 6 | 186.89 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 7791272 | 23069 | 6 | 172.63 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 5281389 | 3696 | 1 | 77.41 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 6808786 | 19596 | 6 | 163.71 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 6571282 | 14106 | 5 | 143.69 | SAT |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 5415298 | 8030 | 2 | 89.91 | SAT |
Total (10 / 10) | 60983961 | 137646 | 39 | 1331.32 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 1956346 | 560981 | 95 | 583.50 | UNSAT |
9dlx_vliw_at_b_iq2.cnf | 44095 | 542253 | 5055924 | 1247957 | 189 | 2073.45 | 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) | 7012270 | 1808938 | 284 | 2656.95 |
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 | 5530198 | 760868 | 125 | 1225.09 | 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) | 5530198 | 760868 | 125 | 1225.09 |