Tinisat, using restart policy (Luby's, unit=512)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 182 (73 SAT + 109 UNSAT)
Time: 642665 seconds / 178.52 hours / 7.44 days
Time on solved instances: 145865 seconds (50802 SAT + 95063 UNSAT)
Instances solved in 10 minutes: 121 (13069 seconds)
Instances solved in 15 minutes: 131 (20074 seconds)
Instances solved in 20 minutes: 142 (31601 seconds)
Instances solved in 30 minutes: 152 (46070 seconds)
Instances solved in 60 minutes: 172 (99467 seconds)
Instances solved in 90 minutes: 180 (133705 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 32 | / | 32 | 59560.1 | ||
engine_unsat_1.0 | 7 | / | 10 | 1708.83 | ||
fvp-sat.3.0 | 18 | / | 20 | 10047.76 | ||
fvp-unsat.1.0 | 4 | / | 4 | 38.72 | ||
fvp-unsat.2.0 | 22 | / | 22 | 687.43 | ||
fvp-unsat.3.0 | 0 | / | 6 | 0 | ||
liveness_sat_1.0 | 7 | / | 10 | 7154.35 | ||
liveness_unsat_1.0 | 4 | / | 12 | 1011.9 | ||
liveness_unsat_2.0 | 3 | / | 9 | 68.37 | ||
npe-1.0 | 4 | / | 6 | 4862.18 | ||
pipe_ooo_unsat_1.0 | 7 | / | 15 | 3897 | ||
pipe_ooo_unsat_1.1 | 8 | / | 14 | 5977.6 | ||
pipe_sat_1.0 | 9 | / | 10 | 4174.31 | ||
pipe_sat_1.1 | 10 | / | 10 | 2709.11 | ||
pipe_unsat_1.0 | 9 | / | 13 | 4136.98 | ||
pipe_unsat_1.1 | 12 | / | 14 | 18334.73 | ||
vliw_sat_2.0 | 9 | / | 9 | 7704.46 | ||
vliw_sat_2.1 | 4 | / | 10 | 7421.26 | ||
vliw_sat_4.0 | 10 | / | 10 | 1396.19 | ||
vliw_unsat_2.0 | 2 | / | 9 | 3984.79 | ||
vliw_unsat_3.0 | 0 | / | 2 | 0 | ||
vliw_unsat_4.0 | 1 | / | 4 | 988.7 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 5742953 | 185269 | 125 | 829.27 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 6262628 | 205348 | 126 | 948.40 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 6933386 | 204460 | 126 | 983.47 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 7474973 | 219049 | 126 | 1174.21 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 7929792 | 217077 | 126 | 1180.50 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 8617203 | 254015 | 152 | 1373.62 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 8633068 | 225544 | 126 | 1352.33 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 9817422 | 243025 | 141 | 1487.00 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 10176097 | 272367 | 160 | 1749.92 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 11606193 | 295635 | 184 | 1917.98 | UNSAT |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2385772 | 119450 | 84 | 314.75 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 11373635 | 279679 | 170 | 1904.09 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 13781701 | 306446 | 188 | 2218.50 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | 13608901 | 406557 | 251 | 3844.57 | UNSAT |
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 15041393 | 321537 | 189 | 2590.63 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 15978279 | 334394 | 198 | 2717.76 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 17255073 | 341486 | 204 | 3107.34 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | 18861914 | 349122 | 211 | 3357.30 | UNSAT |
1dlx_c_iq59_a.cnf | 623700 | 9457051 | 18963608 | 340203 | 204 | 3327.21 | UNSAT |
1dlx_c_iq60_a.cnf | 651875 | 9927770 | 19667448 | 361192 | 220 | 3631.03 | UNSAT |
1dlx_c_iq61_a.cnf | 673311 | 10435991 | 8668262 | 215831 | 126 | 2002.80 | SAT |
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 2808284 | 137753 | 93 | 372.99 | UNSAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | 22960878 | 408890 | 251 | 4522.49 | UNSAT |
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 16644756 | 309491 | 188 | 3367.87 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | 26632582 | 435757 | 253 | 4970.74 | UNSAT |
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 2904220 | 135997 | 93 | 391.63 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 3191263 | 152615 | 108 | 601.20 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 3659992 | 172585 | 124 | 688.49 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 3946875 | 158418 | 113 | 560.91 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 4405144 | 170252 | 123 | 628.27 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 4837744 | 173956 | 124 | 695.20 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 5104832 | 179806 | 124 | 747.63 | UNSAT |
Total (32 / 32) | 335876271 | 8133206 | 5031 | 59560.1 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_4.cnf | 6944 | 66654 | 46106 | 29588 | 29 | 10.52 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 131653 | 95462 | 62 | 58.92 | UNSAT |
engine_5.cnf | 18788 | 214095 | 685053 | 520283 | 254 | 1237.26 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 17912 | 11333 | 13 | 6.00 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 51938 | 36945 | 30 | 23.77 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 67122 | 46513 | 37 | 55.54 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | |||||
engine_6_nd_case1.cnf | 45435 | 610120 | 237832 | 181292 | 125 | 316.82 | UNSAT |
Total (7 / 10) | 1237616 | 921416 | 550 | 1708.83 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | 3702599 | 400006 | 250 | 330.90 | SAT |
pipe_64_4_bug02.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug03.cnf | 35947 | 992674 | 142217 | 696 | 1 | 3.46 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 167981 | 2253 | 3 | 5.05 | SAT |
pipe_64_4_bug05.cnf | 35853 | 1012271 | 4060031 | 445091 | 253 | 365.88 | SAT |
pipe_64_4_bug06.cnf | 35853 | 1012271 | 2382386 | 244788 | 141 | 151.42 | SAT |
pipe_64_4_bug07.cnf | 35853 | 1012271 | 1592610 | 129689 | 92 | 74.17 | SAT |
pipe_64_4_bug08.cnf | 35622 | 1003074 | 746835 | 56346 | 45 | 28.20 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 1003236 | 78129 | 61 | 40.46 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 1029797 | 72187 | 60 | 39.60 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | 4545267 | 509347 | 254 | 472.51 | SAT |
pipe_64_4_bug12.cnf | 35854 | 1012275 | 402538 | 14633 | 14 | 12.54 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 1577622 | 134264 | 93 | 78.10 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 789006 | 56010 | 45 | 30.00 | SAT |
pipe_64_4_bug15.cnf | 35853 | 1012271 | 14242562 | 1767149 | 818 | 4209.72 | SAT |
pipe_64_4_bug16.cnf | 35853 | 1012271 | 2065152 | 178666 | 124 | 109.45 | SAT |
pipe_64_4_bug17.cnf | 35853 | 1012271 | 4553029 | 550907 | 282 | 548.89 | SAT |
pipe_64_4_bug18.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug19.cnf | 35852 | 1012266 | 12427271 | 1672561 | 765 | 3526.56 | SAT |
pipe_64_4_bug20.cnf | 35853 | 1012271 | 648166 | 31726 | 29 | 20.85 | SAT |
Total (18 / 20) | 56078305 | 6344448 | 3330 | 10047.76 |
fvp-unsat.1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_mc_ex_bp_f.cnf | 776 | 3725 | 2284 | 670 | 1 | 0.02 | UNSAT |
2dlx_ca_mc_ex_bp_f.cnf | 3250 | 24640 | 21060 | 5372 | 6 | 0.45 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 33539 | 9167 | 11 | 1.09 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 490960 | 95506 | 62 | 37.16 | UNSAT |
Total (4 / 4) | 547843 | 110715 | 80 | 38.72 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 3334 | 1366 | 2 | 0.05 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 2898 | 1291 | 2 | 0.05 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 2751 | 1278 | 2 | 0.06 | UNSAT |
3pipe.cnf | 2468 | 27533 | 19669 | 6360 | 7 | 0.59 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 17536 | 8608 | 10 | 0.82 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 22325 | 10897 | 13 | 1.14 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 22686 | 9604 | 12 | 1.11 | UNSAT |
4pipe.cnf | 5237 | 80213 | 88400 | 32072 | 29 | 7.24 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 58277 | 25040 | 25 | 5.06 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 80834 | 33824 | 30 | 9.16 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 95484 | 40283 | 30 | 11.48 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 95140 | 38848 | 30 | 11.31 | UNSAT |
5pipe.cnf | 9471 | 195452 | 126109 | 15211 | 14 | 4.89 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 106311 | 36587 | 30 | 14.73 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 116699 | 38337 | 30 | 16.91 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 123983 | 36968 | 30 | 16.90 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 232891 | 77037 | 61 | 42.51 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 127680 | 36313 | 30 | 18.36 | UNSAT |
6pipe.cnf | 15800 | 394739 | 454237 | 121771 | 86 | 103.50 | UNSAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 411868 | 111822 | 77 | 115.32 | UNSAT |
7pipe.cnf | 23910 | 751118 | 866475 | 202546 | 126 | 303.75 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 37851 | 3098 | 5 | 2.49 | SAT |
Total (22 / 22) | 3113438 | 889161 | 681 | 687.43 |
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 | 1058192 | 232240 | 131 | 1261.40 | SAT |
2dlx_cc_ex_bp_f_bug6_liveness.cnf | 331848 | 5706594 | 2632357 | 653137 | 347 | 4488.86 | SAT |
2dlx_cc_ex_bp_f_bug7_liveness.cnf | 375775 | 6617342 | 462927 | 69933 | 60 | 462.39 | SAT |
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 | 134025 | 17365 | 16 | 74.54 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 134508 | 16038 | 14 | 74.53 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 574723 | 114412 | 77 | 499.10 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 388151 | 59564 | 49 | 293.53 | SAT |
Total (7 / 10) | 5384883 | 1162689 | 694 | 7154.35 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 117964 | 58141 | 47 | 30.11 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 709227 | 403168 | 251 | 949.64 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 103027 | 45269 | 37 | 28.43 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 36285 | 16589 | 15 | 3.72 | 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) | 966503 | 523167 | 350 | 1011.9 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 45067 | 18644 | 18 | 4.06 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 146473 | 65849 | 56 | 36.02 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 105218 | 48569 | 40 | 28.29 | 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) | 296758 | 133062 | 114 | 68.37 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 8681 | 4097 | 6 | 0.50 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 126356 | 84484 | 62 | 41.22 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 347089 | 86165 | 62 | 173.98 | SAT |
2dlx_cc_mc_ex_bp_f2_no_pe.cnf | 96675 | 1401773 | |||||
9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf | 889302 | 14582074 | 3769304 | 319332 | 189 | 4646.48 | SAT |
9dlx_vliw_at_bp_mc2_no_pe.cnf | 889302 | 14582081 | |||||
Total (4 / 6) | 4251430 | 494078 | 319 | 4862.18 |
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 | 2894 | 1288 | 2 | 0.06 | UNSAT |
3pipe_3_ooo.cnf | 2533 | 32182 | 27693 | 12817 | 14 | 1.46 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 116673 | 50055 | 42 | 14.73 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 305085 | 114276 | 77 | 59.04 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 884452 | 329380 | 192 | 365.99 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 1780448 | 576936 | 299 | 1042.71 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 3154178 | 838305 | 444 | 2413.01 | UNSAT |
Total (7 / 15) | 6271423 | 1923057 | 1070 | 3897 |
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 | 3634 | 1587 | 2 | 0.06 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 2566 | 25625 | 24959 | 10016 | 12 | 0.87 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 113490 | 42648 | 33 | 9.69 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 265263 | 74772 | 61 | 29.62 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 618377 | 131735 | 93 | 90.44 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 1600720 | 408091 | 251 | 599.33 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 4132894 | 1121317 | 510 | 3381.19 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 3298533 | 694981 | 378 | 1866.40 | UNSAT |
Total (8 / 14) | 10057870 | 2485147 | 1340 | 5977.6 |
pipe_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 118040 | 8804672 | 1270892 | 281391 | 171 | 1172.49 | SAT |
12pipe_bug10.cnf | 118040 | 8804672 | 1302841 | 244325 | 141 | 1015.65 | SAT |
12pipe_bug2.cnf | 118040 | 8804630 | 73351 | 6799 | 8 | 36.08 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | 437212 | 75287 | 61 | 269.31 | SAT |
12pipe_bug4.cnf | 117504 | 8743027 | 127157 | 16454 | 15 | 65.26 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | 263529 | 35160 | 30 | 126.30 | SAT |
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 16.43 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | |||||
12pipe_bug8.cnf | 117526 | 8760516 | 76144 | 1072 | 2 | 23.86 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | 1734085 | 385093 | 236 | 1448.93 | SAT |
Total (9 / 10) | 5290688 | 1045581 | 664 | 4174.31 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 871231 | 111505 | 77 | 351.36 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | 1621636 | 242547 | 141 | 706.49 | SAT |
12pipe_bug2_q0.cnf | 138918 | 4678718 | 136885 | 9645 | 12 | 36.52 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 111263 | 4462 | 6 | 23.32 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 250841 | 25685 | 27 | 91.42 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 645011 | 84787 | 62 | 263.77 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | 311374 | 41001 | 31 | 114.46 | SAT |
12pipe_bug7_q0.cnf | 138918 | 4678760 | 2060408 | 305840 | 188 | 958.36 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 71257 | 521 | 1 | 12.66 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | 417980 | 47032 | 37 | 150.75 | SAT |
Total (10 / 10) | 6497886 | 873025 | 582 | 2709.11 |
pipe_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 860 | 6693 | 2920 | 1104 | 2 | 0.04 | UNSAT |
03pipe_k.cnf | 2391 | 27405 | 23023 | 8318 | 10 | 0.75 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 82785 | 29491 | 29 | 7.26 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 220874 | 82637 | 62 | 42.93 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 249027 | 27787 | 28 | 14.83 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 1017258 | 251400 | 148 | 379.87 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 1684497 | 348968 | 211 | 680.37 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 1485283 | 95222 | 62 | 141.92 | UNSAT |
10pipe_k.cnf | 67300 | 3601247 | 4674959 | 747300 | 381 | 2869.01 | UNSAT |
11pipe_k.cnf | 89315 | 5584003 | |||||
12pipe_k.cnf | 115915 | 8395649 | |||||
13pipe_k.cnf | 147626 | 12295313 | |||||
14pipe_k.cnf | 184980 | 17597059 | |||||
Total (9 / 13) | 9440626 | 1592227 | 933 | 4136.98 |
pipe_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 873 | 6457 | 2713 | 1065 | 2 | 0.04 | UNSAT |
03pipe_q0_k.cnf | 2476 | 25181 | 22084 | 7805 | 9 | 0.59 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 78380 | 28729 | 29 | 5.14 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 209881 | 72791 | 60 | 25.68 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 202429 | 26814 | 28 | 12.00 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 777658 | 172132 | 124 | 136.92 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 1454362 | 319091 | 189 | 375.89 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1334558 | 100064 | 65 | 130.50 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 4121889 | 714955 | 380 | 1564.51 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | 6697102 | 1185473 | 517 | 3923.54 | UNSAT |
12pipe_q0_k.cnf | 136800 | 4216460 | 10348794 | 1544352 | 731 | 5884.46 | UNSAT |
13pipe_q0_k.cnf | 176066 | 5761591 | 13026028 | 1512883 | 707 | 6275.46 | UNSAT |
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (12 / 14) | 38275878 | 5686154 | 2841 | 18334.73 |
vliw_sat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 236038 | 8084666 | 6599389 | 398735 | 250 | 1112.87 | SAT |
9dlx_vliw_at_b_iq6_bug2.cnf | 235928 | 8076545 | 120421 | 59 | 0 | 17.05 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 235402 | 8060882 | 7110212 | 610255 | 317 | 1768.98 | SAT |
9dlx_vliw_at_b_iq6_bug4.cnf | 235277 | 8063780 | 6499179 | 436858 | 253 | 1224.24 | SAT |
9dlx_vliw_at_b_iq6_bug5.cnf | 235923 | 8076534 | 4273733 | 178393 | 124 | 497.85 | SAT |
9dlx_vliw_at_b_iq6_bug6.cnf | 235926 | 8076539 | 793760 | 1471 | 2 | 33.97 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 4590431 | 343955 | 204 | 766.91 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 2665053 | 40382 | 30 | 133.28 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | 8345859 | 703730 | 379 | 2149.31 | SAT |
Total (9 / 9) | 40998037 | 2713838 | 1559 | 7704.46 |
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 | 9701452 | 562183 | 285 | 2175.82 | SAT |
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 | 12866362 | 708216 | 380 | 2997.00 | SAT |
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 | 1220278 | 964 | 1 | 63.18 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | |||||
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | 13726100 | 491765 | 254 | 2185.26 | SAT |
Total (4 / 10) | 37514192 | 1763128 | 920 | 7421.26 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 6923545 | 56757 | 45 | 325.00 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 5095307 | 4726 | 6 | 84.75 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 5068695 | 15038 | 14 | 141.55 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 5187720 | 5615 | 6 | 98.14 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 6056514 | 24806 | 25 | 195.70 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 3416556 | 3239 | 5 | 69.82 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 4872813 | 5172 | 6 | 93.56 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 4520825 | 6904 | 8 | 93.83 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 5530284 | 13742 | 14 | 136.93 | SAT |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 5738227 | 17392 | 16 | 156.91 | SAT |
Total (10 / 10) | 52410486 | 153391 | 145 | 1396.19 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 2311054 | 643426 | 339 | 662.07 | UNSAT |
9dlx_vliw_at_b_iq2.cnf | 44095 | 542253 | 5983570 | 1546037 | 731 | 3322.72 | 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) | 8294624 | 2189463 | 1070 | 3984.79 |
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 | 5381772 | 639748 | 334 | 988.70 | 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) | 5381772 | 639748 | 334 | 988.7 |