Tinisat, using restart policy (Luby's, unit=4096)
22 groups, 251 instances, 2-hour cutoff
Instances solved: 177 (70 SAT + 107 UNSAT)
Time: 665661 seconds / 184.91 hours / 7.70 days
Time on solved instances: 132861 seconds (42521 SAT + 90341 UNSAT)
Instances solved in 10 minutes: 115 (11927 seconds)
Instances solved in 15 minutes: 128 (21386 seconds)
Instances solved in 20 minutes: 140 (33447 seconds)
Instances solved in 30 minutes: 150 (48583 seconds)
Instances solved in 60 minutes: 170 (99807 seconds)
Instances solved in 90 minutes: 174 (116048 seconds)
Instances solved and time on solved instances by group:
dlx_iq_unsat_1.0 | 32 | / | 32 | 64061.5 | ||
engine_unsat_1.0 | 7 | / | 10 | 1353.96 | ||
fvp-sat.3.0 | 18 | / | 20 | 4680.65 | ||
fvp-unsat.1.0 | 4 | / | 4 | 44.15 | ||
fvp-unsat.2.0 | 22 | / | 22 | 1063.88 | ||
fvp-unsat.3.0 | 0 | / | 6 | 0 | ||
liveness_sat_1.0 | 5 | / | 10 | 3573.46 | ||
liveness_unsat_1.0 | 4 | / | 12 | 1041.86 | ||
liveness_unsat_2.0 | 3 | / | 9 | 63.08 | ||
npe-1.0 | 4 | / | 6 | 6737.99 | ||
pipe_ooo_unsat_1.0 | 7 | / | 15 | 5625.03 | ||
pipe_ooo_unsat_1.1 | 8 | / | 14 | 4682.38 | ||
pipe_sat_1.0 | 9 | / | 10 | 2553.35 | ||
pipe_sat_1.1 | 10 | / | 10 | 6324.41 | ||
pipe_unsat_1.0 | 8 | / | 13 | 1361.06 | ||
pipe_unsat_1.1 | 11 | / | 14 | 12709.8 | ||
vliw_sat_2.0 | 9 | / | 9 | 7982.38 | ||
vliw_sat_2.1 | 3 | / | 10 | 3858.49 | ||
vliw_sat_4.0 | 10 | / | 10 | 1524.69 | ||
vliw_unsat_2.0 | 2 | / | 9 | 2707.5 | ||
vliw_unsat_3.0 | 0 | / | 2 | 0 | ||
vliw_unsat_4.0 | 1 | / | 4 | 911.85 |
dlx_iq_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_iq42_a.cnf | 260240 | 3617585 | 6062733 | 252843 | 29 | 1030.39 | UNSAT |
1dlx_c_iq43_a.cnf | 276124 | 3861235 | 5896014 | 233973 | 29 | 999.25 | UNSAT |
1dlx_c_iq44_a.cnf | 292635 | 4115946 | 7120855 | 237899 | 29 | 1075.17 | UNSAT |
1dlx_c_iq45_a.cnf | 309785 | 4381995 | 7269174 | 232555 | 29 | 1117.18 | UNSAT |
1dlx_c_iq46_a.cnf | 327586 | 4659661 | 8147647 | 257781 | 29 | 1363.75 | UNSAT |
1dlx_c_iq47_a.cnf | 346050 | 4949225 | 8688937 | 261282 | 29 | 1451.59 | UNSAT |
1dlx_c_iq48_a.cnf | 365189 | 5250970 | 9619836 | 297307 | 30 | 1645.16 | UNSAT |
1dlx_c_iq49_a.cnf | 385015 | 5565181 | 10114867 | 276389 | 30 | 1656.01 | UNSAT |
1dlx_c_iq50_a.cnf | 405540 | 5892145 | 11654930 | 335971 | 33 | 1990.11 | UNSAT |
1dlx_c_iq51_a.cnf | 426776 | 6232151 | 11763201 | 292640 | 30 | 1974.90 | UNSAT |
1dlx_c_iq33_a.cnf | 143519 | 1877765 | 2600497 | 159065 | 20 | 379.52 | UNSAT |
1dlx_c_iq52_a.cnf | 448735 | 6585490 | 14041731 | 372351 | 37 | 2468.16 | UNSAT |
1dlx_c_iq53_a.cnf | 471429 | 6952455 | 13189541 | 316745 | 30 | 2289.33 | UNSAT |
1dlx_c_iq54_a.cnf | 663574 | 15489863 | 13654201 | 382254 | 39 | 3545.02 | UNSAT |
1dlx_c_iq55_a.cnf | 519070 | 7728445 | 15370318 | 372583 | 37 | 2796.01 | UNSAT |
1dlx_c_iq56_a.cnf | 544041 | 8138066 | 16977236 | 332949 | 32 | 2795.80 | UNSAT |
1dlx_c_iq57_a.cnf | 569795 | 8562505 | 17446206 | 376532 | 37 | 3031.53 | UNSAT |
1dlx_c_iq58_a.cnf | 596344 | 9002065 | 17015284 | 395161 | 41 | 3491.09 | UNSAT |
1dlx_c_iq59_a.cnf | 623700 | 9457051 | 21187150 | 459396 | 46 | 3943.28 | UNSAT |
1dlx_c_iq60_a.cnf | 651875 | 9927770 | 20577763 | 476300 | 49 | 4106.37 | UNSAT |
1dlx_c_iq61_a.cnf | 673311 | 10435991 | 14574225 | 334946 | 32 | 3102.83 | SAT |
1dlx_c_iq34_a.cnf | 154300 | 2034001 | 2941719 | 164828 | 21 | 418.14 | UNSAT |
1dlx_c_iq62_a.cnf | 710730 | 10917645 | 23130275 | 453599 | 45 | 4577.97 | UNSAT |
1dlx_c_iq63_a.cnf | 720715 | 11606548 | 9178668 | 215135 | 28 | 2170.85 | SAT |
1dlx_c_iq64_a.cnf | 773005 | 11974186 | 26417416 | 524637 | 56 | 5602.93 | UNSAT |
1dlx_c_iq35_a.cnf | 165600 | 2198895 | 2999130 | 158492 | 20 | 435.99 | UNSAT |
1dlx_c_iq36_a.cnf | 228994 | 4194027 | 3945895 | 202028 | 26 | 747.20 | UNSAT |
1dlx_c_iq37_a.cnf | 245646 | 4568332 | 3811853 | 211486 | 27 | 815.24 | UNSAT |
1dlx_c_iq38_a.cnf | 202734 | 2748125 | 4087962 | 181628 | 22 | 580.07 | UNSAT |
1dlx_c_iq39_a.cnf | 216230 | 2950261 | 4317246 | 215039 | 28 | 748.67 | UNSAT |
1dlx_c_iq40_a.cnf | 230305 | 3162370 | 5332562 | 248954 | 29 | 917.66 | UNSAT |
1dlx_c_iq41_a.cnf | 244971 | 3384721 | 5152621 | 202086 | 26 | 794.33 | UNSAT |
Total (32 / 32) | 344287693 | 9434834 | 1025 | 64061.5 |
engine_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
engine_4.cnf | 6944 | 66654 | 42273 | 27494 | 5 | 9.17 | UNSAT |
engine_4_nd.cnf | 7000 | 67586 | 126556 | 92984 | 13 | 55.08 | UNSAT |
engine_5.cnf | 18788 | 214095 | 584189 | 448174 | 45 | 904.60 | UNSAT |
engine_5_case1.cnf | 18810 | 214185 | 18576 | 12148 | 2 | 6.71 | UNSAT |
engine_5_nd.cnf | 18878 | 216156 | |||||
engine_5_nd_case1.cnf | 18900 | 216246 | 47133 | 33220 | 6 | 19.55 | UNSAT |
engine_6.cnf | 45276 | 605958 | |||||
engine_6_case1.cnf | 45303 | 606068 | 64681 | 46637 | 6 | 55.63 | UNSAT |
engine_6_nd.cnf | 45408 | 610010 | |||||
engine_6_nd_case1.cnf | 45435 | 610120 | 234530 | 181062 | 22 | 303.22 | UNSAT |
Total (7 / 10) | 1117938 | 841719 | 99 | 1353.96 |
fvp-sat.3.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
pipe_64_4_bug01.cnf | 35853 | 1012270 | 484572 | 34995 | 6 | 18.77 | SAT |
pipe_64_4_bug02.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug03.cnf | 35947 | 992674 | 105173 | 4397 | 1 | 3.69 | SAT |
pipe_64_4_bug04.cnf | 35854 | 1012315 | 88157 | 5463 | 1 | 6.05 | SAT |
pipe_64_4_bug05.cnf | 35853 | 1012271 | 4623803 | 705682 | 62 | 740.39 | SAT |
pipe_64_4_bug06.cnf | 35853 | 1012271 | 410181 | 40751 | 6 | 20.96 | SAT |
pipe_64_4_bug07.cnf | 35853 | 1012271 | 1471169 | 225961 | 28 | 125.63 | SAT |
pipe_64_4_bug08.cnf | 35622 | 1003074 | 733870 | 75532 | 12 | 35.26 | SAT |
pipe_64_4_bug09.cnf | 35726 | 1011764 | 676348 | 101802 | 14 | 43.27 | SAT |
pipe_64_4_bug10.cnf | 35839 | 1012135 | 498666 | 68205 | 10 | 28.92 | SAT |
pipe_64_4_bug11.cnf | 35853 | 1012271 | 1915123 | 279127 | 30 | 170.40 | SAT |
pipe_64_4_bug12.cnf | 35854 | 1012275 | 862861 | 138984 | 16 | 65.59 | SAT |
pipe_64_4_bug13.cnf | 35855 | 1012302 | 429411 | 78388 | 12 | 29.83 | SAT |
pipe_64_4_bug14.cnf | 35855 | 1012407 | 727792 | 115821 | 14 | 51.19 | SAT |
pipe_64_4_bug15.cnf | 35853 | 1012271 | 2309258 | 358694 | 36 | 234.99 | SAT |
pipe_64_4_bug16.cnf | 35853 | 1012271 | |||||
pipe_64_4_bug17.cnf | 35853 | 1012271 | 3954963 | 723273 | 62 | 696.96 | SAT |
pipe_64_4_bug18.cnf | 35853 | 1012271 | 9718225 | 1277650 | 114 | 1867.18 | SAT |
pipe_64_4_bug19.cnf | 35852 | 1012266 | 1352765 | 212722 | 27 | 111.39 | SAT |
pipe_64_4_bug20.cnf | 35853 | 1012271 | 2887466 | 540321 | 58 | 430.18 | SAT |
Total (18 / 20) | 33249803 | 4987768 | 509 | 4680.65 |
fvp-unsat.1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_mc_ex_bp_f.cnf | 776 | 3725 | 2284 | 670 | 0 | 0.02 | UNSAT |
2dlx_ca_mc_ex_bp_f.cnf | 3250 | 24640 | 22521 | 4803 | 1 | 0.44 | UNSAT |
2dlx_cc_mc_ex_bp_f.cnf | 4583 | 41704 | 31692 | 9108 | 2 | 1.13 | UNSAT |
9vliw_bp_mc.cnf | 20093 | 179492 | 503617 | 101399 | 14 | 42.56 | UNSAT |
Total (4 / 4) | 560114 | 115980 | 17 | 44.15 |
fvp-unsat.2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
2pipe.cnf | 892 | 6695 | 3014 | 1170 | 0 | 0.04 | UNSAT |
2pipe_1_ooo.cnf | 834 | 7026 | 2509 | 1089 | 0 | 0.04 | UNSAT |
2pipe_2_ooo.cnf | 925 | 8213 | 2895 | 1371 | 0 | 0.06 | UNSAT |
3pipe.cnf | 2468 | 27533 | 20605 | 6981 | 1 | 0.59 | UNSAT |
3pipe_1_ooo.cnf | 2223 | 26561 | 12741 | 6184 | 1 | 0.52 | UNSAT |
3pipe_2_ooo.cnf | 2400 | 29981 | 18264 | 8602 | 2 | 0.78 | UNSAT |
3pipe_3_ooo.cnf | 2577 | 33270 | 21524 | 9464 | 2 | 1.05 | UNSAT |
4pipe.cnf | 5237 | 80213 | 71742 | 23938 | 4 | 4.61 | UNSAT |
4pipe_1_ooo.cnf | 4647 | 74554 | 52902 | 21271 | 4 | 4.76 | UNSAT |
4pipe_2_ooo.cnf | 4941 | 82207 | 80673 | 34142 | 6 | 8.49 | UNSAT |
4pipe_3_ooo.cnf | 5233 | 89473 | 79310 | 30208 | 5 | 7.72 | UNSAT |
4pipe_4_ooo.cnf | 5525 | 96480 | 100064 | 40828 | 6 | 11.77 | UNSAT |
5pipe.cnf | 9471 | 195452 | 100069 | 19271 | 3 | 6.22 | UNSAT |
5pipe_1_ooo.cnf | 8441 | 187545 | 118220 | 40062 | 6 | 19.99 | UNSAT |
5pipe_2_ooo.cnf | 8851 | 201796 | 157343 | 53649 | 8 | 31.69 | UNSAT |
5pipe_3_ooo.cnf | 9267 | 215440 | 120852 | 35380 | 6 | 19.15 | UNSAT |
5pipe_4_ooo.cnf | 9764 | 221405 | 308043 | 120331 | 14 | 77.43 | UNSAT |
5pipe_5_ooo.cnf | 10113 | 240892 | 135978 | 39057 | 6 | 20.89 | UNSAT |
6pipe.cnf | 15800 | 394739 | 500127 | 142502 | 17 | 123.69 | UNSAT |
6pipe_6_ooo.cnf | 17064 | 545612 | 456341 | 126312 | 14 | 150.85 | UNSAT |
7pipe.cnf | 23910 | 751118 | 1210290 | 345565 | 34 | 531.92 | UNSAT |
7pipe_bug.cnf | 24065 | 731850 | 248954 | 50051 | 7 | 41.62 | SAT |
Total (22 / 22) | 3822460 | 1157428 | 146 | 1063.88 |
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 | 1443698 | 365758 | 37 | 1966.45 | 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 | |||||
2dlx_cc_ex_bp_f_bug10_liveness.cnf | 536469 | 10122798 | |||||
2dlx_cc_ex_bp_f_bug1_liveness.cnf | 171648 | 2614464 | 156626 | 22503 | 4 | 83.29 | SAT |
2dlx_cc_ex_bp_f_bug2_liveness.cnf | 196655 | 3068742 | 64732 | 6045 | 1 | 34.49 | SAT |
2dlx_cc_ex_bp_f_bug3_liveness.cnf | 224920 | 3596474 | 590490 | 125592 | 14 | 530.17 | SAT |
2dlx_cc_ex_bp_f_bug4_liveness.cnf | 256697 | 4205986 | 947074 | 200904 | 26 | 959.06 | SAT |
Total (5 / 10) | 3202620 | 720802 | 82 | 3573.46 |
liveness_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_f_liveness.cnf | 9474 | 107213 | 140509 | 73957 | 12 | 43.08 | UNSAT |
1dlx_c_ex_bp_f_liveness.cnf | 24104 | 339857 | 701955 | 409430 | 43 | 966.06 | UNSAT |
1dlx_c_ex_liveness.cnf | 18274 | 202528 | 102533 | 44952 | 6 | 28.96 | UNSAT |
1dlx_c_liveness.cnf | 6128 | 65112 | 34117 | 16362 | 2 | 3.76 | 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) | 979114 | 544701 | 63 | 1041.86 |
liveness_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bp_u_f_liveness.cnf | 6874 | 65479 | 43405 | 16493 | 3 | 3.60 | UNSAT |
1dlx_c_ex_bp_u_f_liveness.cnf | 14628 | 161477 | 145184 | 66133 | 10 | 36.92 | UNSAT |
1dlx_c_ex_d_liveness.cnf | 16011 | 210685 | 95075 | 41679 | 6 | 22.56 | 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) | 283664 | 124305 | 19 | 63.08 |
npe-1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
1dlx_c_bug_no_pe.cnf | 3295 | 35409 | 20718 | 11729 | 2 | 1.77 | SAT |
1dlx_c_no_pe.cnf | 3295 | 35410 | 104147 | 70403 | 11 | 29.97 | UNSAT |
2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf | 96675 | 1401773 | 777442 | 338655 | 33 | 1108.33 | SAT |
2dlx_cc_mc_ex_bp_f2_no_pe.cnf | 96675 | 1401773 | |||||
9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf | 889302 | 14582074 | 4271991 | 432773 | 45 | 5597.92 | SAT |
9dlx_vliw_at_bp_mc2_no_pe.cnf | 889302 | 14582081 | |||||
Total (4 / 6) | 5174298 | 853560 | 91 | 6737.99 |
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 | 2570 | 1394 | 0 | 0.06 | UNSAT |
3pipe_3_ooo.cnf | 2533 | 32182 | 24035 | 10393 | 2 | 1.09 | UNSAT |
4pipe_4_ooo.cnf | 5356 | 89506 | 103711 | 44263 | 6 | 12.03 | UNSAT |
5pipe_5_ooo.cnf | 9705 | 200959 | 302404 | 112555 | 14 | 59.14 | UNSAT |
6pipe_6_ooo.cnf | 15948 | 397032 | 767417 | 267044 | 30 | 272.37 | UNSAT |
7pipe_7_ooo.cnf | 24415 | 711050 | 2232973 | 799000 | 65 | 1666.94 | UNSAT |
8pipe_8_ooo.cnf | 35510 | 1191215 | |||||
9pipe_9_ooo.cnf | 49309 | 1924020 | 4324720 | 1177727 | 103 | 3613.40 | UNSAT |
Total (7 / 15) | 7757830 | 2412376 | 220 | 5625.03 |
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 | 3236 | 1517 | 0 | 0.05 | UNSAT |
3pipe_3_ooo_q0_T0.cnf | 2566 | 25625 | 23746 | 9390 | 2 | 0.81 | UNSAT |
4pipe_4_ooo_q0_T0.cnf | 5605 | 70042 | 79115 | 27767 | 5 | 5.40 | UNSAT |
5pipe_5_ooo_q0_T0.cnf | 10482 | 156027 | 283849 | 96090 | 13 | 42.65 | UNSAT |
6pipe_6_ooo_q0_T0.cnf | 17710 | 304026 | 702976 | 170000 | 21 | 126.54 | UNSAT |
7pipe_7_ooo_q0_T0.cnf | 27846 | 538853 | 1738575 | 490052 | 51 | 793.56 | UNSAT |
8pipe_8_ooo_q0_T0.cnf | 41491 | 889823 | 3606261 | 935886 | 81 | 2578.78 | UNSAT |
9pipe_9_ooo_q0_T0.cnf | 59024 | 1430330 | 2686326 | 512433 | 54 | 1134.59 | UNSAT |
Total (8 / 14) | 9124084 | 2243135 | 227 | 4682.38 |
pipe_sat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug1.cnf | 118040 | 8804672 | 38089 | 1346 | 0 | 18.97 | SAT |
12pipe_bug10.cnf | 118040 | 8804672 | 183242 | 28302 | 5 | 114.79 | SAT |
12pipe_bug2.cnf | 118040 | 8804630 | 82673 | 8917 | 2 | 37.71 | SAT |
12pipe_bug3.cnf | 118039 | 8804669 | |||||
12pipe_bug4.cnf | 117504 | 8743027 | 1778651 | 350028 | 35 | 1352.76 | SAT |
12pipe_bug5.cnf | 118040 | 8804672 | 1167607 | 265036 | 30 | 898.58 | SAT |
12pipe_bug6.cnf | 117665 | 8647068 | 5477 | 0 | 0 | 16.30 | SAT |
12pipe_bug7.cnf | 118040 | 8804672 | 75460 | 6396 | 1 | 36.26 | SAT |
12pipe_bug8.cnf | 117526 | 8760516 | 154816 | 16387 | 3 | 59.63 | SAT |
12pipe_bug9.cnf | 118038 | 8780591 | 35742 | 1114 | 0 | 18.35 | SAT |
Total (9 / 10) | 3521757 | 677526 | 76 | 2553.35 |
pipe_sat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
12pipe_bug10_q0.cnf | 138918 | 4678760 | 1136222 | 188640 | 24 | 497.08 | SAT |
12pipe_bug1_q0.cnf | 138917 | 4678756 | 2714761 | 445265 | 45 | 1312.57 | SAT |
12pipe_bug2_q0.cnf | 138918 | 4678718 | 474205 | 65981 | 10 | 183.16 | SAT |
12pipe_bug3_q0.cnf | 138917 | 4678757 | 1380852 | 231092 | 29 | 630.84 | SAT |
12pipe_bug4_q0.cnf | 138563 | 4675040 | 479650 | 82904 | 13 | 227.46 | SAT |
12pipe_bug5_q0.cnf | 138918 | 4678760 | 1406414 | 244031 | 29 | 642.62 | SAT |
12pipe_bug6_q0.cnf | 138795 | 4671352 | 382150 | 57375 | 9 | 156.38 | SAT |
12pipe_bug7_q0.cnf | 138918 | 4678760 | 1818366 | 334016 | 32 | 936.82 | SAT |
12pipe_bug8_q0.cnf | 138711 | 4688614 | 255572 | 19303 | 3 | 75.37 | SAT |
12pipe_bug9_q0.cnf | 138916 | 4676007 | 3108721 | 543063 | 59 | 1662.11 | SAT |
Total (10 / 10) | 13156913 | 2211670 | 253 | 6324.41 |
pipe_unsat_1.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_k.cnf | 860 | 6693 | 2930 | 1220 | 0 | 0.05 | UNSAT |
03pipe_k.cnf | 2391 | 27405 | 18579 | 6343 | 1 | 0.53 | UNSAT |
04pipe_k.cnf | 5095 | 79489 | 77934 | 27405 | 5 | 5.93 | UNSAT |
05pipe_k.cnf | 9330 | 189109 | 331583 | 129777 | 14 | 85.43 | UNSAT |
06pipe_k.cnf | 15346 | 408792 | 213090 | 27149 | 5 | 13.27 | UNSAT |
07pipe_k.cnf | 23909 | 751116 | 1021995 | 267778 | 30 | 350.44 | UNSAT |
08pipe_k.cnf | 35065 | 1332773 | 1740203 | 341218 | 33 | 579.61 | UNSAT |
09pipe_k.cnf | 49112 | 2317839 | 1680879 | 117493 | 14 | 325.80 | 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) | 5087193 | 918383 | 102 | 1361.06 |
pipe_unsat_1.1
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
02pipe_q0_k.cnf | 873 | 6457 | 2794 | 1086 | 0 | 0.04 | UNSAT |
03pipe_q0_k.cnf | 2476 | 25181 | 21364 | 8058 | 1 | 0.62 | UNSAT |
04pipe_q0_k.cnf | 5380 | 69072 | 72848 | 26093 | 5 | 4.53 | UNSAT |
05pipe_q0_k.cnf | 10026 | 154409 | 187961 | 62396 | 9 | 19.63 | UNSAT |
06pipe_q0_k.cnf | 16775 | 315960 | 197647 | 37217 | 6 | 16.71 | UNSAT |
07pipe_q0_k.cnf | 26512 | 536414 | 792850 | 182984 | 22 | 137.03 | UNSAT |
08pipe_q0_k.cnf | 39434 | 887706 | 1545098 | 367357 | 37 | 456.87 | UNSAT |
09pipe_q0_k.cnf | 55996 | 1468197 | 1114332 | 109085 | 14 | 130.75 | UNSAT |
10pipe_q0_k.cnf | 77639 | 2082017 | 4555003 | 1125334 | 96 | 2867.88 | UNSAT |
11pipe_q0_k.cnf | 104244 | 3007883 | 6237975 | 1187564 | 105 | 3462.94 | UNSAT |
12pipe_q0_k.cnf | 136800 | 4216460 | 9524670 | 1546338 | 125 | 5612.80 | UNSAT |
13pipe_q0_k.cnf | 176066 | 5761591 | |||||
14pipe_q0_k.cnf | 222845 | 7702617 | |||||
15pipe_q0_k.cnf | 277976 | 10103924 | |||||
Total (11 / 14) | 24252542 | 4653512 | 420 | 12709.8 |
vliw_sat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq6_bug1.cnf | 236038 | 8084666 | 6499699 | 487147 | 51 | 1282.44 | SAT |
9dlx_vliw_at_b_iq6_bug2.cnf | 235928 | 8076545 | 120421 | 59 | 0 | 17.18 | SAT |
9dlx_vliw_at_b_iq6_bug3.cnf | 235402 | 8060882 | 4045967 | 218649 | 28 | 602.88 | SAT |
9dlx_vliw_at_b_iq6_bug4.cnf | 235277 | 8063780 | 7880984 | 698588 | 62 | 1948.58 | SAT |
9dlx_vliw_at_b_iq6_bug5.cnf | 235923 | 8076534 | 4292403 | 242866 | 29 | 606.81 | SAT |
9dlx_vliw_at_b_iq6_bug6.cnf | 235926 | 8076539 | 1255098 | 8864 | 2 | 53.82 | SAT |
9dlx_vliw_at_b_iq6_bug7.cnf | 173811 | 5609632 | 2491267 | 167263 | 21 | 329.43 | SAT |
9dlx_vliw_at_b_iq6_bug8.cnf | 229942 | 7882655 | 3040478 | 100140 | 14 | 251.07 | SAT |
9dlx_vliw_at_b_iq6_bug9.cnf | 235184 | 8063818 | 8073885 | 955323 | 84 | 2890.17 | SAT |
Total (9 / 9) | 37700202 | 2878899 | 291 | 7982.38 |
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 | 9385821 | 443478 | 45 | 1742.91 | SAT |
9dlx_vliw_at_b_iq8_bug4.cnf | 409220 | 15574959 | 9990203 | 532402 | 57 | 2019.17 | 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 | 1628151 | 8822 | 2 | 96.41 | SAT |
9dlx_vliw_at_b_iq8_bug8.cnf | 410560 | 15603495 | |||||
9dlx_vliw_at_b_iq8_bug9.cnf | 449867 | 16331249 | |||||
Total (3 / 10) | 21004175 | 984702 | 104 | 3858.49 |
vliw_sat_4.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9vliw_m_9stages_iq3_C1_bug1.cnf | 521188 | 13378641 | 6442775 | 14246 | 2 | 130.31 | SAT |
9vliw_m_9stages_iq3_C1_bug10.cnf | 521182 | 13378625 | 8657815 | 63541 | 9 | 319.72 | SAT |
9vliw_m_9stages_iq3_C1_bug2.cnf | 521158 | 13378532 | 5669526 | 6846 | 1 | 90.92 | SAT |
9vliw_m_9stages_iq3_C1_bug3.cnf | 521046 | 13376161 | 4447142 | 2098 | 0 | 58.71 | SAT |
9vliw_m_9stages_iq3_C1_bug4.cnf | 520721 | 13348117 | 5063005 | 16231 | 2 | 128.52 | SAT |
9vliw_m_9stages_iq3_C1_bug5.cnf | 520770 | 13380350 | 7571162 | 26734 | 5 | 198.62 | SAT |
9vliw_m_9stages_iq3_C1_bug6.cnf | 521192 | 13378781 | 8166537 | 24815 | 5 | 191.33 | SAT |
9vliw_m_9stages_iq3_C1_bug7.cnf | 521147 | 13378010 | 5756560 | 6840 | 1 | 94.84 | SAT |
9vliw_m_9stages_iq3_C1_bug8.cnf | 521179 | 13378617 | 5878058 | 14309 | 2 | 150.29 | SAT |
9vliw_m_9stages_iq3_C1_bug9.cnf | 521187 | 13378624 | 6239450 | 19667 | 3 | 161.43 | SAT |
Total (10 / 10) | 63892030 | 195327 | 30 | 1524.69 |
vliw_unsat_2.0
CNF | Vars | Clauses | Decisions | Conflicts | Restarts | Time | Sol |
9dlx_vliw_at_b_iq1.cnf | 24604 | 261473 | 2294572 | 673018 | 62 | 740.38 | UNSAT |
9dlx_vliw_at_b_iq2.cnf | 44095 | 542253 | 4948373 | 1201566 | 107 | 1967.12 | 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) | 7242945 | 1874584 | 169 | 2707.5 |
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 | 5054487 | 626013 | 61 | 911.85 | 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) | 5054487 | 626013 | 61 | 911.85 |