Tinisat, using MiniSat restart policy (100, 1.5)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 164 (60 SAT + 104 UNSAT)
Time: 764413 seconds / 212.34 hours / 8.85 days
Time on solved instances: 138013 seconds (48810 SAT + 89203 UNSAT)
Instances solved in 10 minutes: 109 (10881 seconds)
Instances solved in 15 minutes: 117 (16948 seconds)
Instances solved in 20 minutes: 126 (26262 seconds)
Instances solved in 30 minutes: 135 (39379 seconds)
Instances solved in 60 minutes: 152 (80469 seconds)
Instances solved in 90 minutes: 161 (119648 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 32 | / | 32 | 74873.61 | ||
engine_unsat_1.0 | 7 | / | 10 | 1285.85 | ||
fvp-sat.3.0 | 16 | / | 20 | 4206.84 | ||
fvp-unsat.1.0 | 4 | / | 4 | 41.79 | ||
fvp-unsat.2.0 | 22 | / | 22 | 1193.24 | ||
fvp-unsat.3.0 | 0 | / | 6 | 0 | ||
liveness_sat_1.0 | 5 | / | 10 | 2585.43 | ||
liveness_unsat_1.0 | 4 | / | 12 | 1044.86 | ||
liveness_unsat_2.0 | 3 | / | 9 | 57.14 | ||
npe-1.0 | 4 | / | 6 | 1142.39 | ||
pipe_ooo_unsat_1.0 | 7 | / | 15 | 4471.96 | ||
pipe_ooo_unsat_1.1 | 8 | / | 14 | 3817.42 | ||
pipe_sat_1.0 | 6 | / | 10 | 4915.42 | ||
pipe_sat_1.1 | 7 | / | 10 | 19026.08 | ||
pipe_unsat_1.0 | 8 | / | 13 | 1596.68 | ||
pipe_unsat_1.1 | 9 | / | 14 | 4258.84 | ||
vliw_sat_2.0 | 8 | / | 9 | 6957.99 | ||
vliw_sat_2.1 | 2 | / | 10 | 1734.44 | ||
vliw_sat_4.0 | 10 | / | 10 | 1321.4 | ||
vliw_unsat_2.0 | 1 | / | 9 | 1897.52 | ||
vliw_unsat_3.0 | 0 | / | 2 | 0 | ||
vliw_unsat_4.0 | 1 | / | 4 | 1583.62 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2991086 | 194895 | 16 | 474.56 | UNSAT |
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 2610633 | 146045 | 16 | 388.71 | UNSAT |
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 3348946 | 163360 | 16 | 476.46 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 3374158 | 166105 | 16 | 608.68 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 4022326 | 256468 | 17 | 919.49 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 4070882 | 230543 | 17 | 767.76 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 4957597 | 262144 | 17 | 871.99 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 5055486 | 193340 | 16 | 708.35 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 5537248 | 214987 | 17 | 850.43 | UNSAT |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 6230084 | 248951 | 17 | 999.41 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 6917941 | 295068 | 18 | 1238.43 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 6927612 | 268707 | 17 | 1155.50 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 7626148 | 271751 | 17 | 1265.60 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 8279547 | 263408 | 17 | 1358.68 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 9087912 | 273288 | 17 | 1559.83 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 10425806 | 356300 | 18 | 1957.04 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 10768123 | 302203 | 18 | 1763.17 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 11790427 | 302949 | 18 | 1841.14 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 11825801 | 377321 | 18 | 2363.96 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 13121454 | 377889 | 18 | 2515.81 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 14115064 | 408282 | 18 | 2705.90 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | 13345697 | 581677 | 19 | 4611.69 | UNSAT |
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 14077994 | 448199 | 19 | 2971.21 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 17007437 | 410184 | 18 | 3359.61 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 18782146 | 555858 | 19 | 4196.29 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | 22090303 | 624195 | 19 | 5053.86 | UNSAT |
1dlx_c_iq59_a.cnf | 623700 | 9457051 | 20196710 | 475247 | 19 | 4231.56 | UNSAT |
1dlx_c_iq60_a.cnf | 651875 | 9927770 | 23214551 | 550669 | 19 | 4832.74 | UNSAT |
1dlx_c_iq61_a.cnf | 673311 | 10435991 | 17839754 | 415281 | 18 | 3653.18 | SAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | 24029984 | 489959 | 19 | 4788.50 | UNSAT |
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 14885314 | 331297 | 18 | 3191.35 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | 29721563 | 718783 | 20 | 7192.72 | UNSAT |
Total (32 / 32) | 368275734 | 11175353 | 566 | 74873.61 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_6_nd_case1.cnf | 45435 | 610120 | 231007 | 176379 | 16 | 287.67 | UNSAT |
engine_4.cnf | 6944 | 66654 | 46158 | 30657 | 12 | 10.92 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 124990 | 92719 | 15 | 54.51 | UNSAT |
engine_5.cnf | 18788 | 214095 | 561385 | 434188 | 18 | 851.88 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 16655 | 10993 | 9 | 5.43 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 52509 | 38315 | 12 | 24.76 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 62644 | 44760 | 13 | 50.68 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | |||||
Total (7 / 10) | 1095348 | 828011 | 95 | 1285.85 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | 583930 | 35571 | 12 | 17.87 | SAT |
pipe_64_4_bug02.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug03.cnf | 35947 | 992674 | 138513 | 1943 | 5 | 4.40 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 489500 | 25215 | 11 | 13.29 | SAT |
pipe_64_4_bug05.cnf | 35853 | 1012271 | 4788679 | 1139518 | 21 | 1557.85 | SAT |
pipe_64_4_bug06.cnf | 35853 | 1012271 | 1364550 | 210525 | 17 | 107.23 | SAT |
pipe_64_4_bug07.cnf | 35853 | 1012271 | 1302426 | 246510 | 17 | 127.77 | SAT |
pipe_64_4_bug08.cnf | 35622 | 1003074 | 1448943 | 444284 | 19 | 343.62 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 450579 | 30823 | 12 | 14.48 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 1496420 | 314365 | 18 | 179.05 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | 4469109 | 1022909 | 21 | 1086.18 | SAT |
pipe_64_4_bug12.cnf | 35854 | 1012275 | 1292615 | 234143 | 17 | 122.90 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 439157 | 20169 | 11 | 12.13 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 548547 | 19574 | 11 | 13.38 | SAT |
pipe_64_4_bug15.cnf | 35853 | 1012271 | 996735 | 136082 | 16 | 63.18 | SAT |
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 | 3063625 | 634490 | 19 | 502.36 | SAT |
pipe_64_4_bug20.cnf | 35853 | 1012271 | 844799 | 91366 | 15 | 41.15 | SAT |
Total (16 / 20) | 23718127 | 4607487 | 242 | 4206.84 |
fvp-unsat.1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_mc_ex_bp_f.cnf | 776 | 3725 | 2508 | 743 | 3 | 0.02 | UNSAT |
2dlx_ca_mc_ex_bp_f.cnf | 3250 | 24640 | 20496 | 5370 | 8 | 0.45 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 35536 | 9835 | 9 | 1.30 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 492498 | 98285 | 15 | 40.02 | UNSAT |
Total (4 / 4) | 551038 | 114233 | 35 | 41.79 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 3174 | 1287 | 4 | 0.05 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 3147 | 1387 | 5 | 0.06 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 3085 | 1356 | 5 | 0.06 | UNSAT |
3pipe.cnf | 2468 | 27533 | 22157 | 8404 | 9 | 0.74 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 12629 | 5245 | 8 | 0.44 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 23334 | 9943 | 9 | 1.04 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 27407 | 12487 | 10 | 1.37 | UNSAT |
4pipe.cnf | 5237 | 80213 | 95579 | 37319 | 12 | 8.49 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 55785 | 23445 | 11 | 5.35 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 71958 | 29928 | 12 | 7.36 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 88936 | 34633 | 12 | 9.50 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 169434 | 81833 | 14 | 35.62 | UNSAT |
5pipe.cnf | 9471 | 195452 | 110712 | 14569 | 10 | 4.27 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 117321 | 37638 | 12 | 18.16 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 140816 | 48862 | 13 | 29.24 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 149626 | 48628 | 13 | 28.17 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 265416 | 87930 | 15 | 56.29 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 141425 | 42796 | 13 | 24.41 | UNSAT |
6pipe.cnf | 15800 | 394739 | 571806 | 184524 | 16 | 192.17 | UNSAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 463974 | 125891 | 15 | 153.58 | UNSAT |
7pipe.cnf | 23910 | 751118 | 1168826 | 318819 | 18 | 497.61 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 542511 | 143273 | 16 | 119.26 | SAT |
Total (22 / 22) | 4249058 | 1300197 | 252 | 1193.24 |
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 | |||||
2dlx_cc_ex_bp_f_bug1_liveness.cnf | 171648 | 2614464 | 99926 | 12352 | 10 | 49.84 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 335665 | 68294 | 14 | 254.36 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 463626 | 114066 | 15 | 446.30 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 822381 | 177329 | 16 | 784.39 | SAT |
2dlx_cc_ex_bp_f_bug5_liveness.cnf | 292249 | 4906188 | 869188 | 209060 | 17 | 1050.54 | 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 | |||||
Total (5 / 10) | 2590786 | 581101 | 72 | 2585.43 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 130828 | 69417 | 14 | 38.44 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 691116 | 405690 | 18 | 959.40 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 123367 | 60105 | 14 | 43.05 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 35543 | 17532 | 11 | 3.97 | 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) | 980854 | 552744 | 57 | 1044.86 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 52530 | 23464 | 11 | 5.52 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 135597 | 55148 | 13 | 28.01 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 95651 | 44358 | 13 | 23.61 | 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) | 283778 | 122970 | 37 | 57.14 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 13689 | 7297 | 8 | 0.96 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 131793 | 89507 | 15 | 43.93 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 114825 | 26626 | 12 | 48.53 | SAT |
2dlx_cc_mc_ex_bp_f2_no_pe.cnf | 96675 | 1401773 | |||||
9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf | 889302 | 14582074 | 1384635 | 76587 | 14 | 1048.97 | SAT |
9dlx_vliw_at_bp_mc2_no_pe.cnf | 889302 | 14582081 | |||||
Total (4 / 6) | 1644942 | 200017 | 49 | 1142.39 |
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 | 3006 | 1341 | 5 | 0.06 | UNSAT |
3pipe_3_ooo.cnf | 2533 | 32182 | 23436 | 10596 | 9 | 1.09 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 126486 | 59028 | 14 | 18.28 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 338107 | 135808 | 16 | 78.31 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 1031507 | 417405 | 18 | 572.91 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 1787619 | 637685 | 19 | 1226.93 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 3529367 | 949768 | 20 | 2574.38 | UNSAT |
Total (7 / 15) | 6839528 | 2211631 | 101 | 4471.96 |
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 | 4134 | 1785 | 5 | 0.07 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 2566 | 25625 | 29197 | 11076 | 9 | 1.00 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 92547 | 29023 | 12 | 5.85 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 308022 | 105831 | 15 | 49.62 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 712112 | 220689 | 17 | 191.46 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 1519526 | 418438 | 18 | 624.03 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 3137218 | 786461 | 20 | 1966.96 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 2636341 | 447504 | 19 | 978.43 | UNSAT |
Total (8 / 14) | 8439097 | 2020807 | 115 | 3817.42 |
pipe_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 118040 | 8804672 | |||||
12pipe_bug10.cnf | 118040 | 8804672 | |||||
12pipe_bug2.cnf | 118040 | 8804630 | 102119 | 13984 | 10 | 49.28 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | |||||
12pipe_bug4.cnf | 117504 | 8743027 | 590904 | 110765 | 15 | 356.40 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | |||||
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 16.15 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | 2024576 | 609639 | 19 | 2263.45 | SAT |
12pipe_bug8.cnf | 117526 | 8760516 | 48937 | 274 | 2 | 18.35 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | 2285173 | 666223 | 20 | 2211.79 | SAT |
Total (6 / 10) | 5057186 | 1400885 | 66 | 4915.42 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 3961068 | 1068376 | 21 | 3680.90 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | |||||
12pipe_bug2_q0.cnf | 138918 | 4678718 | 88900 | 1991 | 5 | 15.70 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 6455172 | 1484152 | 21 | 5681.91 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 94894 | 3243 | 7 | 17.25 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 4040703 | 1226854 | 21 | 4129.68 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | |||||
12pipe_bug7_q0.cnf | 138918 | 4678760 | 5046961 | 1482663 | 21 | 5490.05 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 60287 | 126 | 1 | 10.59 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | |||||
Total (7 / 10) | 19747985 | 5267405 | 97 | 19026.08 |
pipe_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 860 | 6693 | 3350 | 1270 | 4 | 0.05 | UNSAT |
03pipe_k.cnf | 2391 | 27405 | 21198 | 7508 | 9 | 0.60 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 73107 | 22859 | 11 | 4.73 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 230678 | 72329 | 14 | 37.56 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 240237 | 26913 | 12 | 14.08 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 944645 | 206403 | 17 | 254.78 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 2261085 | 544364 | 19 | 1115.74 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 1301120 | 98713 | 15 | 169.14 | 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) | 5075420 | 980359 | 101 | 1596.68 |
pipe_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 873 | 6457 | 3151 | 1442 | 5 | 0.05 | UNSAT |
03pipe_q0_k.cnf | 2476 | 25181 | 19472 | 7226 | 8 | 0.51 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 77659 | 27705 | 12 | 4.87 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 252205 | 95164 | 15 | 38.45 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 217666 | 25797 | 12 | 10.92 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 1058508 | 352494 | 18 | 362.83 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 1350153 | 321593 | 18 | 377.19 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1329925 | 93986 | 15 | 124.52 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 4839186 | 1233393 | 21 | 3339.50 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | |||||
12pipe_q0_k.cnf | 136800 | 4216460 | |||||
13pipe_q0_k.cnf | 176066 | 5761591 | |||||
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (9 / 14) | 9147925 | 2158800 | 124 | 4258.84 |
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 | 120421 | 59 | 0 | 17.20 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 235402 | 8060882 | 3303967 | 120947 | 15 | 321.32 | SAT |
9dlx_vliw_at_b_iq6_bug4.cnf | 235277 | 8063780 | 5480472 | 747137 | 20 | 2170.74 | SAT |
9dlx_vliw_at_b_iq6_bug5.cnf | 235923 | 8076534 | 2563544 | 84344 | 14 | 198.23 | SAT |
9dlx_vliw_at_b_iq6_bug6.cnf | 235926 | 8076539 | 1106956 | 7660 | 9 | 44.99 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 5406593 | 769496 | 20 | 1817.66 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 3133185 | 203750 | 17 | 445.80 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | 6475196 | 678746 | 20 | 1942.05 | SAT |
Total (8 / 9) | 27590334 | 2612139 | 115 | 6957.99 |
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 | 4108679 | 15402 | 10 | 171.28 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | |||||
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | 15525479 | 352569 | 18 | 1563.16 | SAT |
Total (2 / 10) | 19634158 | 367971 | 28 | 1734.44 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 5672614 | 17483 | 11 | 152.69 | SAT |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 6579408 | 6853 | 8 | 110.47 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 4328631 | 4815 | 7 | 87.10 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 4440992 | 10828 | 9 | 120.83 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 5189992 | 4094 | 7 | 79.34 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 7988539 | 33780 | 12 | 219.92 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 6250000 | 18228 | 11 | 156.54 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 5655991 | 9911 | 9 | 123.02 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 4634744 | 6428 | 8 | 95.28 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 5561713 | 22340 | 11 | 176.21 | SAT |
Total (10 / 10) | 56302624 | 134760 | 93 | 1321.4 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 3550886 | 1230802 | 21 | 1897.52 | 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) | 3550886 | 1230802 | 21 | 1897.52 |
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 | 5578053 | 869238 | 20 | 1583.62 | 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) | 5578053 | 869238 | 20 | 1583.62 |