Tinisat, using restart policy (Luby's, unit=16)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 176 (66 SAT + 110 UNSAT)
Time: 691663 seconds / 192.13 hours / 8.01 days
Time on solved instances: 151663 seconds (54142 SAT + 97521 UNSAT)
Instances solved in 10 minutes: 114 (12304 seconds)
Instances solved in 15 minutes: 125 (20741 seconds)
Instances solved in 20 minutes: 138 (34408 seconds)
Instances solved in 30 minutes: 147 (48022 seconds)
Instances solved in 60 minutes: 165 (96032 seconds)
Instances solved in 90 minutes: 172 (127018 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 32 | / | 32 | 68863.58 | ||
engine_unsat_1.0 | 7 | / | 10 | 2540.78 | ||
fvp-sat.3.0 | 15 | / | 20 | 20069.12 | ||
fvp-unsat.1.0 | 4 | / | 4 | 50 | ||
fvp-unsat.2.0 | 22 | / | 22 | 533.87 | ||
fvp-unsat.3.0 | 0 | / | 6 | 0 | ||
liveness_sat_1.0 | 6 | / | 10 | 3426.2 | ||
liveness_unsat_1.0 | 4 | / | 12 | 1060.35 | ||
liveness_unsat_2.0 | 3 | / | 9 | 67.23 | ||
npe-1.0 | 4 | / | 6 | 1198.43 | ||
pipe_ooo_unsat_1.0 | 7 | / | 15 | 5320.2 | ||
pipe_ooo_unsat_1.1 | 8 | / | 14 | 2641.54 | ||
pipe_sat_1.0 | 10 | / | 10 | 6714.73 | ||
pipe_sat_1.1 | 10 | / | 10 | 2643.03 | ||
pipe_unsat_1.0 | 10 | / | 13 | 5842.17 | ||
pipe_unsat_1.1 | 11 | / | 14 | 6315.47 | ||
vliw_sat_2.0 | 8 | / | 9 | 10554.81 | ||
vliw_sat_2.1 | 1 | / | 10 | 135.73 | ||
vliw_sat_4.0 | 10 | / | 10 | 2123.31 | ||
vliw_unsat_2.0 | 3 | / | 9 | 10266.26 | ||
vliw_unsat_3.0 | 0 | / | 2 | 0 | ||
vliw_unsat_4.0 | 1 | / | 4 | 1296.1 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 5923105 | 154755 | 2044 | 883.92 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 6524116 | 179908 | 2046 | 1040.44 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 6960585 | 200574 | 2393 | 1184.68 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 7917846 | 206038 | 2489 | 1354.50 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 8446514 | 203752 | 2428 | 1428.01 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 8601214 | 201504 | 2412 | 1476.73 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 9397671 | 224427 | 2691 | 1664.11 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 10603326 | 237500 | 2905 | 1909.11 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 10896437 | 245674 | 3055 | 2015.26 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 11331929 | 237476 | 2905 | 2092.86 | UNSAT |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2620140 | 109757 | 1498 | 364.07 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 12838345 | 252767 | 3068 | 2327.00 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 12994870 | 251601 | 3068 | 2378.17 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | 13944313 | 318020 | 3898 | 4309.88 | UNSAT |
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 15603943 | 277740 | 3324 | 2885.47 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 16095308 | 289323 | 3532 | 3175.65 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 17667194 | 315030 | 3835 | 3510.88 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | 18296605 | 302825 | 3668 | 3485.37 | UNSAT |
1dlx_c_iq59_a.cnf | 623700 | 9457051 | 19893525 | 312227 | 3833 | 3835.57 | UNSAT |
1dlx_c_iq60_a.cnf | 651875 | 9927770 | 21103837 | 323253 | 3984 | 4223.54 | UNSAT |
1dlx_c_iq61_a.cnf | 673311 | 10435991 | 18760289 | 279172 | 3346 | 3753.42 | SAT |
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 2807912 | 106115 | 1426 | 385.59 | UNSAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | 24148242 | 358998 | 4093 | 4927.87 | UNSAT |
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 15023635 | 248884 | 3067 | 3565.69 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | 26852949 | 379526 | 4094 | 5806.89 | UNSAT |
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 3102492 | 123452 | 1640 | 453.77 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 3435323 | 140410 | 1911 | 716.69 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 3800954 | 143187 | 1944 | 816.01 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 4063266 | 138560 | 1864 | 628.90 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 4606960 | 140416 | 1911 | 691.93 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 4773478 | 146750 | 2012 | 736.59 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 5236573 | 153355 | 2044 | 835.01 | UNSAT |
Total (32 / 32) | 354272896 | 7202976 | 88428 | 68863.58 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_4.cnf | 6944 | 66654 | 55855 | 31882 | 509 | 14.12 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 165587 | 106722 | 1435 | 81.18 | UNSAT |
engine_5.cnf | 18788 | 214095 | 872306 | 587268 | 6395 | 1875.31 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 19795 | 11575 | 223 | 7.86 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 64047 | 41524 | 617 | 33.93 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 75885 | 48210 | 731 | 69.88 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | |||||
engine_6_nd_case1.cnf | 45435 | 610120 | 298081 | 209057 | 2552 | 458.50 | UNSAT |
Total (7 / 10) | 1551556 | 1036238 | 12462 | 2540.78 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | 3477222 | 158587 | 2045 | 159.42 | SAT |
pipe_64_4_bug02.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug03.cnf | 35947 | 992674 | 302372 | 930 | 29 | 4.42 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 351134 | 3931 | 91 | 7.57 | SAT |
pipe_64_4_bug05.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug06.cnf | 35853 | 1012271 | 15027712 | 1522665 | 15610 | 4880.38 | SAT |
pipe_64_4_bug07.cnf | 35853 | 1012271 | 5467020 | 343487 | 4092 | 462.64 | SAT |
pipe_64_4_bug08.cnf | 35622 | 1003074 | 13370 | 20 | 1 | 1.97 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 1091379 | 31736 | 509 | 29.50 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 17439 | 21 | 1 | 1.99 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | 447681 | 5964 | 125 | 9.47 | SAT |
pipe_64_4_bug12.cnf | 35854 | 1012275 | 5480662 | 338856 | 4092 | 463.67 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 8160924 | 642729 | 7162 | 1217.75 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 17177 | 22 | 1 | 2.02 | SAT |
pipe_64_4_bug15.cnf | 35853 | 1012271 | 15247819 | 1706021 | 16382 | 5992.26 | SAT |
pipe_64_4_bug16.cnf | 35853 | 1012271 | 17351786 | 1723135 | 16382 | 6044.63 | SAT |
pipe_64_4_bug17.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug18.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug19.cnf | 35852 | 1012266 | 7296350 | 510884 | 5628 | 791.43 | SAT |
pipe_64_4_bug20.cnf | 35853 | 1012271 | |||||
Total (15 / 20) | 79750047 | 6988988 | 72150 | 20069.12 |
fvp-unsat.1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_mc_ex_bp_f.cnf | 776 | 3725 | 2586 | 760 | 24 | 0.03 | UNSAT |
2dlx_ca_mc_ex_bp_f.cnf | 3250 | 24640 | 21007 | 4605 | 103 | 0.42 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 33814 | 8108 | 156 | 1.11 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 538024 | 97675 | 1277 | 48.44 | UNSAT |
Total (4 / 4) | 595431 | 111148 | 1560 | 50 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 3418 | 1225 | 30 | 0.05 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 2838 | 1119 | 30 | 0.05 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 3780 | 1563 | 42 | 0.07 | UNSAT |
3pipe.cnf | 2468 | 27533 | 23498 | 6962 | 126 | 0.64 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 14977 | 5952 | 125 | 0.58 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 26183 | 11076 | 218 | 1.33 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 28588 | 11283 | 220 | 1.38 | UNSAT |
4pipe.cnf | 5237 | 80213 | 85266 | 23938 | 396 | 5.70 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 54951 | 19409 | 317 | 4.31 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 61796 | 20479 | 347 | 4.96 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 85813 | 27130 | 459 | 7.56 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 95181 | 29085 | 506 | 8.68 | UNSAT |
5pipe.cnf | 9471 | 195452 | 131709 | 12401 | 249 | 4.42 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 106457 | 31715 | 509 | 13.21 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 119748 | 32914 | 510 | 14.60 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 129294 | 30703 | 508 | 15.32 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 254109 | 63767 | 967 | 38.31 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 133584 | 29289 | 507 | 15.97 | UNSAT |
6pipe.cnf | 15800 | 394739 | 452799 | 76950 | 1022 | 62.64 | UNSAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 373010 | 75195 | 1022 | 76.13 | UNSAT |
7pipe.cnf | 23910 | 751118 | 974791 | 161124 | 2045 | 248.41 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 147844 | 12083 | 238 | 9.55 | SAT |
Total (22 / 22) | 3309634 | 685362 | 10393 | 533.87 |
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 | 573982 | 82995 | 1053 | 565.30 | SAT |
2dlx_cc_ex_bp_f_bug6_liveness.cnf | 331848 | 5706594 | |||||
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 | 1101546 | 181313 | 2077 | 1748.21 | SAT |
2dlx_cc_ex_bp_f_bug10_liveness.cnf | 536469 | 10122798 | |||||
2dlx_cc_ex_bp_f_bug1_liveness.cnf | 171648 | 2614464 | 170470 | 20709 | 348 | 107.35 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 362416 | 46649 | 700 | 250.28 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 377024 | 50915 | 764 | 310.70 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 466758 | 68642 | 1020 | 444.36 | SAT |
Total (6 / 10) | 3052196 | 451223 | 5962 | 3426.2 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 155814 | 70263 | 1021 | 46.38 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 745658 | 372331 | 4094 | 971.95 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 122594 | 51234 | 765 | 37.90 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 35210 | 15271 | 254 | 4.12 | 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) | 1059276 | 509099 | 6134 | 1060.35 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 49564 | 18051 | 300 | 4.24 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 149042 | 56819 | 843 | 35.47 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 110362 | 42560 | 636 | 27.52 | 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) | 308968 | 117430 | 1779 | 67.23 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 4975 | 1383 | 36 | 0.18 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 143708 | 88903 | 1149 | 51.85 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 291270 | 55269 | 821 | 130.98 | SAT |
2dlx_cc_mc_ex_bp_f2_no_pe.cnf | 96675 | 1401773 | |||||
9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf | 889302 | 14582074 | 1036754 | 52851 | 765 | 1015.42 | SAT |
9dlx_vliw_at_bp_mc2_no_pe.cnf | 889302 | 14582081 | |||||
Total (4 / 6) | 1476707 | 198406 | 2771 | 1198.43 |
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 | 3873 | 1564 | 42 | 0.07 | UNSAT |
3pipe_3_ooo.cnf | 2533 | 32182 | 30189 | 11686 | 227 | 1.51 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 129063 | 47328 | 709 | 15.51 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 391019 | 135713 | 1806 | 91.60 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 959228 | 301178 | 3640 | 382.66 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 2318744 | 700533 | 7833 | 1745.00 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 3657940 | 884076 | 8700 | 3083.85 | UNSAT |
Total (7 / 15) | 7490056 | 2082078 | 22957 | 5320.2 |
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 | 3541 | 1350 | 34 | 0.05 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 2566 | 25625 | 26053 | 9345 | 187 | 0.90 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 107511 | 30789 | 509 | 7.03 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 294535 | 67259 | 1019 | 29.70 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 713418 | 126304 | 1674 | 94.87 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 1652199 | 312862 | 3834 | 431.00 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 3421587 | 532930 | 5985 | 1111.50 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 3163829 | 434444 | 4700 | 966.49 | UNSAT |
Total (8 / 14) | 9382673 | 1515283 | 17942 | 2641.54 |
pipe_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 118040 | 8804672 | 210769 | 20089 | 338 | 121.48 | SAT |
12pipe_bug10.cnf | 118040 | 8804672 | 1309073 | 182213 | 2100 | 932.05 | SAT |
12pipe_bug2.cnf | 118040 | 8804630 | 50972 | 996 | 29 | 25.73 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | 1075957 | 146525 | 2009 | 756.83 | SAT |
12pipe_bug4.cnf | 117504 | 8743027 | 85951 | 3870 | 89 | 40.23 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | 1594051 | 232142 | 2812 | 1169.97 | SAT |
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 16.19 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | 3179023 | 464879 | 5116 | 2910.24 | SAT |
12pipe_bug8.cnf | 117526 | 8760516 | 26791 | 33 | 2 | 17.18 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | 1033388 | 142454 | 1921 | 724.83 | SAT |
Total (10 / 10) | 8571452 | 1193201 | 14416 | 6714.73 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 153728 | 8009 | 155 | 44.59 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | 1010969 | 103495 | 1400 | 465.12 | SAT |
12pipe_bug2_q0.cnf | 138918 | 4678718 | 143741 | 7990 | 154 | 43.47 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 2134394 | 232950 | 2812 | 1032.89 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 531289 | 48494 | 737 | 222.28 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 354187 | 28107 | 483 | 133.25 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | 101700 | 4548 | 101 | 30.08 | SAT |
12pipe_bug7_q0.cnf | 138918 | 4678760 | 1289566 | 120361 | 1577 | 559.36 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 12176 | 122 | 5 | 9.65 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | 260235 | 21682 | 378 | 102.34 | SAT |
Total (10 / 10) | 5991985 | 575758 | 7802 | 2643.03 |
pipe_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 860 | 6693 | 3302 | 1317 | 33 | 0.05 | UNSAT |
03pipe_k.cnf | 2391 | 27405 | 23097 | 6672 | 126 | 0.67 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 79554 | 20350 | 346 | 4.98 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 215877 | 50290 | 764 | 24.88 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 299120 | 21092 | 362 | 12.33 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 881811 | 140731 | 1913 | 198.05 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 1752339 | 214013 | 2557 | 488.44 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 1818159 | 72384 | 1021 | 139.72 | UNSAT |
10pipe_k.cnf | 67300 | 3601247 | 4577875 | 434945 | 4715 | 1814.85 | UNSAT |
11pipe_k.cnf | 89315 | 5584003 | 7565598 | 610076 | 6652 | 3158.20 | UNSAT |
12pipe_k.cnf | 115915 | 8395649 | |||||
13pipe_k.cnf | 147626 | 12295313 | |||||
14pipe_k.cnf | 184980 | 17597059 | |||||
Total (10 / 13) | 17216732 | 1571870 | 18489 | 5842.17 |
pipe_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 873 | 6457 | 2955 | 1243 | 30 | 0.05 | UNSAT |
03pipe_q0_k.cnf | 2476 | 25181 | 21012 | 6968 | 126 | 0.55 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 71063 | 17902 | 295 | 3.16 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 179451 | 32615 | 509 | 10.34 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 259299 | 19462 | 318 | 9.82 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 821947 | 127542 | 1704 | 112.46 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 1555036 | 210880 | 2555 | 254.34 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1508226 | 65506 | 1011 | 105.10 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 4198541 | 402674 | 4282 | 854.76 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | 6494669 | 585367 | 6377 | 1684.06 | UNSAT |
12pipe_q0_k.cnf | 136800 | 4216460 | 9877032 | 894713 | 8827 | 3280.83 | UNSAT |
13pipe_q0_k.cnf | 176066 | 5761591 | |||||
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (11 / 14) | 24989231 | 2364872 | 26034 | 6315.47 |
vliw_sat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 236038 | 8084666 | 4726596 | 253573 | 3068 | 1005.92 | SAT |
9dlx_vliw_at_b_iq6_bug2.cnf | 235928 | 8076545 | 80784 | 33 | 2 | 18.24 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 235402 | 8060882 | |||||
9dlx_vliw_at_b_iq6_bug4.cnf | 235277 | 8063780 | 8269871 | 473274 | 5117 | 2077.16 | SAT |
9dlx_vliw_at_b_iq6_bug5.cnf | 235923 | 8076534 | 5649351 | 259613 | 3069 | 1070.87 | SAT |
9dlx_vliw_at_b_iq6_bug6.cnf | 235926 | 8076539 | 2212279 | 23743 | 388 | 130.03 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 5553057 | 336799 | 4092 | 1164.30 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 715905 | 831 | 27 | 33.69 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | 11924214 | 965324 | 9723 | 5054.60 | SAT |
Total (8 / 9) | 39132057 | 2313190 | 25486 | 10554.81 |
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 | 2667794 | 5201 | 122 | 135.73 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | |||||
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | |||||
Total (1 / 10) | 2667794 | 5201 | 122 | 135.73 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 6673011 | 43798 | 637 | 420.39 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 4013249 | 12646 | 251 | 180.24 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 5073043 | 9947 | 189 | 161.81 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 4200118 | 3554 | 77 | 96.84 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 4204081 | 10225 | 189 | 160.70 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 6233187 | 19155 | 317 | 238.51 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 4625217 | 7331 | 133 | 135.66 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 4288862 | 5681 | 125 | 122.50 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 6610527 | 44197 | 644 | 402.98 | SAT |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 5414540 | 17068 | 276 | 203.68 | SAT |
Total (10 / 10) | 51335835 | 173602 | 2838 | 2123.31 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 2542010 | 637852 | 7127 | 1000.35 | UNSAT |
9dlx_vliw_at_b_iq2.cnf | 44095 | 542253 | 5354828 | 1008686 | 10236 | 2464.45 | UNSAT |
9dlx_vliw_at_b_iq3.cnf | 69789 | 968295 | 10475969 | 1718366 | 16382 | 6801.46 | UNSAT |
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 (3 / 9) | 18372807 | 3364904 | 33745 | 10266.26 |
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 | 5471436 | 574800 | 6176 | 1296.10 | 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) | 5471436 | 574800 | 6176 | 1296.1 |