Tinisat, using restart policy (32, 1.1)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 174 (67 SAT + 107 UNSAT)
Time: 691452 seconds / 192.07 hours / 8.00 days
Time on solved instances: 137052 seconds (48524 SAT + 88528 UNSAT)
Instances solved in 10 minutes: 113 (10003 seconds)
Instances solved in 15 minutes: 128 (21337 seconds)
Instances solved in 20 minutes: 134 (27724 seconds)
Instances solved in 30 minutes: 145 (42937 seconds)
Instances solved in 60 minutes: 164 (90192 seconds)
Instances solved in 90 minutes: 171 (118945 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 32 | / | 32 | |||
engine_unsat_1.0 | 7 | / | 10 | |||
fvp-sat.3.0 | 18 | / | 20 | |||
fvp-unsat.1.0 | 4 | / | 4 | |||
fvp-unsat.2.0 | 22 | / | 22 | |||
fvp-unsat.3.0 | 0 | / | 6 | |||
liveness_sat_1.0 | 6 | / | 10 | |||
liveness_unsat_1.0 | 4 | / | 12 | |||
liveness_unsat_2.0 | 3 | / | 9 | |||
npe-1.0 | 3 | / | 6 | |||
pipe_ooo_unsat_1.0 | 7 | / | 15 | |||
pipe_ooo_unsat_1.1 | 8 | / | 14 | |||
pipe_sat_1.0 | 5 | / | 10 | |||
pipe_sat_1.1 | 10 | / | 10 | |||
pipe_unsat_1.0 | 8 | / | 13 | |||
pipe_unsat_1.1 | 11 | / | 14 | |||
vliw_sat_2.0 | 8 | / | 9 | |||
vliw_sat_2.1 | 5 | / | 10 | |||
vliw_sat_4.0 | 10 | / | 10 | |||
vliw_unsat_2.0 | 2 | / | 9 | |||
vliw_unsat_3.0 | 0 | / | 2 | |||
vliw_unsat_4.0 | 1 | / | 4 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 5833550 | 200020 | 69 | 832.97 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 5893695 | 202274 | 69 | 891.72 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 6356375 | 209159 | 69 | 994.61 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 7725083 | 270978 | 72 | 1261.02 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 7591991 | 236550 | 71 | 1217.55 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 8238710 | 240378 | 71 | 1375.71 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 9160161 | 245693 | 71 | 1414.35 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 9767908 | 268876 | 72 | 1589.85 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 10491428 | 317408 | 74 | 1872.45 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 11398909 | 292768 | 73 | 1937.08 | UNSAT |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2588659 | 143940 | 65 | 357.35 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 12560004 | 315008 | 74 | 2043.08 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 13402275 | 303968 | 73 | 2191.49 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | 13699003 | 461890 | 78 | 4025.18 | UNSAT |
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 14931217 | 351097 | 75 | 2661.23 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 15930906 | 384971 | 76 | 3118.18 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 16859125 | 383971 | 76 | 3160.20 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | 18987832 | 380987 | 76 | 3441.43 | UNSAT |
1dlx_c_iq59_a.cnf | 623700 | 9457051 | 20289329 | 426376 | 77 | 3792.51 | UNSAT |
1dlx_c_iq60_a.cnf | 651875 | 9927770 | 19764981 | 449150 | 77 | 3951.41 | UNSAT |
1dlx_c_iq61_a.cnf | 673311 | 10435991 | 14147125 | 272453 | 72 | 2728.95 | SAT |
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 2842376 | 128274 | 64 | 354.46 | UNSAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | 22317831 | 441051 | 77 | 4454.52 | UNSAT |
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 14982042 | 338997 | 74 | 3282.56 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | 27049844 | 497053 | 78 | 5407.37 | UNSAT |
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 3037936 | 144090 | 65 | 419.51 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 3633162 | 199794 | 69 | 730.41 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 3735271 | 201311 | 69 | 765.08 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 4212869 | 182136 | 68 | 584.96 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 4484976 | 190842 | 68 | 692.08 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 4906282 | 178808 | 68 | 697.48 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 5264084 | 197991 | 69 | 800.71 | UNSAT |
Total (32 / 32) | 342084939 | 9058262 | 2299 | 63047.46 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_4.cnf | 6944 | 66654 | 45099 | 28549 | 48 | 9.68 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 131548 | 95379 | 61 | 58.17 | UNSAT |
engine_5.cnf | 18788 | 214095 | 653861 | 502887 | 78 | 1127.69 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 18669 | 11627 | 39 | 6.28 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 54913 | 38538 | 52 | 25.89 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 64962 | 46004 | 53 | 52.90 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | |||||
engine_6_nd_case1.cnf | 45435 | 610120 | 240307 | 185842 | 68 | 320.43 | UNSAT |
Total (7 / 10) | 1209359 | 908826 | 399 | 1601.04 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | 1234761 | 70738 | 58 | 38.17 | SAT |
pipe_64_4_bug02.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug03.cnf | 35947 | 992674 | 163598 | 896 | 14 | 3.44 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 364865 | 4422 | 29 | 7.37 | SAT |
pipe_64_4_bug05.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug06.cnf | 35853 | 1012271 | 5061253 | 863571 | 84 | 808.48 | SAT |
pipe_64_4_bug07.cnf | 35853 | 1012271 | 1678922 | 223851 | 70 | 120.61 | SAT |
pipe_64_4_bug08.cnf | 35622 | 1003074 | 21538 | 36 | 1 | 2.00 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 25900 | 56 | 1 | 2.04 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 25552 | 37 | 1 | 2.03 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | 4697897 | 859606 | 84 | 864.29 | SAT |
pipe_64_4_bug12.cnf | 35854 | 1012275 | 999302 | 71849 | 58 | 35.49 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 5245299 | 993976 | 86 | 1264.64 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 25291 | 38 | 1 | 2.03 | SAT |
pipe_64_4_bug15.cnf | 35853 | 1012271 | 2451733 | 328991 | 74 | 200.93 | SAT |
pipe_64_4_bug16.cnf | 35853 | 1012271 | 6686557 | 1191403 | 88 | 1594.76 | SAT |
pipe_64_4_bug17.cnf | 35853 | 1012271 | 8337933 | 1272430 | 88 | 1668.25 | SAT |
pipe_64_4_bug18.cnf | 35853 | 1012271 | 4884542 | 661905 | 81 | 560.89 | SAT |
pipe_64_4_bug19.cnf | 35852 | 1012266 | 25665 | 53 | 1 | 2.05 | SAT |
pipe_64_4_bug20.cnf | 35853 | 1012271 | 1994739 | 178211 | 68 | 107.56 | SAT |
Total (18 / 20) | 43925347 | 6722069 | 887 | 7285.03 |
fvp-unsat.1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_mc_ex_bp_f.cnf | 776 | 3725 | 2355 | 667 | 12 | 0.02 | UNSAT |
2dlx_ca_mc_ex_bp_f.cnf | 3250 | 24640 | 20073 | 4788 | 30 | 0.41 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 31671 | 8848 | 36 | 1.11 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 458689 | 86751 | 60 | 34.51 | UNSAT |
Total (4 / 4) | 512788 | 101054 | 138 | 36.05 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 2670 | 1037 | 15 | 0.04 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 2768 | 1168 | 16 | 0.05 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 3346 | 1524 | 19 | 0.07 | UNSAT |
3pipe.cnf | 2468 | 27533 | 20485 | 7484 | 34 | 0.71 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 15203 | 6553 | 33 | 0.60 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 23870 | 11096 | 39 | 1.21 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 26050 | 10690 | 38 | 1.25 | UNSAT |
4pipe.cnf | 5237 | 80213 | 74871 | 24756 | 47 | 5.47 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 56691 | 24037 | 47 | 5.21 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 70221 | 26767 | 48 | 6.60 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 95910 | 41172 | 52 | 11.49 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 103371 | 41990 | 52 | 12.38 | UNSAT |
5pipe.cnf | 9471 | 195452 | 125701 | 13661 | 41 | 4.30 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 111507 | 36800 | 51 | 15.66 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 131294 | 38889 | 52 | 17.78 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 124238 | 36244 | 51 | 16.52 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 248310 | 79840 | 59 | 45.02 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 134252 | 37033 | 51 | 18.56 | UNSAT |
6pipe.cnf | 15800 | 394739 | 449018 | 114695 | 63 | 101.34 | UNSAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 419550 | 113388 | 63 | 125.05 | UNSAT |
7pipe.cnf | 23910 | 751118 | 815266 | 174166 | 67 | 181.78 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 688369 | 152013 | 66 | 162.21 | SAT |
Total (22 / 22) | 3742961 | 995003 | 1004 | 733.3 |
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 | 1492392 | 384640 | 76 | 2190.13 | 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 | 1204561 | 284592 | 73 | 1917.29 | SAT |
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 | 65957 | 6755 | 33 | 36.11 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 259754 | 43450 | 53 | 179.12 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 673745 | 144636 | 65 | 628.55 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 1152619 | 273757 | 72 | 1312.44 | SAT |
Total (6 / 10) | 4849028 | 1137830 | 372 | 6263.64 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 129351 | 66286 | 57 | 36.78 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 687862 | 395766 | 76 | 925.53 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 98547 | 43422 | 53 | 27.57 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 35049 | 16181 | 42 | 3.47 | 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) | 950809 | 521655 | 228 | 993.35 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 47973 | 17671 | 43 | 4.00 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 135906 | 55898 | 55 | 29.42 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 101304 | 44982 | 53 | 24.83 | 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) | 285183 | 118551 | 151 | 58.25 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 10758 | 4727 | 30 | 0.54 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 115218 | 77711 | 59 | 33.47 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 195774 | 41206 | 52 | 78.37 | SAT |
2dlx_cc_mc_ex_bp_f2_no_pe.cnf | 96675 | 1401773 | |||||
9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf | 889302 | 14582074 | |||||
9dlx_vliw_at_bp_mc2_no_pe.cnf | 889302 | 14582081 | |||||
Total (3 / 6) | 321750 | 123644 | 141 | 112.38 |
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 | 3198 | 1420 | 18 | 0.06 | UNSAT |
3pipe_3_ooo.cnf | 2533 | 32182 | 24572 | 10069 | 38 | 1.12 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 103843 | 43253 | 53 | 11.82 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 329968 | 128108 | 64 | 73.85 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 843414 | 316136 | 74 | 350.96 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 1854979 | 634335 | 81 | 1153.22 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 3492581 | 863337 | 84 | 2159.47 | UNSAT |
Total (7 / 15) | 6652555 | 1996658 | 412 | 3750.5 |
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 | 4092 | 1682 | 20 | 0.07 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 2566 | 25625 | 25962 | 10065 | 38 | 0.93 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 103254 | 36231 | 51 | 7.68 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 279200 | 81416 | 59 | 34.56 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 613105 | 144393 | 65 | 101.60 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 1354804 | 272554 | 72 | 321.40 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 2982651 | 622958 | 81 | 1313.35 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 3281261 | 710038 | 82 | 1897.91 | UNSAT |
Total (8 / 14) | 8644329 | 1879337 | 468 | 3677.5 |
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 | 145651 | 18080 | 44 | 81.02 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | |||||
12pipe_bug4.cnf | 117504 | 8743027 | 234087 | 38658 | 52 | 138.98 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | 280721 | 46560 | 54 | 162.84 | SAT |
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 16.07 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | |||||
12pipe_bug8.cnf | 117526 | 8760516 | 26927 | 72 | 2 | 17.01 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | |||||
Total (5 / 10) | 692863 | 103370 | 152 | 415.92 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 361594 | 38507 | 52 | 123.03 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | 960920 | 144206 | 65 | 403.64 | SAT |
12pipe_bug2_q0.cnf | 138918 | 4678718 | 138796 | 9799 | 37 | 40.58 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 4456081 | 1020369 | 86 | 3430.73 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 2026174 | 426938 | 77 | 1201.39 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 641692 | 85887 | 60 | 257.80 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | 145987 | 12539 | 40 | 45.45 | SAT |
12pipe_bug7_q0.cnf | 138918 | 4678760 | 6299279 | 1584989 | 91 | 6115.88 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 25957 | 45 | 1 | 9.57 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | 103835 | 6180 | 33 | 27.86 | SAT |
Total (10 / 10) | 15160315 | 3329459 | 542 | 11655.93 |
pipe_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 860 | 6693 | 3051 | 1135 | 16 | 0.05 | UNSAT |
03pipe_k.cnf | 2391 | 27405 | 17985 | 5874 | 32 | 0.51 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 65329 | 22853 | 46 | 4.64 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 200904 | 61291 | 56 | 28.42 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 253568 | 26301 | 48 | 12.65 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 1007502 | 229340 | 70 | 294.62 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 1832524 | 395278 | 76 | 845.71 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 1499759 | 97587 | 61 | 149.94 | 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) | 4880622 | 839659 | 405 | 1336.54 |
pipe_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 873 | 6457 | 3078 | 1328 | 18 | 0.05 | UNSAT |
03pipe_q0_k.cnf | 2476 | 25181 | 19973 | 6559 | 33 | 0.50 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 80104 | 27886 | 48 | 4.93 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 178672 | 50758 | 54 | 15.93 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 232390 | 25806 | 47 | 11.61 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 800689 | 186851 | 68 | 147.53 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 1530408 | 358322 | 75 | 440.43 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1281739 | 86285 | 60 | 111.21 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 4473809 | 790379 | 83 | 1807.73 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | 6913676 | 1388187 | 89 | 4322.73 | UNSAT |
12pipe_q0_k.cnf | 136800 | 4216460 | 9737046 | 1727033 | 91 | 6583.74 | UNSAT |
13pipe_q0_k.cnf | 176066 | 5761591 | |||||
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (11 / 14) | 25251584 | 4649394 | 666 | 13446.39 |
vliw_sat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 236038 | 8084666 | 9449516 | 1073432 | 86 | 3505.16 | SAT |
9dlx_vliw_at_b_iq6_bug2.cnf | 235928 | 8076545 | 120670 | 57 | 1 | 17.42 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 235402 | 8060882 | |||||
9dlx_vliw_at_b_iq6_bug4.cnf | 235277 | 8063780 | 6554096 | 703856 | 82 | 1881.34 | SAT |
9dlx_vliw_at_b_iq6_bug5.cnf | 235923 | 8076534 | 4277908 | 125804 | 64 | 334.69 | SAT |
9dlx_vliw_at_b_iq6_bug6.cnf | 235926 | 8076539 | 1830221 | 6734 | 33 | 55.82 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 3929826 | 336558 | 74 | 631.02 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 2229881 | 29238 | 49 | 117.64 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | 6318929 | 221856 | 70 | 620.61 | SAT |
Total (8 / 9) | 34711047 | 2497535 | 459 | 7163.7 |
vliw_sat_2.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq8_bug1.cnf | 410707 | 15613033 | 6747834 | 207552 | 69 | 839.02 | SAT |
9dlx_vliw_at_b_iq8_bug10.cnf | 408558 | 15554750 | 11817469 | 518989 | 79 | 2028.25 | SAT |
9dlx_vliw_at_b_iq8_bug2.cnf | 409731 | 15576332 | 12610193 | 1010409 | 86 | 3896.86 | SAT |
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 | 1820647 | 2400 | 23 | 87.17 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | 8280132 | 303664 | 73 | 1194.28 | SAT |
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | |||||
Total (5 / 10) | 41276275 | 2043014 | 330 | 8045.58 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 5473297 | 14175 | 41 | 147.47 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 6909041 | 18840 | 44 | 173.97 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 5130946 | 8870 | 36 | 117.19 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 5036460 | 8309 | 36 | 118.46 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 4244387 | 7594 | 35 | 107.41 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 5914071 | 13509 | 41 | 144.68 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 4068534 | 5717 | 32 | 94.13 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 4117780 | 3349 | 26 | 83.77 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 6998941 | 48373 | 54 | 301.56 | SAT |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 5556636 | 15839 | 42 | 153.33 | SAT |
Total (10 / 10) | 53450093 | 144575 | 387 | 1441.97 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 2326826 | 676145 | 82 | 685.54 | UNSAT |
9dlx_vliw_at_b_iq2.cnf | 44095 | 542253 | 6603409 | 1886900 | 92 | 4310.58 | 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) | 8930235 | 2563045 | 174 | 4996.12 |
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 | 4844018 | 664596 | 81 | 991.74 | 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) | 4844018 | 664596 | 81 | 991.74 |