Tinisat, using restart policy (Luby's, unit=128)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 175 (66 SAT + 109 UNSAT)
Time: 685605 seconds / 190.45 hours / 7.94 days
Time on solved instances: 138405 seconds (46702 SAT + 91703 UNSAT)
Instances solved in 10 minutes: 116 (12109 seconds)
Instances solved in 15 minutes: 126 (19405 seconds)
Instances solved in 20 minutes: 137 (30891 seconds)
Instances solved in 30 minutes: 147 (45656 seconds)
Instances solved in 60 minutes: 168 (104326 seconds)
Instances solved in 90 minutes: 172 (121205 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 32 | / | 32 | 60322.6 | ||
engine_unsat_1.0 | 7 | / | 10 | 1922.5 | ||
fvp-sat.3.0 | 14 | / | 20 | 8805.67 | ||
fvp-unsat.1.0 | 4 | / | 4 | 47.19 | ||
fvp-unsat.2.0 | 22 | / | 22 | 578.35 | ||
fvp-unsat.3.0 | 0 | / | 6 | 0 | ||
liveness_sat_1.0 | 6 | / | 10 | 6833.58 | ||
liveness_unsat_1.0 | 4 | / | 12 | 1255.53 | ||
liveness_unsat_2.0 | 3 | / | 9 | 69.72 | ||
npe-1.0 | 4 | / | 6 | 1159.27 | ||
pipe_ooo_unsat_1.0 | 7 | / | 15 | 4857.74 | ||
pipe_ooo_unsat_1.1 | 8 | / | 14 | 3092.18 | ||
pipe_sat_1.0 | 9 | / | 10 | 2940.12 | ||
pipe_sat_1.1 | 10 | / | 10 | 3362.53 | ||
pipe_unsat_1.0 | 9 | / | 13 | 3550.43 | ||
pipe_unsat_1.1 | 11 | / | 14 | 10806.68 | ||
vliw_sat_2.0 | 9 | / | 9 | 12567.15 | ||
vliw_sat_2.1 | 2 | / | 10 | 3277.34 | ||
vliw_sat_4.0 | 10 | / | 10 | 1767.56 | ||
vliw_unsat_2.0 | 2 | / | 9 | 4220.53 | ||
vliw_unsat_3.0 | 1 | / | 2 | 5968.88 | ||
vliw_unsat_4.0 | 1 | / | 4 | 999.38 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 5480680 | 176442 | 380 | 807.66 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 6390635 | 201436 | 426 | 990.27 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 6807771 | 187535 | 381 | 985.60 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 7093508 | 219769 | 473 | 1176.23 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 7227595 | 210006 | 444 | 1146.54 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 8570323 | 223146 | 475 | 1348.39 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 9003353 | 236110 | 507 | 1476.28 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 9773809 | 247585 | 509 | 1634.06 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 10106169 | 227957 | 494 | 1585.75 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 11092376 | 267534 | 510 | 1889.79 | UNSAT |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2557742 | 116964 | 254 | 328.40 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 11995136 | 264857 | 510 | 2015.09 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 13454811 | 302449 | 540 | 2246.03 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | 13337451 | 344604 | 637 | 3569.21 | UNSAT |
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 15413819 | 326084 | 601 | 2786.54 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 16779586 | 332308 | 618 | 2990.72 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 16450735 | 306350 | 548 | 2821.54 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | 18709678 | 328946 | 604 | 3291.68 | UNSAT |
1dlx_c_iq59_a.cnf | 623700 | 9457051 | 19193164 | 341184 | 636 | 3397.98 | UNSAT |
1dlx_c_iq60_a.cnf | 651875 | 9927770 | 20827360 | 364869 | 681 | 3679.15 | UNSAT |
1dlx_c_iq61_a.cnf | 673311 | 10435991 | 14155406 | 280416 | 510 | 2798.52 | SAT |
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 2635280 | 117361 | 254 | 338.94 | UNSAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | 23402779 | 387989 | 737 | 4373.04 | UNSAT |
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 14748025 | 281322 | 510 | 3183.01 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | 26451371 | 401899 | 764 | 5002.04 | UNSAT |
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 3287725 | 136230 | 276 | 423.47 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 3389721 | 157006 | 324 | 644.02 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 3454764 | 160763 | 338 | 690.12 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 4076189 | 142922 | 293 | 551.81 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 4359148 | 154558 | 317 | 614.59 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 4900693 | 166982 | 355 | 726.21 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 5572593 | 183963 | 381 | 809.92 | UNSAT |
Total (32 / 32) | 340699395 | 7797546 | 15287 | 60322.6 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_4.cnf | 6944 | 66654 | 47607 | 30416 | 86 | 10.90 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 144942 | 103622 | 252 | 70.46 | UNSAT |
engine_5.cnf | 18788 | 214095 | 724535 | 531231 | 1018 | 1351.08 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 17134 | 10522 | 33 | 5.73 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 53769 | 37674 | 107 | 24.96 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 70249 | 47994 | 125 | 59.01 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | |||||
engine_6_nd_case1.cnf | 45435 | 610120 | 277413 | 208837 | 443 | 400.36 | UNSAT |
Total (7 / 10) | 1335649 | 970296 | 2064 | 1922.5 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | 1367726 | 79009 | 189 | 49.17 | SAT |
pipe_64_4_bug02.cnf | 35853 | 1012271 | 9886808 | 931635 | 1533 | 1504.09 | SAT |
pipe_64_4_bug03.cnf | 35947 | 992674 | 260693 | 2115 | 10 | 4.71 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 323493 | 4328 | 16 | 7.01 | SAT |
pipe_64_4_bug05.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug06.cnf | 35853 | 1012271 | 7616633 | 747270 | 1243 | 1015.00 | SAT |
pipe_64_4_bug07.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug08.cnf | 35622 | 1003074 | 1557691 | 122471 | 254 | 71.78 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 1213432 | 77324 | 188 | 47.26 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 557145 | 19650 | 61 | 12.83 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug12.cnf | 35854 | 1012275 | 1985039 | 119650 | 254 | 78.38 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 1657393 | 118470 | 254 | 71.81 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 3286147 | 273819 | 510 | 215.26 | SAT |
pipe_64_4_bug15.cnf | 35853 | 1012271 | 16017392 | 1987240 | 3067 | 5678.49 | SAT |
pipe_64_4_bug16.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug17.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug18.cnf | 35853 | 1012271 | 700779 | 22300 | 62 | 16.44 | SAT |
pipe_64_4_bug19.cnf | 35852 | 1012266 | |||||
pipe_64_4_bug20.cnf | 35853 | 1012271 | 1178879 | 50837 | 126 | 33.44 | SAT |
Total (14 / 20) | 47609250 | 4556118 | 7767 | 8805.67 |
fvp-unsat.1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_mc_ex_bp_f.cnf | 776 | 3725 | 2435 | 782 | 5 | 0.03 | UNSAT |
2dlx_ca_mc_ex_bp_f.cnf | 3250 | 24640 | 20072 | 4977 | 20 | 0.44 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 30286 | 8236 | 30 | 0.97 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 507070 | 102071 | 251 | 45.75 | UNSAT |
Total (4 / 4) | 559863 | 116066 | 306 | 47.19 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 3857 | 1629 | 7 | 0.06 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 3064 | 1482 | 6 | 0.06 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 3427 | 1438 | 6 | 0.07 | UNSAT |
3pipe.cnf | 2468 | 27533 | 22555 | 8395 | 30 | 0.79 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 12643 | 5719 | 22 | 0.49 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 22711 | 10195 | 30 | 1.09 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 25832 | 11886 | 38 | 1.38 | UNSAT |
4pipe.cnf | 5237 | 80213 | 95083 | 36316 | 100 | 9.46 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 58427 | 22734 | 62 | 4.85 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 85471 | 35660 | 99 | 9.36 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 114346 | 48876 | 125 | 15.47 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 129720 | 55457 | 126 | 18.83 | UNSAT |
5pipe.cnf | 9471 | 195452 | 118848 | 14544 | 47 | 4.27 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 112975 | 39097 | 110 | 16.61 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 118579 | 35036 | 95 | 14.79 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 124060 | 36173 | 100 | 16.66 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 244622 | 76249 | 188 | 42.28 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 136820 | 33062 | 93 | 16.72 | UNSAT |
6pipe.cnf | 15800 | 394739 | 438788 | 96588 | 238 | 85.24 | UNSAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 351936 | 87736 | 213 | 77.59 | UNSAT |
7pipe.cnf | 23910 | 751118 | 896282 | 165919 | 349 | 203.40 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 286300 | 53217 | 126 | 38.88 | SAT |
Total (22 / 22) | 3406346 | 877408 | 2210 | 578.35 |
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 | 1912130 | 427199 | 772 | 2675.04 | SAT |
2dlx_cc_ex_bp_f_bug6_liveness.cnf | 331848 | 5706594 | 2125949 | 472048 | 891 | 3312.68 | 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 | 63619 | 7157 | 28 | 37.68 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 78092 | 7405 | 29 | 46.22 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 182647 | 24755 | 64 | 131.38 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 694415 | 122502 | 254 | 630.58 | SAT |
Total (6 / 10) | 5056852 | 1061066 | 2038 | 6833.58 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 132496 | 65219 | 156 | 36.88 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 788218 | 442128 | 821 | 1183.07 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 106447 | 45673 | 125 | 31.56 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 37509 | 18123 | 60 | 4.02 | 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) | 1064670 | 571143 | 1162 | 1255.53 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 45538 | 16799 | 58 | 3.48 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 147255 | 61657 | 143 | 35.00 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 116079 | 51930 | 126 | 31.24 | 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) | 308872 | 130386 | 327 | 69.72 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 7945 | 3176 | 14 | 0.35 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 109661 | 72341 | 177 | 31.62 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 311848 | 74677 | 186 | 148.97 | SAT |
2dlx_cc_mc_ex_bp_f2_no_pe.cnf | 96675 | 1401773 | |||||
9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf | 889302 | 14582074 | 1198127 | 66054 | 157 | 978.33 | SAT |
9dlx_vliw_at_bp_mc2_no_pe.cnf | 889302 | 14582081 | |||||
Total (4 / 6) | 1627581 | 216248 | 534 | 1159.27 |
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 | 3088 | 1403 | 6 | 0.06 | UNSAT |
3pipe_3_ooo.cnf | 2533 | 32182 | 25686 | 11255 | 36 | 1.20 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 126406 | 54762 | 126 | 16.92 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 322758 | 118526 | 254 | 69.64 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 907121 | 323205 | 588 | 384.04 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 2159662 | 740360 | 1227 | 1628.31 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 3430839 | 924107 | 1533 | 2757.57 | UNSAT |
Total (7 / 15) | 6975560 | 2173618 | 3770 | 4857.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 | 3121 | 1345 | 6 | 0.05 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 2566 | 25625 | 28637 | 11393 | 37 | 1.05 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 120220 | 46246 | 125 | 11.70 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 268808 | 67624 | 158 | 26.66 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 668259 | 161847 | 343 | 122.58 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 1428187 | 277822 | 510 | 336.57 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 3017789 | 594329 | 1022 | 1238.33 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 3193018 | 572558 | 1021 | 1355.24 | UNSAT |
Total (8 / 14) | 8728039 | 1733164 | 3222 | 3092.18 |
pipe_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 118040 | 8804672 | 243516 | 34194 | 93 | 136.14 | SAT |
12pipe_bug10.cnf | 118040 | 8804672 | 1116328 | 213032 | 445 | 937.72 | SAT |
12pipe_bug2.cnf | 118040 | 8804630 | 63494 | 3173 | 14 | 28.50 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | |||||
12pipe_bug4.cnf | 117504 | 8743027 | 158975 | 16025 | 54 | 77.62 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | 766556 | 137516 | 282 | 503.76 | SAT |
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 16.21 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | 1071996 | 196803 | 412 | 819.42 | SAT |
12pipe_bug8.cnf | 117526 | 8760516 | 64660 | 755 | 4 | 23.98 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | 652980 | 107247 | 253 | 396.77 | SAT |
Total (9 / 10) | 4143982 | 708745 | 1557 | 2940.12 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 2028352 | 309917 | 561 | 1030.97 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | 1218029 | 139005 | 284 | 492.79 | SAT |
12pipe_bug2_q0.cnf | 138918 | 4678718 | 289029 | 24548 | 62 | 86.47 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 1342794 | 161382 | 340 | 547.54 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 68056 | 4136 | 15 | 20.81 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 1567504 | 197153 | 412 | 671.92 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | 293072 | 30376 | 86 | 104.98 | SAT |
12pipe_bug7_q0.cnf | 138918 | 4678760 | 243676 | 17015 | 59 | 70.60 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 59886 | 135 | 1 | 10.77 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | 872019 | 89120 | 219 | 325.68 | SAT |
Total (10 / 10) | 7982417 | 972787 | 2039 | 3362.53 |
pipe_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 860 | 6693 | 3515 | 1273 | 6 | 0.05 | UNSAT |
03pipe_k.cnf | 2391 | 27405 | 20549 | 7669 | 29 | 0.68 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 71621 | 23708 | 62 | 5.39 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 189990 | 51692 | 126 | 23.90 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 267830 | 26860 | 74 | 14.06 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 1001329 | 233753 | 507 | 356.83 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 1689215 | 301246 | 537 | 599.50 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 1600611 | 84588 | 203 | 134.44 | UNSAT |
10pipe_k.cnf | 67300 | 3601247 | 4659306 | 657225 | 1032 | 2415.58 | UNSAT |
11pipe_k.cnf | 89315 | 5584003 | |||||
12pipe_k.cnf | 115915 | 8395649 | |||||
13pipe_k.cnf | 147626 | 12295313 | |||||
14pipe_k.cnf | 184980 | 17597059 | |||||
Total (9 / 13) | 9503966 | 1388014 | 2576 | 3550.43 |
pipe_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 873 | 6457 | 2766 | 1130 | 6 | 0.04 | UNSAT |
03pipe_q0_k.cnf | 2476 | 25181 | 19705 | 8067 | 29 | 0.60 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 77546 | 28004 | 77 | 5.13 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 197905 | 54322 | 126 | 18.64 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 226024 | 24889 | 65 | 11.67 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 745383 | 147124 | 309 | 112.55 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 1391718 | 253165 | 509 | 282.99 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1443389 | 79630 | 189 | 107.67 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 4271891 | 697837 | 1146 | 1644.11 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | 6902447 | 1048086 | 1777 | 3070.86 | UNSAT |
12pipe_q0_k.cnf | 136800 | 4216460 | 10744318 | 1422530 | 2046 | 5552.42 | UNSAT |
13pipe_q0_k.cnf | 176066 | 5761591 | |||||
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (11 / 14) | 26023092 | 3764784 | 6279 | 10806.68 |
vliw_sat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 236038 | 8084666 | 5835150 | 342980 | 636 | 1042.39 | SAT |
9dlx_vliw_at_b_iq6_bug2.cnf | 235928 | 8076545 | 120421 | 59 | 0 | 17.36 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 235402 | 8060882 | 10266825 | 867951 | 1467 | 3250.74 | SAT |
9dlx_vliw_at_b_iq6_bug4.cnf | 235277 | 8063780 | 8630599 | 566257 | 1021 | 1842.14 | SAT |
9dlx_vliw_at_b_iq6_bug5.cnf | 235923 | 8076534 | 11019376 | 998888 | 1659 | 3824.81 | SAT |
9dlx_vliw_at_b_iq6_bug6.cnf | 235926 | 8076539 | 1344436 | 13441 | 45 | 73.16 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 4088978 | 183497 | 381 | 427.91 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 3464470 | 67496 | 157 | 221.58 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | 8451719 | 583252 | 1021 | 1867.06 | SAT |
Total (9 / 9) | 53221974 | 3623821 | 6387 | 12567.15 |
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 | 2920770 | 11004 | 35 | 127.72 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | |||||
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | 19128772 | 597567 | 1022 | 3149.62 | SAT |
Total (2 / 10) | 22049542 | 608571 | 1057 | 3277.34 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 6697846 | 44248 | 124 | 315.10 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 6444768 | 32209 | 92 | 260.42 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 6815702 | 18162 | 60 | 175.85 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 5239341 | 6855 | 28 | 106.37 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 5543743 | 18213 | 60 | 176.89 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 4558736 | 12724 | 43 | 145.86 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 4668768 | 4478 | 17 | 91.04 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 6788396 | 13698 | 45 | 156.65 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 4349008 | 8749 | 30 | 120.21 | SAT |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 5203392 | 25796 | 69 | 219.17 | SAT |
Total (10 / 10) | 56309700 | 185132 | 568 | 1767.56 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 2602122 | 720410 | 1179 | 882.00 | UNSAT |
9dlx_vliw_at_b_iq2.cnf | 44095 | 542253 | 6014048 | 1458350 | 2104 | 3338.53 | 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) | 8616170 | 2178760 | 3283 | 4220.53 |
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 | 40328392 | 1800375 | 2711 | 5968.88 | UNSAT |
Total (1 / 2) | 40328392 | 1800375 | 2711 | 5968.88 |
vliw_unsat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_C1.cnf | 96177 | 1814189 | 5391451 | 607258 | 1022 | 999.38 | 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) | 5391451 | 607258 | 1022 | 999.38 |