Tinisat, using Chaff II's restart policy (700, 1)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 166 (58 SAT + 108 UNSAT)
Time: 733654 seconds / 203.79 hours / 8.49 days
Time on solved instances: 121654 seconds (30865 SAT + 90789 UNSAT)
Instances solved in 10 minutes: 110 (10774 seconds)
Instances solved in 15 minutes: 120 (18341 seconds)
Instances solved in 20 minutes: 130 (28763 seconds)
Instances solved in 30 minutes: 143 (47946 seconds)
Instances solved in 60 minutes: 161 (97148 seconds)
Instances solved in 90 minutes: 165 (116040 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 32 | / | 32 | 58353.98 | ||
engine_unsat_1.0 | 8 | / | 10 | 2672.9 | ||
fvp-sat.3.0 | 9 | / | 20 | 3883.5 | ||
fvp-unsat.1.0 | 4 | / | 4 | 40.56 | ||
fvp-unsat.2.0 | 22 | / | 22 | 692.78 | ||
fvp-unsat.3.0 | 0 | / | 6 | 0 | ||
liveness_sat_1.0 | 8 | / | 10 | 6439.55 | ||
liveness_unsat_1.0 | 4 | / | 12 | 1073.9 | ||
liveness_unsat_2.0 | 3 | / | 9 | 66.64 | ||
npe-1.0 | 3 | / | 6 | 76.39 | ||
pipe_ooo_unsat_1.0 | 7 | / | 15 | 7714.17 | ||
pipe_ooo_unsat_1.1 | 8 | / | 14 | 4690.12 | ||
pipe_sat_1.0 | 9 | / | 10 | 6442.24 | ||
pipe_sat_1.1 | 10 | / | 10 | 2226.47 | ||
pipe_unsat_1.0 | 9 | / | 13 | 4456.15 | ||
pipe_unsat_1.1 | 11 | / | 14 | 10087.59 | ||
vliw_sat_2.0 | 5 | / | 9 | 3168.65 | ||
vliw_sat_2.1 | 1 | / | 10 | 81.14 | ||
vliw_sat_4.0 | 10 | / | 10 | 1515.51 | ||
vliw_unsat_2.0 | 1 | / | 9 | 1166.21 | ||
vliw_unsat_3.0 | 1 | / | 2 | 5613.93 | ||
vliw_unsat_4.0 | 1 | / | 4 | 1191.83 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2436900 | 113570 | 162 | 313.71 | UNSAT |
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 787418 | 58195 | 83 | 145.64 | UNSAT |
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 2880572 | 125675 | 179 | 374.29 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 3376045 | 143860 | 205 | 592.40 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 3810543 | 150536 | 215 | 668.32 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 3927169 | 153737 | 219 | 554.84 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 4540508 | 155608 | 222 | 617.80 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 4734637 | 151884 | 216 | 638.65 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 5211523 | 177079 | 252 | 760.29 | UNSAT |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 5795598 | 178170 | 254 | 836.67 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 5781822 | 176894 | 252 | 859.84 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 6504088 | 192181 | 274 | 985.74 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 7223783 | 192299 | 274 | 1059.12 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 7283428 | 195918 | 279 | 1138.11 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 8230328 | 224153 | 320 | 1294.13 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 8938633 | 225679 | 322 | 1392.16 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 9698593 | 231158 | 330 | 1540.93 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 10173141 | 238332 | 340 | 1627.31 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 11066983 | 241350 | 344 | 1770.13 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 11948499 | 266072 | 380 | 2011.08 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 12685195 | 270235 | 386 | 2131.05 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | 12133248 | 300328 | 429 | 3133.99 | UNSAT |
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 14590283 | 285259 | 407 | 2460.42 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 15976492 | 310483 | 443 | 2803.06 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 17079547 | 322196 | 460 | 2914.25 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | 18234253 | 321503 | 459 | 3135.75 | UNSAT |
1dlx_c_iq59_a.cnf | 623700 | 9457051 | 19123644 | 330379 | 471 | 3326.41 | UNSAT |
1dlx_c_iq60_a.cnf | 651875 | 9927770 | 18722823 | 336730 | 481 | 3507.88 | UNSAT |
1dlx_c_iq61_a.cnf | 673311 | 10435991 | 18185061 | 328606 | 469 | 3511.03 | SAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | 22456517 | 363880 | 519 | 4133.83 | UNSAT |
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 15940606 | 291104 | 415 | 3404.19 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | 24997789 | 376089 | 537 | 4710.96 | UNSAT |
Total (32 / 32) | 334475669 | 7429142 | 10598 | 58353.98 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_6_nd_case1.cnf | 45435 | 610120 | 254331 | 190991 | 272 | 347.68 | UNSAT |
engine_4.cnf | 6944 | 66654 | 48616 | 30205 | 43 | 10.90 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 150361 | 105945 | 151 | 71.54 | UNSAT |
engine_5.cnf | 18788 | 214095 | 871109 | 645774 | 922 | 1998.05 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 19487 | 11994 | 17 | 6.75 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 53688 | 37267 | 53 | 24.53 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 66825 | 46226 | 66 | 57.87 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | 220229 | 119028 | 170 | 155.58 | SAT |
Total (8 / 10) | 1684646 | 1187430 | 1694 | 2672.9 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | 7579493 | 792333 | 1131 | 1258.94 | SAT |
pipe_64_4_bug02.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug03.cnf | 35947 | 992674 | 145245 | 2156 | 3 | 4.81 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 137093 | 3979 | 5 | 5.79 | SAT |
pipe_64_4_bug05.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug06.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug07.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug08.cnf | 35622 | 1003074 | 3236483 | 255312 | 364 | 210.37 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 635739 | 31990 | 45 | 19.91 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 631341 | 31170 | 44 | 19.76 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug12.cnf | 35854 | 1012275 | 1286768 | 83952 | 119 | 49.59 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 8264990 | 797966 | 1139 | 1297.44 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 8135392 | 681517 | 973 | 1016.89 | SAT |
pipe_64_4_bug15.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug16.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug17.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug18.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug19.cnf | 35852 | 1012266 | |||||
pipe_64_4_bug20.cnf | 35853 | 1012271 | |||||
Total (9 / 20) | 30052544 | 2680375 | 3823 | 3883.5 |
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 | 22244 | 5854 | 8 | 0.50 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 33056 | 8800 | 12 | 1.04 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 502917 | 96160 | 137 | 39.00 | UNSAT |
Total (4 / 4) | 560501 | 111484 | 157 | 40.56 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 3796 | 1582 | 2 | 0.06 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 2538 | 1092 | 1 | 0.05 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 2965 | 1382 | 1 | 0.06 | UNSAT |
3pipe.cnf | 2468 | 27533 | 21556 | 7420 | 10 | 0.68 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 13447 | 6217 | 8 | 0.54 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 23016 | 10276 | 14 | 1.10 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 23697 | 10496 | 14 | 1.13 | UNSAT |
4pipe.cnf | 5237 | 80213 | 80413 | 27604 | 39 | 6.25 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 50994 | 20692 | 29 | 4.00 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 66213 | 25136 | 35 | 5.78 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 96707 | 39248 | 56 | 11.31 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 82481 | 30099 | 42 | 8.21 | UNSAT |
5pipe.cnf | 9471 | 195452 | 111318 | 14845 | 21 | 4.43 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 99828 | 33316 | 47 | 13.04 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 106831 | 33954 | 48 | 13.17 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 120891 | 35385 | 50 | 15.34 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 225716 | 70250 | 100 | 35.88 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 118092 | 34534 | 49 | 15.99 | UNSAT |
6pipe.cnf | 15800 | 394739 | 557028 | 170899 | 244 | 205.86 | UNSAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 334401 | 88926 | 127 | 75.38 | UNSAT |
7pipe.cnf | 23910 | 751118 | 916258 | 190391 | 271 | 269.15 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 82254 | 9840 | 14 | 5.37 | SAT |
Total (22 / 22) | 3140440 | 863584 | 1222 | 692.78 |
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_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 | 172901 | 21750 | 31 | 90.09 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 334248 | 54978 | 78 | 230.02 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 81173 | 8398 | 11 | 53.37 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 523409 | 83582 | 119 | 421.76 | SAT |
2dlx_cc_ex_bp_f_bug5_liveness.cnf | 292249 | 4906188 | 1211741 | 238798 | 341 | 1457.76 | SAT |
2dlx_cc_ex_bp_f_bug6_liveness.cnf | 331848 | 5706594 | 1108012 | 204567 | 292 | 1290.18 | SAT |
2dlx_cc_ex_bp_f_bug7_liveness.cnf | 375775 | 6617342 | 805585 | 133774 | 191 | 897.81 | SAT |
2dlx_cc_ex_bp_f_bug8_liveness.cnf | 424320 | 7649214 | 1414355 | 252591 | 360 | 1998.56 | SAT |
Total (8 / 10) | 5651424 | 998438 | 1423 | 6439.55 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 116734 | 55558 | 79 | 30.17 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 721686 | 396609 | 566 | 1006.23 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 112336 | 49572 | 70 | 33.27 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 37325 | 18705 | 26 | 4.23 | 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) | 988081 | 520444 | 741 | 1073.9 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 41253 | 15175 | 21 | 3.27 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 140600 | 59695 | 85 | 34.14 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 111522 | 49117 | 70 | 29.23 | 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) | 293375 | 123987 | 176 | 66.64 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 9989 | 4858 | 6 | 0.61 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 129358 | 87406 | 124 | 44.40 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 108236 | 16987 | 24 | 31.38 | 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) | 247583 | 109251 | 154 | 76.39 |
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 | 2919 | 1363 | 1 | 0.06 | UNSAT |
3pipe_3_ooo.cnf | 2533 | 32182 | 24073 | 10706 | 15 | 1.11 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 125760 | 53786 | 76 | 16.01 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 386929 | 152121 | 217 | 101.60 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 929921 | 339015 | 484 | 409.63 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 2442237 | 883766 | 1262 | 2301.41 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 4161506 | 1235589 | 1765 | 4884.35 | UNSAT |
Total (7 / 15) | 8073345 | 2676346 | 3820 | 7714.17 |
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 | 3571 | 1646 | 2 | 0.06 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 2566 | 25625 | 22679 | 8772 | 12 | 0.73 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 89174 | 26828 | 38 | 5.23 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 300747 | 75653 | 108 | 31.54 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 710771 | 175184 | 250 | 137.55 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 1545055 | 341737 | 488 | 459.57 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 3864035 | 929837 | 1328 | 2536.14 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 3108840 | 615170 | 878 | 1519.30 | UNSAT |
Total (8 / 14) | 9644872 | 2174827 | 3104 | 4690.12 |
pipe_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 118040 | 8804672 | 1289310 | 234685 | 335 | 959.39 | SAT |
12pipe_bug10.cnf | 118040 | 8804672 | 1466930 | 304288 | 434 | 1497.09 | SAT |
12pipe_bug2.cnf | 118040 | 8804630 | 573976 | 89276 | 127 | 351.43 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | 1140313 | 227514 | 325 | 917.48 | SAT |
12pipe_bug4.cnf | 117504 | 8743027 | 121342 | 13321 | 19 | 61.49 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | 1971373 | 411474 | 587 | 2370.08 | SAT |
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 17.33 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | |||||
12pipe_bug8.cnf | 117526 | 8760516 | 71375 | 1419 | 2 | 23.36 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | 388012 | 61886 | 88 | 244.59 | SAT |
Total (9 / 10) | 7028108 | 1343863 | 1917 | 6442.24 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 197657 | 15457 | 22 | 52.93 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | 1698281 | 223333 | 319 | 784.70 | SAT |
12pipe_bug2_q0.cnf | 138918 | 4678718 | 183812 | 15119 | 21 | 49.94 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 429678 | 46954 | 67 | 157.73 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 567865 | 63069 | 90 | 217.55 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 229164 | 20063 | 28 | 68.73 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | 680056 | 70378 | 100 | 243.68 | SAT |
12pipe_bug7_q0.cnf | 138918 | 4678760 | 1316978 | 159027 | 227 | 540.73 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 75137 | 710 | 1 | 14.37 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | 310653 | 28037 | 40 | 96.11 | SAT |
Total (10 / 10) | 5689281 | 642147 | 915 | 2226.47 |
pipe_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 860 | 6693 | 2940 | 1056 | 1 | 0.04 | UNSAT |
03pipe_k.cnf | 2391 | 27405 | 19576 | 7382 | 10 | 0.63 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 73936 | 25956 | 37 | 5.82 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 241222 | 84355 | 120 | 51.45 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 270465 | 25467 | 36 | 13.43 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 827454 | 162835 | 232 | 184.18 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 1663668 | 356128 | 508 | 896.60 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 1559987 | 86539 | 123 | 135.13 | UNSAT |
10pipe_k.cnf | 67300 | 3601247 | 4874691 | 711763 | 1016 | 3168.87 | UNSAT |
11pipe_k.cnf | 89315 | 5584003 | |||||
12pipe_k.cnf | 115915 | 8395649 | |||||
13pipe_k.cnf | 147626 | 12295313 | |||||
14pipe_k.cnf | 184980 | 17597059 | |||||
Total (9 / 13) | 9533939 | 1461481 | 2083 | 4456.15 |
pipe_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 873 | 6457 | 2869 | 1072 | 1 | 0.04 | UNSAT |
03pipe_q0_k.cnf | 2476 | 25181 | 20502 | 7599 | 10 | 0.62 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 62888 | 19015 | 27 | 3.07 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 173742 | 46378 | 66 | 14.19 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 218121 | 25766 | 36 | 11.19 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 919959 | 226533 | 323 | 205.66 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 1592340 | 313278 | 447 | 388.19 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1324988 | 88604 | 126 | 111.31 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 4201247 | 701859 | 1002 | 1700.73 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | 6519799 | 871783 | 1245 | 2489.67 | UNSAT |
12pipe_q0_k.cnf | 136800 | 4216460 | 10454095 | 1360768 | 1943 | 5162.92 | UNSAT |
13pipe_q0_k.cnf | 176066 | 5761591 | |||||
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (11 / 14) | 25490550 | 3662655 | 5226 | 10087.59 |
vliw_sat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 236038 | 8084666 | 7109356 | 466175 | 665 | 1537.20 | SAT |
9dlx_vliw_at_b_iq6_bug2.cnf | 235928 | 8076545 | 120421 | 59 | 0 | 17.50 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 235402 | 8060882 | |||||
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 | 342521 | 752 | 1 | 26.28 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 5419769 | 370034 | 528 | 981.07 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 3985621 | 220345 | 314 | 606.60 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | |||||
Total (5 / 9) | 16977688 | 1057365 | 1508 | 3168.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 | |||||
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 | 1739031 | 3861 | 5 | 81.14 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | |||||
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | |||||
Total (1 / 10) | 1739031 | 3861 | 5 | 81.14 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 6632415 | 32496 | 46 | 232.44 | SAT |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 6171513 | 29374 | 41 | 202.01 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 6011611 | 29036 | 41 | 204.61 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 5959151 | 10048 | 14 | 123.84 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 3645439 | 1247 | 1 | 51.85 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 4831020 | 9197 | 13 | 117.25 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 7025346 | 24177 | 34 | 194.54 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 5757262 | 5193 | 7 | 85.59 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 6315851 | 15562 | 22 | 159.97 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 5496425 | 14469 | 20 | 143.41 | SAT |
Total (10 / 10) | 57846033 | 170799 | 239 | 1515.51 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 2662057 | 786688 | 1123 | 1166.21 | UNSAT |
9dlx_vliw_at_b_iq2.cnf | 44095 | 542253 | |||||
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 (1 / 9) | 2662057 | 786688 | 1123 | 1166.21 |
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 | 41400934 | 1695261 | 2421 | 5613.93 | UNSAT |
Total (1 / 2) | 41400934 | 1695261 | 2421 | 5613.93 |
vliw_unsat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_C1.cnf | 96177 | 1814189 | 5758362 | 656729 | 938 | 1191.83 | 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) | 5758362 | 656729 | 938 | 1191.83 |