Tinisat, using BerkMin's restart policy (550, 1)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 168 (62 SAT + 106 UNSAT)
Time: 739219 seconds / 205.34 hours / 8.56 days
Time on solved instances: 141619 seconds (56598 SAT + 85021 UNSAT)
Instances solved in 10 minutes: 109 (10916 seconds)
Instances solved in 15 minutes: 120 (19147 seconds)
Instances solved in 20 minutes: 126 (25584 seconds)
Instances solved in 30 minutes: 140 (46210 seconds)
Instances solved in 60 minutes: 159 (97019 seconds)
Instances solved in 90 minutes: 166 (128763 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 32 | / | 32 | 58925.57 | ||
engine_unsat_1.0 | 7 | / | 10 | 2580 | ||
fvp-sat.3.0 | 9 | / | 20 | 3481.01 | ||
fvp-unsat.1.0 | 4 | / | 4 | 47.19 | ||
fvp-unsat.2.0 | 22 | / | 22 | 732.14 | ||
fvp-unsat.3.0 | 0 | / | 6 | 0 | ||
liveness_sat_1.0 | 9 | / | 10 | 16483.85 | ||
liveness_unsat_1.0 | 4 | / | 12 | 1447.11 | ||
liveness_unsat_2.0 | 3 | / | 9 | 61.43 | ||
npe-1.0 | 4 | / | 6 | 5159.22 | ||
pipe_ooo_unsat_1.0 | 7 | / | 15 | 8640.24 | ||
pipe_ooo_unsat_1.1 | 8 | / | 14 | 3196.07 | ||
pipe_sat_1.0 | 10 | / | 10 | 7195.5 | ||
pipe_sat_1.1 | 10 | / | 10 | 2280.47 | ||
pipe_unsat_1.0 | 8 | / | 13 | 914.69 | ||
pipe_unsat_1.1 | 11 | / | 14 | 12578.33 | ||
vliw_sat_2.0 | 6 | / | 9 | 7377.07 | ||
vliw_sat_2.1 | 2 | / | 10 | 6179.42 | ||
vliw_sat_4.0 | 10 | / | 10 | 1729.09 | ||
vliw_unsat_2.0 | 1 | / | 9 | 1279.16 | ||
vliw_unsat_3.0 | 0 | / | 2 | 0 | ||
vliw_unsat_4.0 | 1 | / | 4 | 1331.91 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2318668 | 108851 | 197 | 289.06 | UNSAT |
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 2809843 | 122468 | 222 | 366.56 | UNSAT |
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 3097111 | 126192 | 229 | 395.52 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 3515925 | 150442 | 273 | 625.70 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 3725773 | 157339 | 286 | 673.75 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 3815204 | 149246 | 271 | 553.34 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 4386105 | 151889 | 276 | 595.24 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 5020329 | 173569 | 315 | 696.91 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 5242822 | 175835 | 319 | 765.10 | UNSAT |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 5440594 | 172213 | 313 | 784.72 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 6042160 | 187032 | 340 | 893.13 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 6634296 | 189840 | 345 | 992.88 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 7187529 | 198720 | 361 | 1077.03 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 7526825 | 203676 | 370 | 1148.56 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 8535774 | 226204 | 411 | 1343.87 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 8963714 | 218762 | 397 | 1392.12 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 9733687 | 226900 | 412 | 1474.00 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 10156907 | 240332 | 436 | 1662.78 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 10679240 | 241919 | 439 | 1748.60 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 11718832 | 251336 | 456 | 1938.69 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 12477065 | 264226 | 480 | 2067.04 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | 13196823 | 317634 | 577 | 3468.47 | UNSAT |
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 14885491 | 297416 | 540 | 2542.57 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 15923164 | 298564 | 542 | 2753.55 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 16839336 | 305320 | 555 | 2940.58 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | 17251924 | 308256 | 560 | 3119.65 | UNSAT |
1dlx_c_iq59_a.cnf | 623700 | 9457051 | 18622741 | 328255 | 596 | 3373.01 | UNSAT |
1dlx_c_iq60_a.cnf | 651875 | 9927770 | 20506246 | 329885 | 599 | 3627.31 | UNSAT |
1dlx_c_iq61_a.cnf | 673311 | 10435991 | 17877531 | 302664 | 550 | 3341.18 | SAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | 21841464 | 367885 | 668 | 4152.34 | UNSAT |
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 15820295 | 288043 | 523 | 3360.23 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | 25448566 | 375578 | 682 | 4762.08 | UNSAT |
Total (32 / 32) | 337241984 | 7456491 | 13540 | 58925.57 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_6_nd_case1.cnf | 45435 | 610120 | 263671 | 198602 | 361 | 378.37 | UNSAT |
engine_4.cnf | 6944 | 66654 | 47154 | 29534 | 53 | 10.73 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 148795 | 104138 | 189 | 70.31 | UNSAT |
engine_5.cnf | 18788 | 214095 | 885928 | 647104 | 1176 | 2031.37 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 17816 | 11073 | 20 | 6.07 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 56078 | 38598 | 70 | 25.36 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 68490 | 47048 | 85 | 57.79 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | |||||
Total (7 / 10) | 1487932 | 1076097 | 1954 | 2580 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | 1344101 | 81146 | 147 | 50.39 | SAT |
pipe_64_4_bug02.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug03.cnf | 35947 | 992674 | 140446 | 802 | 1 | 3.66 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 154405 | 3978 | 7 | 6.13 | 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 | 8502707 | 875549 | 1591 | 1531.81 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 476257 | 26037 | 47 | 15.52 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 9072032 | 960784 | 1746 | 1803.57 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug12.cnf | 35854 | 1012275 | 982116 | 49142 | 89 | 30.75 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 542561 | 31158 | 56 | 20.59 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 535867 | 33479 | 60 | 18.59 | 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) | 21750492 | 2062075 | 3744 | 3481.01 |
fvp-unsat.1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_mc_ex_bp_f.cnf | 776 | 3725 | 2330 | 678 | 1 | 0.02 | UNSAT |
2dlx_ca_mc_ex_bp_f.cnf | 3250 | 24640 | 21113 | 4734 | 8 | 0.40 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 33722 | 9781 | 17 | 1.28 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 515617 | 102932 | 187 | 45.49 | UNSAT |
Total (4 / 4) | 572782 | 118125 | 213 | 47.19 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 3122 | 1144 | 2 | 0.04 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 2563 | 1204 | 2 | 0.05 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 3350 | 1697 | 3 | 0.08 | UNSAT |
3pipe.cnf | 2468 | 27533 | 21296 | 7015 | 12 | 0.62 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 14604 | 6525 | 11 | 0.59 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 20085 | 9613 | 17 | 1.00 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 28078 | 12519 | 22 | 1.47 | UNSAT |
4pipe.cnf | 5237 | 80213 | 76703 | 22530 | 40 | 4.83 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 52226 | 21755 | 39 | 4.44 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 84098 | 36564 | 66 | 9.82 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 86523 | 32647 | 59 | 8.83 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 84936 | 32616 | 59 | 8.87 | UNSAT |
5pipe.cnf | 9471 | 195452 | 131633 | 14775 | 26 | 4.69 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 102529 | 33681 | 61 | 12.74 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 114348 | 32173 | 58 | 13.36 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 117088 | 35592 | 64 | 15.17 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 249249 | 79676 | 144 | 44.01 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 125309 | 34167 | 62 | 16.01 | UNSAT |
6pipe.cnf | 15800 | 394739 | 527747 | 152240 | 276 | 166.50 | UNSAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 363436 | 89470 | 162 | 80.24 | UNSAT |
7pipe.cnf | 23910 | 751118 | 943430 | 204716 | 372 | 293.65 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 261361 | 60540 | 110 | 45.13 | SAT |
Total (22 / 22) | 3413714 | 922859 | 1667 | 732.14 |
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 | 2651511 | 518889 | 943 | 5147.10 | SAT |
2dlx_cc_ex_bp_f_bug1_liveness.cnf | 171648 | 2614464 | 207128 | 28878 | 52 | 111.42 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 241296 | 34451 | 62 | 147.09 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 253844 | 34608 | 62 | 166.72 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 933264 | 173479 | 315 | 925.62 | SAT |
2dlx_cc_ex_bp_f_bug5_liveness.cnf | 292249 | 4906188 | 1238208 | 239368 | 435 | 1455.82 | SAT |
2dlx_cc_ex_bp_f_bug6_liveness.cnf | 331848 | 5706594 | 1668224 | 322060 | 585 | 2285.58 | SAT |
2dlx_cc_ex_bp_f_bug7_liveness.cnf | 375775 | 6617342 | 1469941 | 274030 | 498 | 2043.72 | SAT |
2dlx_cc_ex_bp_f_bug8_liveness.cnf | 424320 | 7649214 | 2573445 | 487329 | 886 | 4200.78 | SAT |
Total (9 / 10) | 11236861 | 2113092 | 3838 | 16483.85 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 127491 | 63475 | 115 | 35.12 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 847057 | 478528 | 870 | 1376.19 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 111353 | 49449 | 89 | 31.97 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 35255 | 17532 | 31 | 3.83 | 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) | 1121156 | 608984 | 1105 | 1447.11 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 46132 | 18022 | 32 | 4.09 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 129595 | 53463 | 97 | 28.31 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 111024 | 47838 | 86 | 29.03 | 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) | 286751 | 119323 | 215 | 61.43 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 1953 | 583 | 1 | 0.13 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 112633 | 75850 | 137 | 34.15 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 210243 | 45183 | 82 | 85.70 | SAT |
2dlx_cc_mc_ex_bp_f2_no_pe.cnf | 96675 | 1401773 | |||||
9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf | 889302 | 14582074 | 4107572 | 305059 | 554 | 5039.24 | SAT |
9dlx_vliw_at_bp_mc2_no_pe.cnf | 889302 | 14582081 | |||||
Total (4 / 6) | 4432401 | 426675 | 774 | 5159.22 |
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 | 2901 | 1387 | 2 | 0.06 | UNSAT |
3pipe_3_ooo.cnf | 2533 | 32182 | 25731 | 10815 | 19 | 1.20 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 90783 | 34752 | 63 | 9.12 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 397692 | 159523 | 290 | 108.78 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 1184404 | 476230 | 865 | 769.05 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 2596306 | 995730 | 1810 | 2936.25 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 4010484 | 1211900 | 2203 | 4815.78 | UNSAT |
Total (7 / 15) | 8308301 | 2890337 | 5252 | 8640.24 |
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 | 3709 | 1738 | 3 | 0.07 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 2566 | 25625 | 26168 | 10384 | 18 | 0.92 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 106767 | 39513 | 71 | 9.06 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 253476 | 64294 | 116 | 24.70 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 702374 | 166712 | 303 | 128.75 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 1489832 | 316964 | 576 | 407.47 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 3076355 | 570197 | 1036 | 1167.60 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 3256532 | 605010 | 1100 | 1457.50 | UNSAT |
Total (8 / 14) | 8915213 | 1774812 | 3223 | 3196.07 |
pipe_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 118040 | 8804672 | 1466293 | 299973 | 545 | 1425.78 | SAT |
12pipe_bug10.cnf | 118040 | 8804672 | 1148550 | 216803 | 394 | 870.77 | SAT |
12pipe_bug2.cnf | 118040 | 8804630 | 39559 | 1656 | 3 | 21.35 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | 433944 | 66738 | 121 | 260.81 | SAT |
12pipe_bug4.cnf | 117504 | 8743027 | 908204 | 166212 | 302 | 636.96 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | 1049202 | 200194 | 363 | 781.89 | SAT |
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 16.40 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | 1317484 | 254124 | 462 | 1125.55 | SAT |
12pipe_bug8.cnf | 117526 | 8760516 | 78386 | 1143 | 2 | 24.79 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | 1959031 | 379713 | 690 | 2031.20 | SAT |
Total (10 / 10) | 8406130 | 1586556 | 2882 | 7195.5 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 973472 | 119550 | 217 | 417.75 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | 589076 | 63962 | 116 | 225.41 | SAT |
12pipe_bug2_q0.cnf | 138918 | 4678718 | 266398 | 24931 | 45 | 86.28 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 1733663 | 203766 | 370 | 733.18 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 35896 | 1199 | 2 | 11.97 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 356186 | 33621 | 61 | 115.97 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | 189500 | 16562 | 30 | 57.72 | SAT |
12pipe_bug7_q0.cnf | 138918 | 4678760 | 998183 | 111258 | 202 | 394.99 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 71954 | 557 | 1 | 12.82 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | 586350 | 63909 | 116 | 224.38 | SAT |
Total (10 / 10) | 5800678 | 639315 | 1160 | 2280.47 |
pipe_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 860 | 6693 | 2994 | 1113 | 2 | 0.05 | UNSAT |
03pipe_k.cnf | 2391 | 27405 | 19350 | 7110 | 12 | 0.61 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 70106 | 23930 | 43 | 5.08 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 214451 | 66762 | 121 | 33.50 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 245717 | 26290 | 47 | 13.34 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 938595 | 198714 | 361 | 257.50 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 1571429 | 256359 | 466 | 475.13 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 1527757 | 83700 | 152 | 129.48 | 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) | 4590399 | 663978 | 1204 | 914.69 |
pipe_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 873 | 6457 | 2895 | 1080 | 1 | 0.04 | UNSAT |
03pipe_q0_k.cnf | 2476 | 25181 | 21722 | 7675 | 13 | 0.61 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 76130 | 23792 | 43 | 3.99 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 206648 | 64461 | 117 | 22.72 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 214694 | 26435 | 48 | 11.66 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 930099 | 253501 | 460 | 261.81 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 1498109 | 295886 | 537 | 366.38 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1349789 | 83603 | 152 | 107.87 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 4311835 | 738638 | 1342 | 1759.10 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | 6795111 | 1057640 | 1922 | 3309.06 | UNSAT |
12pipe_q0_k.cnf | 136800 | 4216460 | 11272361 | 1586958 | 2885 | 6735.09 | UNSAT |
13pipe_q0_k.cnf | 176066 | 5761591 | |||||
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (11 / 14) | 26679393 | 4139669 | 7520 | 12578.33 |
vliw_sat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 236038 | 8084666 | 8881516 | 636836 | 1157 | 2328.86 | SAT |
9dlx_vliw_at_b_iq6_bug2.cnf | 235928 | 8076545 | 120421 | 59 | 0 | 17.40 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 235402 | 8060882 | 10004874 | 800182 | 1454 | 3133.83 | 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 | 1601227 | 17291 | 31 | 75.78 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 3505732 | 184161 | 334 | 433.51 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 6198568 | 426463 | 775 | 1387.69 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | |||||
Total (6 / 9) | 30312338 | 2064992 | 3751 | 7377.07 |
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 | 1308146 | 914 | 1 | 58.52 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | |||||
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | 21237454 | 1000073 | 1818 | 6120.90 | SAT |
Total (2 / 10) | 22545600 | 1000987 | 1819 | 6179.42 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 6008533 | 28709 | 52 | 226.24 | SAT |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 5961909 | 17544 | 31 | 164.77 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 7170036 | 27212 | 49 | 215.33 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 6517899 | 12549 | 22 | 141.72 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 6071731 | 7940 | 14 | 118.60 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 6815427 | 15753 | 28 | 163.45 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 5721652 | 13802 | 25 | 146.19 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 5515873 | 6303 | 11 | 107.23 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 4143292 | 2530 | 4 | 67.59 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 6820568 | 63077 | 114 | 377.97 | SAT |
Total (10 / 10) | 60746920 | 195419 | 350 | 1729.09 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 2742349 | 810952 | 1474 | 1279.16 | 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) | 2742349 | 810952 | 1474 | 1279.16 |
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 | 6438581 | 697520 | 1268 | 1331.91 | 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) | 6438581 | 697520 | 1268 | 1331.91 |