Tinisat, using restart policy (Luby's, unit=2)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 175 (65 SAT + 110 UNSAT)
Time: 767276 seconds / 213.13 hours / 8.88 days
Time on solved instances: 220076 seconds (88204 SAT + 131871 UNSAT)
Instances solved in 10 minutes: 105 (10532 seconds)
Instances solved in 15 minutes: 113 (16881 seconds)
Instances solved in 20 minutes: 117 (21326 seconds)
Instances solved in 30 minutes: 132 (44784 seconds)
Instances solved in 60 minutes: 152 (97327 seconds)
Instances solved in 90 minutes: 164 (151227 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 30 | / | 32 | 87805.36 | ||
engine_unsat_1.0 | 7 | / | 10 | 4464.49 | ||
fvp-sat.3.0 | 16 | / | 20 | 30047.14 | ||
fvp-unsat.1.0 | 4 | / | 4 | 67.28 | ||
fvp-unsat.2.0 | 22 | / | 22 | 477.33 | ||
fvp-unsat.3.0 | 0 | / | 6 | 0 | ||
liveness_sat_1.0 | 6 | / | 10 | 11892.87 | ||
liveness_unsat_1.0 | 4 | / | 12 | 1822.39 | ||
liveness_unsat_2.0 | 3 | / | 9 | 85.39 | ||
npe-1.0 | 3 | / | 6 | 174.03 | ||
pipe_ooo_unsat_1.0 | 7 | / | 15 | 7303.74 | ||
pipe_ooo_unsat_1.1 | 8 | / | 14 | 3507.43 | ||
pipe_sat_1.0 | 10 | / | 10 | 8645.44 | ||
pipe_sat_1.1 | 10 | / | 10 | 3979.34 | ||
pipe_unsat_1.0 | 12 | / | 13 | 17539.86 | ||
pipe_unsat_1.1 | 12 | / | 14 | 13656.62 | ||
vliw_sat_2.0 | 7 | / | 9 | 18755.88 | ||
vliw_sat_2.1 | 1 | / | 10 | 197.74 | ||
vliw_sat_4.0 | 10 | / | 10 | 3669.68 | ||
vliw_unsat_2.0 | 2 | / | 9 | 4166.5 | ||
vliw_unsat_3.0 | 0 | / | 2 | 0 | ||
vliw_unsat_4.0 | 1 | / | 4 | 1817.18 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 6428864 | 162413 | 13080 | 1466.66 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 6857257 | 170451 | 13819 | 1647.50 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 7760068 | 171848 | 14027 | 1736.12 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 8460633 | 180155 | 14587 | 1930.50 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 9327367 | 189977 | 15606 | 2097.36 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 9880160 | 189971 | 15606 | 2248.11 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 10767046 | 195844 | 16248 | 2449.84 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 11912476 | 216498 | 16382 | 2742.94 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 12181502 | 221615 | 16382 | 2944.20 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 13408998 | 239050 | 17405 | 3273.24 | UNSAT |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2840606 | 99467 | 8190 | 532.00 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 13270512 | 240603 | 17556 | 3400.59 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 14803719 | 244192 | 17916 | 3591.48 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | 14609705 | 281353 | 20859 | 6305.59 | UNSAT |
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 17122351 | 263647 | 19688 | 4280.86 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 18054385 | 283853 | 21114 | 4910.21 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 20050389 | 279217 | 20602 | 5010.15 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | 21297920 | 313929 | 23910 | 5801.53 | UNSAT |
1dlx_c_iq59_a.cnf | 623700 | 9457051 | 21835936 | 315420 | 24058 | 6098.57 | UNSAT |
1dlx_c_iq60_a.cnf | 651875 | 9927770 | 23297337 | 316358 | 24139 | 6399.45 | UNSAT |
1dlx_c_iq61_a.cnf | 673311 | 10435991 | 14298447 | 220591 | 16382 | 4724.30 | SAT |
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 3307291 | 110757 | 8701 | 595.39 | UNSAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | |||||
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 19564459 | 274495 | 20477 | 6169.43 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | |||||
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 3338088 | 113350 | 9000 | 656.97 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 3703752 | 128125 | 10237 | 1098.99 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 4348969 | 144998 | 11947 | 1320.06 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 4840216 | 126532 | 10236 | 885.18 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 5028881 | 138300 | 11260 | 1034.39 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 5665713 | 143588 | 11771 | 1161.93 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 5938168 | 153587 | 12285 | 1291.82 | UNSAT |
Total (30 / 32) | 334201215 | 6130184 | 473470 | 87805.36 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_4.cnf | 6944 | 66654 | 76816 | 33117 | 3132 | 21.55 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 237861 | 118168 | 9434 | 143.33 | UNSAT |
engine_5.cnf | 18788 | 214095 | 1264459 | 642254 | 45051 | 3271.40 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 27845 | 12653 | 1340 | 14.34 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 87712 | 43326 | 4093 | 62.41 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 100722 | 49522 | 4157 | 127.63 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | |||||
engine_6_nd_case1.cnf | 45435 | 610120 | 400198 | 216956 | 16382 | 823.83 | UNSAT |
Total (7 / 10) | 2195613 | 1115996 | 83589 | 4464.49 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | 42204 | 24 | 7 | 2.14 | SAT |
pipe_64_4_bug02.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug03.cnf | 35947 | 992674 | 482671 | 1501 | 235 | 7.32 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 179834 | 341 | 62 | 3.21 | SAT |
pipe_64_4_bug05.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug06.cnf | 35853 | 1012271 | 12818368 | 711322 | 49149 | 2504.70 | SAT |
pipe_64_4_bug07.cnf | 35853 | 1012271 | 3093618 | 99304 | 8190 | 145.36 | SAT |
pipe_64_4_bug08.cnf | 35622 | 1003074 | 22308 | 30 | 9 | 2.17 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 96273 | 179 | 37 | 2.56 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 14726 | 21 | 6 | 2.02 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug12.cnf | 35854 | 1012275 | 5111089 | 212640 | 16381 | 379.62 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 129398 | 169 | 34 | 2.68 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 19888956 | 1144707 | 73724 | 5979.88 | SAT |
pipe_64_4_bug15.cnf | 35853 | 1012271 | 5081932 | 209360 | 16381 | 383.49 | SAT |
pipe_64_4_bug16.cnf | 35853 | 1012271 | 21969442 | 1442493 | 95225 | 6273.78 | SAT |
pipe_64_4_bug17.cnf | 35853 | 1012271 | 19636141 | 1150941 | 73725 | 5499.46 | SAT |
pipe_64_4_bug18.cnf | 35853 | 1012271 | 17677092 | 1146540 | 73724 | 4566.31 | SAT |
pipe_64_4_bug19.cnf | 35852 | 1012266 | 18992182 | 929419 | 65531 | 4292.44 | SAT |
pipe_64_4_bug20.cnf | 35853 | 1012271 | |||||
Total (16 / 20) | 125236234 | 7048991 | 472420 | 30047.14 |
fvp-unsat.1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_mc_ex_bp_f.cnf | 776 | 3725 | 2955 | 681 | 124 | 0.03 | UNSAT |
2dlx_ca_mc_ex_bp_f.cnf | 3250 | 24640 | 22079 | 4478 | 510 | 0.51 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 38306 | 8265 | 1018 | 1.53 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 616910 | 82164 | 7217 | 65.21 | UNSAT |
Total (4 / 4) | 680250 | 95588 | 8869 | 67.28 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 4258 | 1117 | 172 | 0.06 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 4216 | 1166 | 186 | 0.06 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 4718 | 1435 | 220 | 0.08 | UNSAT |
3pipe.cnf | 2468 | 27533 | 27905 | 5725 | 683 | 0.66 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 20495 | 5761 | 694 | 0.68 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 26046 | 6533 | 765 | 0.94 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 31013 | 7710 | 923 | 1.18 | UNSAT |
4pipe.cnf | 5237 | 80213 | 97557 | 17129 | 1838 | 5.32 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 81875 | 21481 | 2046 | 6.72 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 85525 | 19232 | 2044 | 6.58 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 90731 | 17525 | 1904 | 6.60 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 116426 | 24441 | 2301 | 9.65 | UNSAT |
5pipe.cnf | 9471 | 195452 | 152263 | 9362 | 1022 | 4.92 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 135999 | 29503 | 2874 | 16.10 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 152785 | 28196 | 2717 | 17.68 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 155458 | 26309 | 2555 | 17.02 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 319597 | 55120 | 4816 | 43.41 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 172041 | 25813 | 2491 | 19.41 | UNSAT |
6pipe.cnf | 15800 | 394739 | 508900 | 53274 | 4605 | 53.92 | UNSAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 482249 | 67020 | 6030 | 89.42 | UNSAT |
7pipe.cnf | 23910 | 751118 | 1077845 | 98224 | 8189 | 174.16 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 36722 | 906 | 131 | 2.76 | SAT |
Total (22 / 22) | 3784624 | 522982 | 49206 | 477.33 |
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 | 1674001 | 235229 | 17083 | 2776.09 | SAT |
2dlx_cc_ex_bp_f_bug6_liveness.cnf | 331848 | 5706594 | 2179532 | 309552 | 23545 | 4362.86 | 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 | 198834 | 20646 | 2046 | 170.73 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 462046 | 53202 | 4604 | 462.36 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 1126782 | 144676 | 11898 | 1490.69 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 1682219 | 239971 | 17468 | 2630.14 | SAT |
Total (6 / 10) | 7323414 | 1003276 | 76644 | 11892.87 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 196430 | 68045 | 6138 | 60.76 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 1086825 | 414552 | 31544 | 1706.54 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 148472 | 45652 | 4094 | 50.17 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 47088 | 14525 | 1533 | 4.92 | 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) | 1478815 | 542774 | 43309 | 1822.39 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 57953 | 13664 | 1492 | 4.71 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 159806 | 46713 | 4094 | 40.09 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 133111 | 39636 | 3881 | 40.59 | 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) | 350870 | 100013 | 9467 | 85.39 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 4799 | 586 | 107 | 0.15 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 175247 | 78051 | 6906 | 54.39 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 240035 | 29406 | 2858 | 119.49 | 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) | 420081 | 108043 | 9871 | 174.03 |
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 | 4941 | 1387 | 218 | 0.08 | UNSAT |
3pipe_3_ooo.cnf | 2533 | 32182 | 37207 | 9741 | 1022 | 1.49 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 176187 | 45604 | 4094 | 19.79 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 528979 | 132745 | 10746 | 123.69 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 1203247 | 266339 | 19963 | 441.95 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 2967689 | 642201 | 45051 | 2143.41 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 5144178 | 869226 | 61432 | 4573.33 | UNSAT |
Total (7 / 15) | 10062428 | 1967243 | 142526 | 7303.74 |
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 | 4851 | 1294 | 195 | 0.06 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 2566 | 25625 | 31246 | 6271 | 763 | 0.67 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 112862 | 18777 | 2043 | 5.23 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 344368 | 53187 | 4604 | 29.27 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 827218 | 112115 | 8858 | 104.67 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 1838790 | 223916 | 16382 | 359.78 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 4122706 | 522299 | 35831 | 1463.44 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 4102594 | 489297 | 32766 | 1544.31 | UNSAT |
Total (8 / 14) | 11384635 | 1427156 | 101442 | 3507.43 |
pipe_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 118040 | 8804672 | 2041781 | 179187 | 14489 | 1550.83 | SAT |
12pipe_bug10.cnf | 118040 | 8804672 | 1276717 | 107923 | 8411 | 879.79 | SAT |
12pipe_bug2.cnf | 118040 | 8804630 | 205868 | 8338 | 1019 | 107.08 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | 2190665 | 190479 | 15616 | 1628.43 | SAT |
12pipe_bug4.cnf | 117504 | 8743027 | 314654 | 16956 | 1803 | 183.21 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | 133813 | 4628 | 517 | 68.38 | SAT |
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 16.20 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | 3379162 | 307076 | 23256 | 2702.17 | SAT |
12pipe_bug8.cnf | 117526 | 8760516 | 13216 | 8 | 3 | 17.13 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | 2011743 | 173676 | 14253 | 1492.22 | SAT |
Total (10 / 10) | 11573096 | 988271 | 79367 | 8645.44 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 428039 | 17243 | 1851 | 148.01 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | 2398134 | 147301 | 12244 | 1149.78 | SAT |
12pipe_bug2_q0.cnf | 138918 | 4678718 | 217007 | 7369 | 891 | 63.58 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 1909595 | 114730 | 9208 | 879.19 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 97883 | 2541 | 346 | 25.54 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 63672 | 1016 | 156 | 17.37 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | 120129 | 3064 | 411 | 33.83 | SAT |
12pipe_bug7_q0.cnf | 138918 | 4678760 | 78655 | 1204 | 188 | 18.82 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 18711 | 31 | 9 | 9.50 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | 3222003 | 230541 | 16569 | 1633.72 | SAT |
Total (10 / 10) | 8553828 | 525040 | 41873 | 3979.34 |
pipe_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 860 | 6693 | 4100 | 1103 | 171 | 0.05 | UNSAT |
03pipe_k.cnf | 2391 | 27405 | 25907 | 5807 | 699 | 0.70 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 96529 | 14985 | 1564 | 4.53 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 238783 | 31337 | 3068 | 18.14 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 355443 | 17882 | 1938 | 16.35 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 1038192 | 94457 | 8189 | 168.30 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 1978886 | 171570 | 13984 | 451.15 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 2096677 | 64588 | 5736 | 192.46 | UNSAT |
10pipe_k.cnf | 67300 | 3601247 | 5357331 | 330423 | 24573 | 1694.50 | UNSAT |
11pipe_k.cnf | 89315 | 5584003 | 8099020 | 387345 | 28984 | 2593.36 | UNSAT |
12pipe_k.cnf | 115915 | 8395649 | 12256656 | 597700 | 40957 | 5327.58 | UNSAT |
13pipe_k.cnf | 147626 | 12295313 | 17633872 | 698760 | 49148 | 7072.74 | UNSAT |
14pipe_k.cnf | 184980 | 17597059 | |||||
Total (12 / 13) | 49181396 | 2415957 | 179011 | 17539.86 |
pipe_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 873 | 6457 | 4353 | 1147 | 181 | 0.05 | UNSAT |
03pipe_q0_k.cnf | 2476 | 25181 | 27026 | 6189 | 762 | 0.65 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 86964 | 14033 | 1531 | 3.45 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 217463 | 29445 | 2871 | 13.02 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 299564 | 17696 | 1915 | 13.25 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 985878 | 97863 | 8189 | 112.56 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 1791921 | 161143 | 12923 | 265.38 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1885808 | 57259 | 5086 | 129.08 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 4694458 | 299766 | 22524 | 894.82 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | 7695989 | 516331 | 35119 | 2079.19 | UNSAT |
12pipe_q0_k.cnf | 136800 | 4216460 | 11918582 | 736900 | 50868 | 3912.18 | UNSAT |
13pipe_q0_k.cnf | 176066 | 5761591 | 18176235 | 961857 | 65533 | 6232.99 | UNSAT |
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (12 / 14) | 47784241 | 2899629 | 207502 | 13656.62 |
vliw_sat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 236038 | 8084666 | 5817966 | 211321 | 16381 | 1791.53 | SAT |
9dlx_vliw_at_b_iq6_bug2.cnf | 235928 | 8076545 | 61322 | 12 | 5 | 17.80 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 235402 | 8060882 | 9316465 | 447897 | 32765 | 4208.38 | SAT |
9dlx_vliw_at_b_iq6_bug4.cnf | 235277 | 8063780 | |||||
9dlx_vliw_at_b_iq6_bug5.cnf | 235923 | 8076534 | |||||
9dlx_vliw_at_b_iq6_bug6.cnf | 235926 | 8076539 | 2089306 | 16099 | 1723 | 188.27 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 10979866 | 758741 | 52815 | 7014.85 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 7639756 | 409589 | 30970 | 3731.78 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | 6096020 | 208489 | 16381 | 1803.27 | SAT |
Total (7 / 9) | 42000701 | 2052148 | 151040 | 18755.88 |
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 | |||||
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 | 1960968 | 5726 | 683 | 197.74 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | |||||
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | |||||
Total (1 / 10) | 1960968 | 5726 | 683 | 197.74 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 4379572 | 9970 | 1022 | 282.66 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 5666172 | 16693 | 1788 | 439.55 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 4456112 | 8753 | 1021 | 278.74 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 3827962 | 4250 | 510 | 163.78 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 5828802 | 32365 | 3069 | 706.62 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 5160152 | 18973 | 2044 | 494.40 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 4384747 | 10920 | 1147 | 315.61 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 5000560 | 6772 | 795 | 229.82 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 4536846 | 11134 | 1149 | 306.45 | SAT |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 5304142 | 17244 | 1851 | 452.05 | SAT |
Total (10 / 10) | 48545067 | 137074 | 14396 | 3669.68 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 2181853 | 344069 | 25588 | 622.60 | UNSAT |
9dlx_vliw_at_b_iq2.cnf | 44095 | 542253 | 6063286 | 821678 | 57340 | 3543.90 | 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) | 8245139 | 1165747 | 82928 | 4166.5 |
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 | 6101129 | 440210 | 32764 | 1817.18 | 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) | 6101129 | 440210 | 32764 | 1817.18 |