Tinisat, using restart policy (Luby's, unit=1)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 166 (63 SAT + 103 UNSAT)
Time: 800321 seconds / 222.31 hours / 9.26 days
Time on solved instances: 188321 seconds (72065 SAT + 116256 UNSAT)
Instances solved in 10 minutes: 107 (12200 seconds)
Instances solved in 15 minutes: 112 (15788 seconds)
Instances solved in 20 minutes: 116 (20176 seconds)
Instances solved in 30 minutes: 130 (39846 seconds)
Instances solved in 60 minutes: 147 (85078 seconds)
Instances solved in 90 minutes: 157 (130067 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 25 | / | 32 | 73651.94 | ||
engine_unsat_1.0 | 7 | / | 10 | 5906.16 | ||
fvp-sat.3.0 | 15 | / | 20 | 18808.09 | ||
fvp-unsat.1.0 | 4 | / | 4 | 66.06 | ||
fvp-unsat.2.0 | 22 | / | 22 | 558.12 | ||
fvp-unsat.3.0 | 0 | / | 6 | 0 | ||
liveness_sat_1.0 | 6 | / | 10 | 8708.31 | ||
liveness_unsat_1.0 | 4 | / | 12 | 2548.66 | ||
liveness_unsat_2.0 | 3 | / | 9 | 117.54 | ||
npe-1.0 | 4 | / | 6 | 5129.98 | ||
pipe_ooo_unsat_1.0 | 7 | / | 15 | 8113.52 | ||
pipe_ooo_unsat_1.1 | 8 | / | 14 | 3474.41 | ||
pipe_sat_1.0 | 10 | / | 10 | 14749.95 | ||
pipe_sat_1.1 | 10 | / | 10 | 2891.61 | ||
pipe_unsat_1.0 | 11 | / | 13 | 11846.41 | ||
pipe_unsat_1.1 | 11 | / | 14 | 7975.57 | ||
vliw_sat_2.0 | 5 | / | 9 | 9400.1 | ||
vliw_sat_2.1 | 1 | / | 10 | 193.34 | ||
vliw_sat_4.0 | 10 | / | 10 | 5044.1 | ||
vliw_unsat_2.0 | 2 | / | 9 | 6834.49 | ||
vliw_unsat_3.0 | 0 | / | 2 | 0 | ||
vliw_unsat_4.0 | 1 | / | 4 | 2302.22 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 42026 | 1760 | 485 | 35.74 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 7107200 | 160836 | 24571 | 1906.91 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 8580246 | 174641 | 26025 | 2283.08 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 8665350 | 173550 | 25747 | 2383.43 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 9615270 | 189916 | 28667 | 2777.59 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 10640147 | 197439 | 29691 | 2992.83 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 10844409 | 196126 | 29537 | 3187.89 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 12134227 | 218707 | 32764 | 3593.25 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 12778437 | 224916 | 32765 | 3839.56 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 14009714 | 236191 | 32766 | 4274.69 | UNSAT |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2939639 | 97294 | 16117 | 677.88 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 14303718 | 238573 | 32766 | 4401.62 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 16011137 | 252820 | 34299 | 4879.73 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | |||||
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 18415486 | 266275 | 36855 | 5695.31 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 20055518 | 283451 | 39416 | 6343.07 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 20237324 | 297646 | 40957 | 6892.62 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | |||||
1dlx_c_iq59_a.cnf | 623700 | 9457051 | |||||
1dlx_c_iq60_a.cnf | 651875 | 9927770 | |||||
1dlx_c_iq61_a.cnf | 673311 | 10435991 | |||||
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 3370230 | 108787 | 16382 | 799.88 | UNSAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | |||||
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 17946610 | 237918 | 32766 | 7153.74 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | |||||
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 3600094 | 104446 | 16381 | 820.81 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 3877595 | 125972 | 18442 | 1377.63 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 4404426 | 135772 | 20475 | 1635.22 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 4904240 | 130164 | 19449 | 1254.77 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 5444436 | 137283 | 20477 | 1328.19 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 6136298 | 144009 | 21500 | 1449.09 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 6466925 | 153346 | 23193 | 1667.41 | UNSAT |
Total (25 / 32) | 242530702 | 4487838 | 652493 | 73651.94 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_4.cnf | 6944 | 66654 | 91421 | 32940 | 5883 | 27.03 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 311058 | 127291 | 18800 | 202.95 | UNSAT |
engine_5.cnf | 18788 | 214095 | 1515026 | 633966 | 81917 | 4202.20 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 30906 | 12279 | 2301 | 18.09 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 97094 | 41288 | 7287 | 75.23 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 117795 | 49441 | 8190 | 180.41 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | |||||
engine_6_nd_case1.cnf | 45435 | 610120 | 490668 | 222542 | 32765 | 1200.25 | UNSAT |
Total (7 / 10) | 2653968 | 1119747 | 157143 | 5906.16 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | 17072 | 4 | 3 | 1.99 | SAT |
pipe_64_4_bug02.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug03.cnf | 35947 | 992674 | 481532 | 605 | 188 | 5.32 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 708773 | 7402 | 1533 | 16.79 | SAT |
pipe_64_4_bug05.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug06.cnf | 35853 | 1012271 | 23401925 | 1218433 | 147452 | 7061.00 | SAT |
pipe_64_4_bug07.cnf | 35853 | 1012271 | 20629825 | 936259 | 122875 | 4227.33 | SAT |
pipe_64_4_bug08.cnf | 35622 | 1003074 | 5487 | 1 | 1 | 1.92 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 222724 | 227 | 80 | 3.29 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 10685 | 3 | 2 | 1.97 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug12.cnf | 35854 | 1012275 | 396635 | 347 | 124 | 4.53 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 2421521 | 43204 | 7675 | 86.06 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 2388758 | 50135 | 8190 | 89.64 | SAT |
pipe_64_4_bug15.cnf | 35853 | 1012271 | 4138596 | 104183 | 16381 | 204.65 | SAT |
pipe_64_4_bug16.cnf | 35853 | 1012271 | 6320712 | 184254 | 27643 | 433.69 | SAT |
pipe_64_4_bug17.cnf | 35853 | 1012271 | 22470902 | 1095242 | 131070 | 6625.18 | SAT |
pipe_64_4_bug18.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug19.cnf | 35852 | 1012266 | |||||
pipe_64_4_bug20.cnf | 35853 | 1012271 | 1414472 | 22420 | 4093 | 44.73 | SAT |
Total (15 / 20) | 85029619 | 3662719 | 467310 | 18808.09 |
fvp-unsat.1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_mc_ex_bp_f.cnf | 776 | 3725 | 3184 | 617 | 189 | 0.03 | UNSAT |
2dlx_ca_mc_ex_bp_f.cnf | 3250 | 24640 | 27063 | 4749 | 1022 | 0.64 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 40632 | 7281 | 1533 | 1.54 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 641791 | 69540 | 11260 | 63.85 | UNSAT |
Total (4 / 4) | 712670 | 82187 | 14004 | 66.06 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 4979 | 1024 | 254 | 0.06 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 4657 | 1149 | 308 | 0.07 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 6131 | 1342 | 372 | 0.09 | UNSAT |
3pipe.cnf | 2468 | 27533 | 31788 | 5312 | 1085 | 0.71 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 25213 | 5661 | 1188 | 0.76 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 37137 | 8245 | 1786 | 1.37 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 39072 | 8093 | 1738 | 1.42 | UNSAT |
4pipe.cnf | 5237 | 80213 | 101679 | 13667 | 2601 | 4.56 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 83032 | 16902 | 3227 | 5.89 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 95991 | 17755 | 3449 | 6.99 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 110677 | 18650 | 3580 | 8.31 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 128509 | 20700 | 4090 | 10.26 | UNSAT |
5pipe.cnf | 9471 | 195452 | 167966 | 10144 | 2045 | 6.89 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 163782 | 28106 | 4930 | 19.09 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 168532 | 27170 | 4711 | 18.94 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 198481 | 27365 | 4751 | 21.61 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 354177 | 51914 | 8190 | 47.46 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 194171 | 23818 | 4094 | 21.01 | UNSAT |
6pipe.cnf | 15800 | 394739 | 315762 | 26904 | 4620 | 30.53 | SAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 594669 | 66501 | 10747 | 105.76 | UNSAT |
7pipe.cnf | 23910 | 751118 | 1202298 | 101595 | 16380 | 228.91 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 185931 | 8982 | 1952 | 17.43 | SAT |
Total (22 / 22) | 4214634 | 490999 | 86098 | 558.12 |
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 | |||||
2dlx_cc_ex_bp_f_bug6_liveness.cnf | 331848 | 5706594 | 1485230 | 179618 | 26747 | 3085.75 | SAT |
2dlx_cc_ex_bp_f_bug7_liveness.cnf | 375775 | 6617342 | 726519 | 64950 | 10364 | 1204.37 | 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 | 395548 | 38518 | 6778 | 414.48 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 802848 | 85096 | 13819 | 1048.85 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 1084770 | 125489 | 18429 | 1615.75 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 829513 | 90083 | 14587 | 1339.11 | SAT |
Total (6 / 10) | 5324428 | 583754 | 90724 | 8708.31 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 222783 | 62647 | 10234 | 65.81 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 1397917 | 445148 | 62941 | 2408.56 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 185521 | 49182 | 8190 | 68.60 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 55009 | 14008 | 2684 | 5.69 | 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) | 1861230 | 570985 | 84049 | 2548.66 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 70898 | 15119 | 2970 | 6.62 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 212131 | 56108 | 8874 | 64.54 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 143153 | 39140 | 6907 | 46.38 | 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) | 426182 | 110367 | 18751 | 117.54 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 10425 | 1587 | 430 | 0.31 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 213225 | 76187 | 12285 | 62.36 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 309477 | 30830 | 5418 | 166.41 | SAT |
2dlx_cc_mc_ex_bp_f2_no_pe.cnf | 96675 | 1401773 | |||||
9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf | 889302 | 14582074 | 2613308 | 107331 | 16382 | 4900.90 | SAT |
9dlx_vliw_at_bp_mc2_no_pe.cnf | 889302 | 14582081 | |||||
Total (4 / 6) | 3146435 | 215935 | 34515 | 5129.98 |
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 | 5738 | 1225 | 324 | 0.08 | UNSAT |
3pipe_3_ooo.cnf | 2533 | 32182 | 39036 | 8291 | 1787 | 1.47 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 190538 | 40379 | 7163 | 20.50 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 573788 | 113975 | 16382 | 121.42 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 1477314 | 269680 | 36861 | 546.52 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 3378415 | 577931 | 73852 | 2204.03 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 6016526 | 836960 | 109091 | 5219.50 | UNSAT |
Total (7 / 15) | 11681355 | 1848441 | 245460 | 8113.52 |
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 | 5316 | 1231 | 327 | 0.06 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 2566 | 25625 | 34058 | 5718 | 1211 | 0.70 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 133396 | 19722 | 3842 | 6.52 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 424842 | 53217 | 8190 | 35.28 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 946439 | 100088 | 16379 | 114.79 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 2135351 | 203732 | 30715 | 399.44 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 4302296 | 431714 | 60855 | 1373.09 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 4328004 | 426958 | 59897 | 1544.53 | UNSAT |
Total (8 / 14) | 12309702 | 1242380 | 181416 | 3474.41 |
pipe_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 118040 | 8804672 | 4126150 | 300506 | 41354 | 3466.68 | SAT |
12pipe_bug10.cnf | 118040 | 8804672 | 112632 | 1323 | 363 | 46.34 | SAT |
12pipe_bug2.cnf | 118040 | 8804630 | 135006 | 1896 | 508 | 55.26 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | 3458587 | 266072 | 36791 | 2820.36 | SAT |
12pipe_bug4.cnf | 117504 | 8743027 | 167473 | 2580 | 608 | 62.95 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | 1684339 | 102983 | 16381 | 1158.65 | SAT |
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 16.17 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | 5289468 | 399127 | 55966 | 4886.09 | SAT |
12pipe_bug8.cnf | 117526 | 8760516 | 23005 | 8 | 6 | 17.35 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | 2946440 | 204468 | 30934 | 2220.10 | SAT |
Total (10 / 10) | 17948577 | 1278963 | 182911 | 14749.95 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 343715 | 9381 | 2043 | 103.22 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | 2513119 | 117777 | 17145 | 1117.95 | SAT |
12pipe_bug2_q0.cnf | 138918 | 4678718 | 353073 | 11374 | 2092 | 105.53 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 1466751 | 57908 | 9213 | 545.02 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 216406 | 5729 | 1212 | 60.19 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 1370239 | 54983 | 8666 | 510.77 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | 148361 | 2328 | 525 | 30.91 | SAT |
12pipe_bug7_q0.cnf | 138918 | 4678760 | 244957 | 6480 | 1402 | 72.11 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 64185 | 402 | 126 | 11.78 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | 916184 | 33607 | 6070 | 334.13 | SAT |
Total (10 / 10) | 7636990 | 299969 | 48494 | 2891.61 |
pipe_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 860 | 6693 | 5569 | 1168 | 315 | 0.07 | UNSAT |
03pipe_k.cnf | 2391 | 27405 | 30752 | 5993 | 1276 | 0.82 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 99907 | 14481 | 2812 | 5.39 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 273604 | 29962 | 5211 | 20.81 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 377174 | 17741 | 3448 | 20.18 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 1152689 | 96130 | 15865 | 193.82 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 1997458 | 132433 | 19832 | 395.83 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 2188503 | 62726 | 10235 | 230.01 | UNSAT |
10pipe_k.cnf | 67300 | 3601247 | 5392516 | 259793 | 35462 | 1436.14 | UNSAT |
11pipe_k.cnf | 89315 | 5584003 | 8510457 | 427401 | 59959 | 3549.01 | UNSAT |
12pipe_k.cnf | 115915 | 8395649 | 12996040 | 572498 | 73724 | 5994.33 | UNSAT |
13pipe_k.cnf | 147626 | 12295313 | |||||
14pipe_k.cnf | 184980 | 17597059 | |||||
Total (11 / 13) | 33024669 | 1620326 | 228139 | 11846.41 |
pipe_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 873 | 6457 | 4962 | 1052 | 269 | 0.05 | UNSAT |
03pipe_q0_k.cnf | 2476 | 25181 | 29618 | 5409 | 1127 | 0.61 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 107421 | 15392 | 3064 | 4.51 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 248071 | 28310 | 4987 | 14.76 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 315917 | 16028 | 3069 | 14.46 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 1092990 | 82770 | 13308 | 114.12 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 1936874 | 127922 | 18939 | 245.39 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1878492 | 60055 | 9672 | 156.16 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 5575606 | 324933 | 45430 | 1245.10 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | 8290229 | 418384 | 58363 | 2023.29 | UNSAT |
12pipe_q0_k.cnf | 136800 | 4216460 | 13574640 | 641815 | 82592 | 4157.12 | UNSAT |
13pipe_q0_k.cnf | 176066 | 5761591 | |||||
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (11 / 14) | 33054820 | 1722070 | 240820 | 7975.57 |
vliw_sat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 236038 | 8084666 | |||||
9dlx_vliw_at_b_iq6_bug2.cnf | 235928 | 8076545 | 77543 | 14 | 9 | 17.23 | 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 | 2146663 | 8119 | 1752 | 166.53 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 2715457 | 51698 | 8190 | 472.99 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 5438326 | 166999 | 24573 | 2026.90 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | 10147697 | 494754 | 65534 | 6716.45 | SAT |
Total (5 / 9) | 20525686 | 721584 | 100058 | 9400.1 |
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 | 2183353 | 3581 | 858 | 193.34 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | |||||
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | |||||
Total (1 / 10) | 2183353 | 3581 | 858 | 193.34 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 5593440 | 12982 | 2520 | 493.76 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 6191024 | 15470 | 3066 | 601.04 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 5260798 | 14918 | 2935 | 570.94 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 3191398 | 4393 | 1021 | 224.98 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 4517146 | 16224 | 3069 | 589.69 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 5343231 | 18609 | 3580 | 687.77 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 5420126 | 12759 | 2442 | 495.03 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 4015939 | 11665 | 2173 | 444.23 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 5963140 | 13495 | 2557 | 515.76 | SAT |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 4841044 | 10060 | 2045 | 420.90 | SAT |
Total (10 / 10) | 50337286 | 130575 | 25408 | 5044.1 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 2863285 | 400128 | 56214 | 1062.69 | UNSAT |
9dlx_vliw_at_b_iq2.cnf | 44095 | 542253 | 7411578 | 930539 | 122872 | 5771.80 | 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) | 10274863 | 1330667 | 179086 | 6834.49 |
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 | 6584455 | 410872 | 57340 | 2302.22 | 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) | 6584455 | 410872 | 57340 | 2302.22 |