Solver: Clearn |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
Adder | 8 | 1 | 0.01 | 0 | 0 | 1 | 0.01 |
Blocks | 8 | 1 | 4.49 | 0 | 0 | 1 | 4.49 |
C432 | 8 | 3 | 297.33 | 3 | 297.33 | 0 | 0 |
C499 | 8 | 2 | 0.23 | 2 | 0.23 | 0 | 0 |
C5315 | 8 | 2 | 0.25 | 2 | 0.25 | 0 | 0 |
C880 | 8 | 2 | 87.65 | 2 | 87.65 | 0 | 0 |
Chain | 8 | 8 | 632.6 | 8 | 632.6 | 0 | 0 |
comp | 8 | 6 | 640.62 | 4 | 0.05 | 2 | 640.57 |
Connect2 | 8 | 8 | 5.65 | 5 | 4.55 | 3 | 1.1 |
Connect3 | 8 | 7 | 16.65 | 0 | 0 | 7 | 16.65 |
Connect4 | 8 | 7 | 2.96 | 0 | 0 | 7 | 2.96 |
Connect5 | 8 | 7 | 4.91 | 0 | 0 | 7 | 4.91 |
Connect6 | 8 | 5 | 99.91 | 0 | 0 | 5 | 99.91 |
Connect7 | 8 | 7 | 5.12 | 0 | 0 | 7 | 5.12 |
Connect8 | 8 | 5 | 5.24 | 0 | 0 | 5 | 5.24 |
Connect9 | 3 | 2 | 2.3 | 0 | 0 | 2 | 2.3 |
counter | 8 | 4 | 0.89 | 4 | 0.89 | 0 | 0 |
DFlipFlop | 8 | 8 | 3.16 | 0 | 0 | 8 | 3.16 |
Impl | 8 | 8 | 0.06 | 8 | 0.06 | 0 | 0 |
k_branch_n | 8 | 1 | 0.01 | 1 | 0.01 | 0 | 0 |
k_branch_p | 8 | 1 | 1.82 | 0 | 0 | 1 | 1.82 |
k_d4_p | 8 | 2 | 390.8 | 0 | 0 | 2 | 390.8 |
k_dum_n | 8 | 6 | 798.72 | 6 | 798.72 | 0 | 0 |
k_dum_p | 8 | 4 | 602.58 | 0 | 0 | 4 | 602.58 |
k_grz_n | 8 | 5 | 474.89 | 5 | 474.89 | 0 | 0 |
k_grz_p | 8 | 7 | 1970.09 | 0 | 0 | 7 | 1970.09 |
k_lin_n | 8 | 5 | 59.19 | 5 | 59.19 | 0 | 0 |
k_lin_p | 8 | 8 | 44.85 | 0 | 0 | 8 | 44.85 |
k_path_n | 8 | 5 | 385.31 | 5 | 385.31 | 0 | 0 |
k_path_p | 8 | 3 | 34.11 | 0 | 0 | 3 | 34.11 |
k_ph_n | 8 | 7 | 131.85 | 7 | 131.85 | 0 | 0 |
k_ph_p | 8 | 3 | 4.91 | 0 | 0 | 3 | 4.91 |
k_poly_n | 8 | 2 | 403.07 | 2 | 403.07 | 0 | 0 |
k_poly_p | 8 | 1 | 4.68 | 0 | 0 | 1 | 4.68 |
k_t4p_n | 8 | 1 | 41.15 | 1 | 41.15 | 0 | 0 |
k_t4p_p | 8 | 2 | 336.75 | 0 | 0 | 2 | 336.75 |
Logn | 4 | 2 | 66.67 | 0 | 0 | 2 | 66.67 |
mA-t2-2qbf-5cnf-100var | 18 | 7 | 834.71 | 1 | 724.2 | 6 | 110.51 |
mA-t2-2qbf-5cnf-150var | 18 | 5 | 840.69 | 1 | 594.76 | 4 | 245.93 |
mA-t2-2qbf-5cnf-50var | 18 | 11 | 19.93 | 2 | 0.09 | 9 | 19.84 |
mA-t2-3qbf-5cnf-100var | 18 | 10 | 257.62 | 6 | 0.05 | 4 | 257.57 |
mA-t2-3qbf-5cnf-150var | 18 | 8 | 520.57 | 6 | 3.09 | 2 | 517.48 |
mA-t2-3qbf-5cnf-50var | 18 | 15 | 187.29 | 8 | 6.93 | 7 | 180.36 |
mA-t2-4qbf-5cnf-100var | 18 | 11 | 280.89 | 2 | 0.02 | 9 | 280.87 |
mA-t2-4qbf-5cnf-150var | 18 | 11 | 809.96 | 2 | 0.01 | 9 | 809.95 |
mA-t2-4qbf-5cnf-50var | 18 | 14 | 20.93 | 4 | 19.96 | 10 | 0.97 |
mA-t2-5qbf-5cnf-100var | 18 | 8 | 296.53 | 7 | 216.11 | 1 | 80.42 |
mA-t2-5qbf-5cnf-150var | 18 | 7 | 364.34 | 6 | 0.09 | 1 | 364.25 |
mA-t2-5qbf-5cnf-50var | 18 | 15 | 499.15 | 9 | 48.51 | 6 | 450.64 |
mB-t2-2qbf-5cnf-100var | 18 | 18 | 332.83 | 1 | 325.31 | 17 | 7.52 |
mB-t2-2qbf-5cnf-150var | 18 | 18 | 0.53 | 0 | 0 | 18 | 0.53 |
mB-t2-2qbf-5cnf-50var | 18 | 18 | 0.38 | 1 | 0.04 | 17 | 0.34 |
mB-t2-3qbf-5cnf-100var | 18 | 18 | 0.19 | 2 | 0.01 | 16 | 0.18 |
mB-t2-3qbf-5cnf-150var | 18 | 18 | 0.31 | 2 | 0.02 | 16 | 0.29 |
mB-t2-3qbf-5cnf-50var | 18 | 18 | 0.12 | 2 | 0.02 | 16 | 0.1 |
mB-t2-4qbf-5cnf-100var | 18 | 18 | 0.19 | 2 | 0.02 | 16 | 0.17 |
mB-t2-4qbf-5cnf-150var | 18 | 18 | 0.28 | 2 | 0.01 | 16 | 0.27 |
mB-t2-4qbf-5cnf-50var | 18 | 18 | 0.06 | 2 | 0.01 | 16 | 0.05 |
mB-t2-5qbf-5cnf-100var | 18 | 18 | 0.19 | 2 | 0.01 | 16 | 0.18 |
mB-t2-5qbf-5cnf-150var | 18 | 18 | 0.25 | 2 | 0.01 | 16 | 0.24 |
mB-t2-5qbf-5cnf-50var | 18 | 18 | 0.05 | 4 | 0 | 14 | 0.05 |
MutexP | 7 | 3 | 1.75 | 3 | 1.75 | 0 | 0 |
RobotsD2 | 8 | 8 | 1240.64 | 6 | 111.58 | 2 | 1129.06 |
RobotsD3 | 8 | 3 | 182.79 | 3 | 182.79 | 0 | 0 |
RobotsD4 | 8 | 6 | 331.28 | 5 | 110.01 | 1 | 221.27 |
RobotsD5 | 8 | 7 | 1148.76 | 4 | 37.88 | 3 | 1110.88 |
s27 | 4 | 2 | 103.5 | 0 | 0 | 2 | 103.5 |
SzymanskiP | 8 | 8 | 63.32 | 0 | 0 | 8 | 63.32 |
term1 | 8 | 7 | 661.99 | 4 | 1.42 | 3 | 660.57 |
Toilet | 8 | 8 | 122.29 | 5 | 0.11 | 3 | 122.18 |
ToiletA | 8 | 8 | 1.92 | 1 | 0.37 | 7 | 1.55 |
ToiletC | 8 | 8 | 0.22 | 3 | 0.03 | 5 | 0.19 |
ToiletG | 7 | 7 | 0.05 | 7 | 0.05 | 0 | 0 |
Tree | 8 | 7 | 130.24 | 1 | 130.24 | 6 | 0 |
VonNeumann | 8 | 7 | 15.02 | 0 | 0 | 7 | 15.02 |
z4ml | 8 | 8 | 0.08 | 4 | 0.03 | 4 | 0.05 |
Solved Families: 76 |
Solver: CSBJ |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
Adder | 8 | 1 | 0.02 | 0 | 0 | 1 | 0.02 |
C432 | 8 | 3 | 181.83 | 3 | 181.83 | 0 | 0 |
C499 | 8 | 2 | 0.25 | 2 | 0.25 | 0 | 0 |
C5315 | 8 | 2 | 0.26 | 2 | 0.26 | 0 | 0 |
C880 | 8 | 1 | 0.3 | 1 | 0.3 | 0 | 0 |
Chain | 8 | 8 | 641.2 | 8 | 641.2 | 0 | 0 |
comp | 8 | 8 | 794.65 | 4 | 0.06 | 4 | 794.59 |
Connect2 | 8 | 8 | 5.63 | 5 | 4.54 | 3 | 1.09 |
Connect3 | 8 | 7 | 21.6 | 0 | 0 | 7 | 21.6 |
Connect4 | 8 | 7 | 2.95 | 0 | 0 | 7 | 2.95 |
Connect5 | 8 | 7 | 6.33 | 0 | 0 | 7 | 6.33 |
Connect6 | 8 | 4 | 2.32 | 0 | 0 | 4 | 2.32 |
Connect7 | 8 | 7 | 5.11 | 0 | 0 | 7 | 5.11 |
Connect8 | 8 | 5 | 5.22 | 0 | 0 | 5 | 5.22 |
Connect9 | 3 | 2 | 2.29 | 0 | 0 | 2 | 2.29 |
counter | 8 | 3 | 64.26 | 3 | 64.26 | 0 | 0 |
DFlipFlop | 8 | 8 | 3.16 | 0 | 0 | 8 | 3.16 |
Impl | 8 | 8 | 0.06 | 8 | 0.06 | 0 | 0 |
k_branch_n | 8 | 1 | 0.02 | 1 | 0.02 | 0 | 0 |
k_d4_p | 8 | 1 | 204.5 | 0 | 0 | 1 | 204.5 |
k_dum_n | 8 | 2 | 155.88 | 2 | 155.88 | 0 | 0 |
k_dum_p | 8 | 1 | 2.16 | 0 | 0 | 1 | 2.16 |
k_grz_n | 8 | 2 | 427.34 | 2 | 427.34 | 0 | 0 |
k_grz_p | 8 | 2 | 429.58 | 0 | 0 | 2 | 429.58 |
k_lin_n | 8 | 3 | 2.85 | 3 | 2.85 | 0 | 0 |
k_lin_p | 8 | 3 | 163.34 | 0 | 0 | 3 | 163.34 |
k_path_n | 8 | 3 | 343.28 | 3 | 343.28 | 0 | 0 |
k_path_p | 8 | 2 | 0.4 | 0 | 0 | 2 | 0.4 |
k_ph_n | 8 | 6 | 50.43 | 6 | 50.43 | 0 | 0 |
k_ph_p | 8 | 2 | 0.18 | 0 | 0 | 2 | 0.18 |
k_poly_n | 8 | 2 | 405.95 | 2 | 405.95 | 0 | 0 |
k_poly_p | 8 | 1 | 620.94 | 0 | 0 | 1 | 620.94 |
k_t4p_p | 8 | 1 | 55.29 | 0 | 0 | 1 | 55.29 |
mA-t2-2qbf-5cnf-100var | 18 | 8 | 946.53 | 1 | 744.82 | 7 | 201.71 |
mA-t2-2qbf-5cnf-150var | 18 | 5 | 651.59 | 1 | 608.1 | 4 | 43.49 |
mA-t2-2qbf-5cnf-50var | 18 | 12 | 269.29 | 2 | 0.09 | 10 | 269.2 |
mA-t2-3qbf-5cnf-100var | 18 | 8 | 560.08 | 6 | 0.1 | 2 | 559.98 |
mA-t2-3qbf-5cnf-150var | 18 | 5 | 14.65 | 5 | 14.65 | 0 | 0 |
mA-t2-3qbf-5cnf-50var | 18 | 14 | 808.75 | 8 | 29.34 | 6 | 779.41 |
mA-t2-4qbf-5cnf-100var | 18 | 8 | 820.87 | 2 | 0.02 | 6 | 820.85 |
mA-t2-4qbf-5cnf-150var | 18 | 6 | 815.05 | 2 | 0.01 | 4 | 815.04 |
mA-t2-4qbf-5cnf-50var | 18 | 14 | 43.43 | 4 | 20.31 | 10 | 23.12 |
mA-t2-5qbf-5cnf-100var | 18 | 6 | 0.03 | 6 | 0.03 | 0 | 0 |
mA-t2-5qbf-5cnf-150var | 18 | 6 | 0.06 | 6 | 0.06 | 0 | 0 |
mA-t2-5qbf-5cnf-50var | 18 | 12 | 699.35 | 9 | 304.49 | 3 | 394.86 |
mB-t2-2qbf-5cnf-100var | 18 | 18 | 323.62 | 1 | 316.24 | 17 | 7.38 |
mB-t2-2qbf-5cnf-150var | 18 | 18 | 0.58 | 0 | 0 | 18 | 0.58 |
mB-t2-2qbf-5cnf-50var | 18 | 18 | 0.45 | 1 | 0.05 | 17 | 0.4 |
mB-t2-3qbf-5cnf-100var | 18 | 18 | 0.1 | 2 | 0.01 | 16 | 0.09 |
mB-t2-3qbf-5cnf-150var | 18 | 18 | 0.15 | 2 | 0 | 16 | 0.15 |
mB-t2-3qbf-5cnf-50var | 18 | 18 | 0.01 | 2 | 0 | 16 | 0.01 |
mB-t2-4qbf-5cnf-100var | 18 | 18 | 0.19 | 2 | 0.02 | 16 | 0.17 |
mB-t2-4qbf-5cnf-150var | 18 | 18 | 0.28 | 2 | 0.02 | 16 | 0.26 |
mB-t2-4qbf-5cnf-50var | 18 | 18 | 0.15 | 2 | 0.02 | 16 | 0.13 |
mB-t2-5qbf-5cnf-100var | 18 | 18 | 0.22 | 2 | 0 | 16 | 0.22 |
mB-t2-5qbf-5cnf-150var | 18 | 18 | 0.53 | 2 | 0 | 16 | 0.53 |
mB-t2-5qbf-5cnf-50var | 18 | 18 | 0.1 | 4 | 0.01 | 14 | 0.09 |
MutexP | 7 | 3 | 1.74 | 3 | 1.74 | 0 | 0 |
RobotsD2 | 8 | 5 | 232.49 | 5 | 232.49 | 0 | 0 |
RobotsD3 | 8 | 1 | 48.36 | 1 | 48.36 | 0 | 0 |
RobotsD4 | 8 | 4 | 137.04 | 4 | 137.04 | 0 | 0 |
RobotsD5 | 8 | 4 | 454 | 4 | 454 | 0 | 0 |
s27 | 4 | 1 | 0.08 | 1 | 0.08 | 0 | 0 |
SzymanskiP | 8 | 8 | 62.86 | 0 | 0 | 8 | 62.86 |
term1 | 8 | 4 | 123.17 | 4 | 123.17 | 0 | 0 |
Toilet | 8 | 8 | 91.31 | 5 | 0.11 | 3 | 91.2 |
ToiletA | 8 | 8 | 42.86 | 1 | 0.37 | 7 | 42.49 |
ToiletC | 8 | 8 | 0.95 | 3 | 0.05 | 5 | 0.9 |
ToiletG | 7 | 7 | 0.07 | 7 | 0.07 | 0 | 0 |
Tree | 8 | 6 | 719.09 | 1 | 131.16 | 5 | 587.93 |
VonNeumann | 8 | 7 | 15.21 | 0 | 0 | 7 | 15.21 |
z4ml | 8 | 8 | 0.03 | 4 | 0.01 | 4 | 0.02 |
Solved Families: 72 |
Solver: eqube-bj |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
Adder | 8 | 1 | 0.96 | 0 | 0 | 1 | 0.96 |
Blocks | 8 | 3 | 13.03 | 2 | 11.56 | 1 | 1.47 |
C432 | 8 | 3 | 64.79 | 2 | 37.43 | 1 | 27.36 |
C499 | 8 | 2 | 3.98 | 2 | 3.98 | 0 | 0 |
C5315 | 8 | 1 | 1.11 | 1 | 1.11 | 0 | 0 |
C880 | 8 | 1 | 2.19 | 1 | 2.19 | 0 | 0 |
Chain | 8 | 6 | 598.08 | 6 | 598.08 | 0 | 0 |
comp | 8 | 6 | 18.58 | 4 | 7.4 | 2 | 11.18 |
Connect2 | 8 | 6 | 7.39 | 4 | 5.3 | 2 | 2.09 |
Connect3 | 8 | 2 | 68.56 | 0 | 0 | 2 | 68.56 |
Connect4 | 8 | 5 | 5.41 | 0 | 0 | 5 | 5.41 |
Connect5 | 8 | 6 | 493.59 | 0 | 0 | 6 | 493.59 |
Connect6 | 8 | 3 | 3.52 | 0 | 0 | 3 | 3.52 |
Connect7 | 8 | 5 | 6.33 | 0 | 0 | 5 | 6.33 |
Connect8 | 8 | 1 | 1.25 | 0 | 0 | 1 | 1.25 |
counter | 8 | 4 | 51.97 | 4 | 51.97 | 0 | 0 |
DFlipFlop | 8 | 8 | 9.47 | 0 | 0 | 8 | 9.47 |
Impl | 8 | 8 | 712.72 | 8 | 712.72 | 0 | 0 |
k_branch_n | 8 | 1 | 0.97 | 1 | 0.97 | 0 | 0 |
k_branch_p | 8 | 1 | 1.55 | 0 | 0 | 1 | 1.55 |
k_d4_p | 8 | 7 | 194.73 | 0 | 0 | 7 | 194.73 |
k_dum_n | 8 | 5 | 177.57 | 5 | 177.57 | 0 | 0 |
k_dum_p | 8 | 4 | 650.94 | 0 | 0 | 4 | 650.94 |
k_grz_n | 8 | 7 | 1413.74 | 7 | 1413.74 | 0 | 0 |
k_grz_p | 8 | 6 | 1405.42 | 0 | 0 | 6 | 1405.42 |
k_lin_n | 8 | 4 | 12.58 | 4 | 12.58 | 0 | 0 |
k_lin_p | 8 | 8 | 9.38 | 0 | 0 | 8 | 9.38 |
k_path_n | 8 | 5 | 406.04 | 5 | 406.04 | 0 | 0 |
k_path_p | 8 | 3 | 44.47 | 0 | 0 | 3 | 44.47 |
k_ph_n | 8 | 6 | 6.28 | 6 | 6.28 | 0 | 0 |
k_ph_p | 8 | 2 | 1.97 | 0 | 0 | 2 | 1.97 |
k_poly_n | 8 | 2 | 215.22 | 2 | 215.22 | 0 | 0 |
k_poly_p | 8 | 8 | 7.92 | 0 | 0 | 8 | 7.92 |
k_t4p_n | 8 | 1 | 61.43 | 1 | 61.43 | 0 | 0 |
k_t4p_p | 8 | 2 | 295.46 | 0 | 0 | 2 | 295.46 |
Logn | 4 | 3 | 353.56 | 0 | 0 | 3 | 353.56 |
mA-t2-2qbf-5cnf-100var | 18 | 16 | 234 | 1 | 1.56 | 15 | 232.44 |
mA-t2-2qbf-5cnf-150var | 18 | 11 | 45.49 | 0 | 0 | 11 | 45.49 |
mA-t2-2qbf-5cnf-50var | 18 | 18 | 64.57 | 2 | 1.95 | 16 | 62.62 |
mA-t2-3qbf-5cnf-100var | 18 | 18 | 88.55 | 7 | 8.85 | 11 | 79.7 |
mA-t2-3qbf-5cnf-150var | 18 | 18 | 1392.48 | 6 | 6.01 | 12 | 1386.47 |
mA-t2-3qbf-5cnf-50var | 18 | 17 | 22.84 | 7 | 6.87 | 10 | 15.97 |
mA-t2-4qbf-5cnf-100var | 18 | 18 | 218.67 | 2 | 1.98 | 16 | 216.69 |
mA-t2-4qbf-5cnf-150var | 18 | 16 | 259.71 | 2 | 1.99 | 14 | 257.72 |
mA-t2-4qbf-5cnf-50var | 18 | 18 | 21.77 | 4 | 3.99 | 14 | 17.78 |
mA-t2-5qbf-5cnf-100var | 18 | 18 | 878.05 | 7 | 10.52 | 11 | 867.53 |
mA-t2-5qbf-5cnf-150var | 18 | 16 | 871.29 | 8 | 8.32 | 8 | 862.97 |
mA-t2-5qbf-5cnf-50var | 18 | 18 | 28.95 | 8 | 7.89 | 10 | 21.06 |
mB-t2-2qbf-5cnf-100var | 18 | 18 | 23.55 | 1 | 6.7 | 17 | 16.85 |
mB-t2-2qbf-5cnf-150var | 18 | 18 | 17.71 | 0 | 0 | 18 | 17.71 |
mB-t2-2qbf-5cnf-50var | 18 | 18 | 17.72 | 1 | 1.01 | 17 | 16.71 |
mB-t2-3qbf-5cnf-100var | 18 | 18 | 17.78 | 2 | 1.96 | 16 | 15.82 |
mB-t2-3qbf-5cnf-150var | 18 | 18 | 17.61 | 2 | 1.95 | 16 | 15.66 |
mB-t2-3qbf-5cnf-50var | 18 | 18 | 17.58 | 2 | 1.94 | 16 | 15.64 |
mB-t2-4qbf-5cnf-100var | 18 | 18 | 17.58 | 2 | 1.94 | 16 | 15.64 |
mB-t2-4qbf-5cnf-150var | 18 | 18 | 17.65 | 2 | 1.94 | 16 | 15.71 |
mB-t2-4qbf-5cnf-50var | 18 | 18 | 17.59 | 2 | 1.95 | 16 | 15.64 |
mB-t2-5qbf-5cnf-100var | 18 | 18 | 17.64 | 2 | 1.96 | 16 | 15.68 |
mB-t2-5qbf-5cnf-150var | 18 | 18 | 17.64 | 2 | 1.95 | 16 | 15.69 |
mB-t2-5qbf-5cnf-50var | 18 | 18 | 17.56 | 4 | 3.89 | 14 | 13.67 |
MutexP | 7 | 3 | 4.64 | 3 | 4.64 | 0 | 0 |
RobotsD2 | 8 | 7 | 568.9 | 6 | 187.34 | 1 | 381.56 |
RobotsD3 | 8 | 5 | 737.82 | 3 | 350.91 | 2 | 386.91 |
RobotsD4 | 8 | 7 | 189.74 | 5 | 86.56 | 2 | 103.18 |
RobotsD5 | 8 | 8 | 76.75 | 4 | 4.49 | 4 | 72.26 |
s27 | 4 | 1 | 1.01 | 1 | 1.01 | 0 | 0 |
s3271 | 8 | 3 | 6.42 | 0 | 0 | 3 | 6.42 |
SzymanskiP | 8 | 8 | 75.7 | 0 | 0 | 8 | 75.7 |
term1 | 8 | 5 | 58 | 4 | 4.76 | 1 | 53.24 |
Toilet | 8 | 4 | 169.95 | 2 | 64.39 | 2 | 105.56 |
ToiletA | 8 | 7 | 82.35 | 1 | 1.06 | 6 | 81.29 |
ToiletC | 8 | 8 | 100.33 | 3 | 94.59 | 5 | 5.74 |
ToiletG | 7 | 7 | 6.77 | 7 | 6.77 | 0 | 0 |
Tree | 8 | 8 | 8.19 | 2 | 2.3 | 6 | 5.89 |
VonNeumann | 8 | 4 | 9.56 | 0 | 0 | 4 | 9.56 |
z4ml | 8 | 8 | 7.8 | 4 | 3.88 | 4 | 3.92 |
Solved Families: 76 |
Solver: eqube-lrn |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
Adder | 8 | 1 | 0.97 | 0 | 0 | 1 | 0.97 |
Blocks | 8 | 5 | 166.22 | 2 | 5.8 | 3 | 160.42 |
C432 | 8 | 5 | 328.83 | 3 | 35.21 | 2 | 293.62 |
C499 | 8 | 4 | 35.83 | 3 | 8.84 | 1 | 26.99 |
C5315 | 8 | 2 | 148.12 | 1 | 1.14 | 1 | 146.98 |
C880 | 8 | 2 | 153.29 | 2 | 153.29 | 0 | 0 |
Chain | 8 | 5 | 362.07 | 5 | 362.07 | 0 | 0 |
comp | 8 | 8 | 741.95 | 4 | 4.01 | 4 | 737.94 |
Connect2 | 8 | 6 | 7.35 | 4 | 5.21 | 2 | 2.14 |
Connect3 | 8 | 2 | 116.41 | 0 | 0 | 2 | 116.41 |
Connect4 | 8 | 5 | 5.44 | 0 | 0 | 5 | 5.44 |
Connect5 | 8 | 6 | 659.02 | 0 | 0 | 6 | 659.02 |
Connect6 | 8 | 3 | 3.49 | 0 | 0 | 3 | 3.49 |
Connect7 | 8 | 5 | 6.36 | 0 | 0 | 5 | 6.36 |
Connect8 | 8 | 1 | 1.24 | 0 | 0 | 1 | 1.24 |
counter | 8 | 4 | 4.56 | 4 | 4.56 | 0 | 0 |
DFlipFlop | 8 | 8 | 9.79 | 0 | 0 | 8 | 9.79 |
Impl | 8 | 8 | 7.78 | 8 | 7.78 | 0 | 0 |
k_branch_n | 8 | 1 | 0.97 | 1 | 0.97 | 0 | 0 |
k_branch_p | 8 | 1 | 1.6 | 0 | 0 | 1 | 1.6 |
k_d4_p | 8 | 1 | 1.32 | 0 | 0 | 1 | 1.32 |
k_dum_n | 8 | 4 | 140.71 | 4 | 140.71 | 0 | 0 |
k_dum_p | 8 | 3 | 243.5 | 0 | 0 | 3 | 243.5 |
k_grz_n | 8 | 3 | 53.63 | 3 | 53.63 | 0 | 0 |
k_grz_p | 8 | 3 | 331.14 | 0 | 0 | 3 | 331.14 |
k_lin_n | 8 | 8 | 1070.65 | 8 | 1070.65 | 0 | 0 |
k_lin_p | 8 | 8 | 8.32 | 0 | 0 | 8 | 8.32 |
k_path_n | 8 | 3 | 25.22 | 3 | 25.22 | 0 | 0 |
k_path_p | 8 | 3 | 414.44 | 0 | 0 | 3 | 414.44 |
k_ph_n | 8 | 8 | 418.82 | 8 | 418.82 | 0 | 0 |
k_ph_p | 8 | 3 | 4.28 | 0 | 0 | 3 | 4.28 |
k_poly_n | 8 | 1 | 0.98 | 1 | 0.98 | 0 | 0 |
k_poly_p | 8 | 1 | 2.1 | 0 | 0 | 1 | 2.1 |
k_t4p_p | 8 | 1 | 1.56 | 0 | 0 | 1 | 1.56 |
Logn | 4 | 4 | 356.97 | 0 | 0 | 4 | 356.97 |
mA-t2-2qbf-5cnf-100var | 18 | 17 | 686.78 | 2 | 2.07 | 15 | 684.71 |
mA-t2-2qbf-5cnf-150var | 18 | 13 | 801.44 | 2 | 2.13 | 11 | 799.31 |
mA-t2-2qbf-5cnf-50var | 18 | 18 | 439.34 | 2 | 1.94 | 16 | 437.4 |
mA-t2-3qbf-5cnf-100var | 18 | 18 | 19.83 | 8 | 8.45 | 10 | 11.38 |
mA-t2-3qbf-5cnf-150var | 18 | 18 | 45.09 | 7 | 7.23 | 11 | 37.86 |
mA-t2-3qbf-5cnf-50var | 18 | 18 | 20.64 | 8 | 7.87 | 10 | 12.77 |
mA-t2-4qbf-5cnf-100var | 18 | 18 | 122.07 | 2 | 1.95 | 16 | 120.12 |
mA-t2-4qbf-5cnf-150var | 18 | 18 | 929.33 | 2 | 1.94 | 16 | 927.39 |
mA-t2-4qbf-5cnf-50var | 18 | 18 | 24.35 | 5 | 11.44 | 13 | 12.91 |
mA-t2-5qbf-5cnf-100var | 18 | 18 | 28.67 | 7 | 7.01 | 11 | 21.66 |
mA-t2-5qbf-5cnf-150var | 18 | 18 | 105.37 | 8 | 7.83 | 10 | 97.54 |
mA-t2-5qbf-5cnf-50var | 18 | 18 | 18.6 | 11 | 11.46 | 7 | 7.14 |
mB-t2-2qbf-5cnf-100var | 18 | 18 | 17.92 | 1 | 1.3 | 17 | 16.62 |
mB-t2-2qbf-5cnf-150var | 18 | 18 | 17.57 | 0 | 0 | 18 | 17.57 |
mB-t2-2qbf-5cnf-50var | 18 | 18 | 17.54 | 1 | 0.97 | 17 | 16.57 |
mB-t2-3qbf-5cnf-100var | 18 | 18 | 17.59 | 2 | 1.97 | 16 | 15.62 |
mB-t2-3qbf-5cnf-150var | 18 | 18 | 17.63 | 2 | 1.95 | 16 | 15.68 |
mB-t2-3qbf-5cnf-50var | 18 | 18 | 17.51 | 2 | 1.95 | 16 | 15.56 |
mB-t2-4qbf-5cnf-100var | 18 | 18 | 17.55 | 2 | 1.95 | 16 | 15.6 |
mB-t2-4qbf-5cnf-150var | 18 | 18 | 17.62 | 2 | 1.96 | 16 | 15.66 |
mB-t2-4qbf-5cnf-50var | 18 | 18 | 17.51 | 2 | 1.96 | 16 | 15.55 |
mB-t2-5qbf-5cnf-100var | 18 | 18 | 17.57 | 2 | 1.96 | 16 | 15.61 |
mB-t2-5qbf-5cnf-150var | 18 | 18 | 17.62 | 2 | 1.95 | 16 | 15.67 |
mB-t2-5qbf-5cnf-50var | 18 | 18 | 17.53 | 4 | 3.88 | 14 | 13.65 |
MutexP | 7 | 2 | 1.96 | 2 | 1.96 | 0 | 0 |
RobotsD2 | 8 | 8 | 29.01 | 6 | 9.02 | 2 | 19.99 |
RobotsD3 | 8 | 8 | 534.83 | 6 | 506.6 | 2 | 28.23 |
RobotsD4 | 8 | 8 | 451.13 | 6 | 439.64 | 2 | 11.49 |
RobotsD5 | 8 | 8 | 135.66 | 4 | 4.4 | 4 | 131.26 |
s27 | 4 | 1 | 1.06 | 1 | 1.06 | 0 | 0 |
s3271 | 8 | 3 | 6.31 | 0 | 0 | 3 | 6.31 |
SzymanskiP | 8 | 8 | 71.06 | 0 | 0 | 8 | 71.06 |
term1 | 8 | 7 | 312.78 | 4 | 4.13 | 3 | 308.65 |
Toilet | 8 | 6 | 831.2 | 3 | 74.82 | 3 | 756.38 |
ToiletA | 8 | 7 | 9.89 | 1 | 1.07 | 6 | 8.82 |
ToiletC | 8 | 8 | 8.82 | 3 | 3.72 | 5 | 5.1 |
ToiletG | 7 | 7 | 6.84 | 7 | 6.84 | 0 | 0 |
Tree | 8 | 8 | 15.58 | 2 | 9.77 | 6 | 5.81 |
VonNeumann | 8 | 4 | 12.11 | 0 | 0 | 4 | 12.11 |
z4ml | 8 | 8 | 7.81 | 4 | 3.91 | 4 | 3.9 |
Solved Families: 75 |
Solver: GRL |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
Adder | 8 | 1 | 0.01 | 0 | 0 | 1 | 0.01 |
Blocks | 8 | 1 | 4.73 | 0 | 0 | 1 | 4.73 |
C432 | 8 | 3 | 323.26 | 3 | 323.26 | 0 | 0 |
C499 | 8 | 2 | 0.21 | 2 | 0.21 | 0 | 0 |
C5315 | 8 | 2 | 0.25 | 2 | 0.25 | 0 | 0 |
C880 | 8 | 2 | 52.79 | 2 | 52.79 | 0 | 0 |
Chain | 8 | 4 | 750.83 | 4 | 750.83 | 0 | 0 |
comp | 8 | 6 | 641.38 | 4 | 0.02 | 2 | 641.36 |
Connect2 | 8 | 8 | 7.44 | 5 | 6.22 | 3 | 1.22 |
Connect3 | 8 | 7 | 23.31 | 0 | 0 | 7 | 23.31 |
Connect4 | 8 | 7 | 3.26 | 0 | 0 | 7 | 3.26 |
Connect5 | 8 | 7 | 6.51 | 0 | 0 | 7 | 6.51 |
Connect6 | 8 | 5 | 226.87 | 0 | 0 | 5 | 226.87 |
Connect7 | 8 | 7 | 6.25 | 0 | 0 | 7 | 6.25 |
Connect8 | 8 | 5 | 6.32 | 0 | 0 | 5 | 6.32 |
Connect9 | 3 | 2 | 2.79 | 0 | 0 | 2 | 2.79 |
counter | 8 | 4 | 5.51 | 4 | 5.51 | 0 | 0 |
DFlipFlop | 8 | 8 | 3.46 | 0 | 0 | 8 | 3.46 |
Impl | 8 | 8 | 0.08 | 8 | 0.08 | 0 | 0 |
k_branch_n | 8 | 1 | 0 | 1 | 0 | 0 | 0 |
k_branch_p | 8 | 1 | 4.13 | 0 | 0 | 1 | 4.13 |
k_d4_p | 8 | 1 | 0.56 | 0 | 0 | 1 | 0.56 |
k_dum_n | 8 | 5 | 480 | 5 | 480 | 0 | 0 |
k_dum_p | 8 | 3 | 57.87 | 0 | 0 | 3 | 57.87 |
k_grz_n | 8 | 3 | 309.84 | 3 | 309.84 | 0 | 0 |
k_grz_p | 8 | 3 | 210.35 | 0 | 0 | 3 | 210.35 |
k_lin_n | 8 | 5 | 361.67 | 5 | 361.67 | 0 | 0 |
k_lin_p | 8 | 8 | 172.88 | 0 | 0 | 8 | 172.88 |
k_path_n | 8 | 4 | 401.66 | 4 | 401.66 | 0 | 0 |
k_path_p | 8 | 3 | 401.72 | 0 | 0 | 3 | 401.72 |
k_ph_n | 8 | 6 | 4.73 | 6 | 4.73 | 0 | 0 |
k_ph_p | 8 | 3 | 33.69 | 0 | 0 | 3 | 33.69 |
k_poly_n | 8 | 2 | 426.33 | 2 | 426.33 | 0 | 0 |
k_poly_p | 8 | 1 | 1.47 | 0 | 0 | 1 | 1.47 |
k_t4p_n | 8 | 1 | 306.88 | 1 | 306.88 | 0 | 0 |
k_t4p_p | 8 | 1 | 0.72 | 0 | 0 | 1 | 0.72 |
Logn | 4 | 2 | 69.26 | 0 | 0 | 2 | 69.26 |
mA-t2-2qbf-5cnf-100var | 18 | 7 | 573.25 | 1 | 531.26 | 6 | 41.99 |
mA-t2-2qbf-5cnf-150var | 18 | 4 | 212.9 | 0 | 0 | 4 | 212.9 |
mA-t2-2qbf-5cnf-50var | 18 | 11 | 26.17 | 2 | 0.04 | 9 | 26.13 |
mA-t2-3qbf-5cnf-100var | 18 | 10 | 839.34 | 6 | 0.13 | 4 | 839.21 |
mA-t2-3qbf-5cnf-150var | 18 | 8 | 551.03 | 6 | 8.69 | 2 | 542.34 |
mA-t2-3qbf-5cnf-50var | 18 | 15 | 937.39 | 8 | 17.67 | 7 | 919.72 |
mA-t2-4qbf-5cnf-100var | 18 | 11 | 227.9 | 2 | 0 | 9 | 227.9 |
mA-t2-4qbf-5cnf-150var | 18 | 11 | 932.34 | 2 | 0.02 | 9 | 932.32 |
mA-t2-4qbf-5cnf-50var | 18 | 14 | 62.18 | 4 | 54.7 | 10 | 7.48 |
mA-t2-5qbf-5cnf-100var | 18 | 7 | 99.47 | 6 | 0.06 | 1 | 99.41 |
mA-t2-5qbf-5cnf-150var | 18 | 7 | 395.99 | 6 | 0.12 | 1 | 395.87 |
mA-t2-5qbf-5cnf-50var | 18 | 15 | 1092.28 | 9 | 600.33 | 6 | 491.95 |
mB-t2-2qbf-5cnf-100var | 18 | 17 | 18.27 | 0 | 0 | 17 | 18.27 |
mB-t2-2qbf-5cnf-150var | 18 | 18 | 1.46 | 0 | 0 | 18 | 1.46 |
mB-t2-2qbf-5cnf-50var | 18 | 18 | 0.86 | 1 | 0.04 | 17 | 0.82 |
mB-t2-3qbf-5cnf-100var | 18 | 18 | 0.45 | 2 | 0.03 | 16 | 0.42 |
mB-t2-3qbf-5cnf-150var | 18 | 18 | 0.59 | 2 | 0.02 | 16 | 0.57 |
mB-t2-3qbf-5cnf-50var | 18 | 18 | 0.11 | 2 | 0.02 | 16 | 0.09 |
mB-t2-4qbf-5cnf-100var | 18 | 18 | 0.45 | 2 | 0.02 | 16 | 0.43 |
mB-t2-4qbf-5cnf-150var | 18 | 18 | 0.74 | 2 | 0.03 | 16 | 0.71 |
mB-t2-4qbf-5cnf-50var | 18 | 18 | 0.35 | 2 | 0.02 | 16 | 0.33 |
mB-t2-5qbf-5cnf-100var | 18 | 18 | 0.53 | 2 | 0.02 | 16 | 0.51 |
mB-t2-5qbf-5cnf-150var | 18 | 18 | 0.78 | 2 | 0.04 | 16 | 0.74 |
mB-t2-5qbf-5cnf-50var | 18 | 18 | 0.31 | 4 | 0.04 | 14 | 0.27 |
MutexP | 7 | 3 | 32.33 | 3 | 32.33 | 0 | 0 |
RobotsD2 | 8 | 8 | 1447.71 | 6 | 110.83 | 2 | 1336.88 |
RobotsD3 | 8 | 4 | 846.22 | 4 | 846.22 | 0 | 0 |
RobotsD4 | 8 | 7 | 1237.79 | 5 | 109.13 | 2 | 1128.66 |
RobotsD5 | 8 | 8 | 1812.98 | 4 | 41.06 | 4 | 1771.92 |
s27 | 4 | 1 | 0.28 | 0 | 0 | 1 | 0.28 |
SzymanskiP | 8 | 8 | 134.94 | 0 | 0 | 8 | 134.94 |
term1 | 8 | 7 | 928.24 | 4 | 1.97 | 3 | 926.27 |
Toilet | 8 | 8 | 123.72 | 5 | 0.12 | 3 | 123.6 |
ToiletA | 8 | 8 | 7.57 | 1 | 5.19 | 7 | 2.38 |
ToiletC | 8 | 8 | 0.2 | 3 | 0.03 | 5 | 0.17 |
ToiletG | 7 | 7 | 0.03 | 7 | 0.03 | 0 | 0 |
Tree | 8 | 6 | 0.02 | 0 | 0 | 6 | 0.02 |
VonNeumann | 8 | 7 | 14.82 | 0 | 0 | 7 | 14.82 |
z4ml | 8 | 8 | 0.05 | 4 | 0.03 | 4 | 0.02 |
Solved Families: 76 |
Solver: orsat |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
C432 | 8 | 2 | 0.84 | 2 | 0.84 | 0 | 0 |
C499 | 8 | 1 | 0.03 | 1 | 0.03 | 0 | 0 |
comp | 8 | 1 | 22.07 | 1 | 22.07 | 0 | 0 |
Connect2 | 8 | 1 | 0.52 | 0 | 0 | 1 | 0.52 |
Connect3 | 8 | 2 | 3.89 | 0 | 0 | 2 | 3.89 |
Connect4 | 8 | 5 | 2.44 | 0 | 0 | 5 | 2.44 |
Connect5 | 8 | 3 | 1.63 | 0 | 0 | 3 | 1.63 |
Connect6 | 8 | 3 | 3.91 | 0 | 0 | 3 | 3.91 |
Connect7 | 8 | 4 | 5.82 | 0 | 0 | 4 | 5.82 |
Connect8 | 8 | 2 | 4.03 | 0 | 0 | 2 | 4.03 |
Connect9 | 3 | 1 | 1.93 | 0 | 0 | 1 | 1.93 |
counter | 8 | 2 | 1.49 | 2 | 1.49 | 0 | 0 |
DFlipFlop | 8 | 1 | 0 | 0 | 0 | 1 | 0 |
Impl | 8 | 4 | 402.49 | 4 | 402.49 | 0 | 0 |
k_lin_n | 8 | 1 | 0 | 1 | 0 | 0 | 0 |
k_ph_n | 8 | 1 | 0.01 | 1 | 0.01 | 0 | 0 |
mB-t2-3qbf-5cnf-100var | 18 | 14 | 0.27 | 0 | 0 | 14 | 0.27 |
mB-t2-3qbf-5cnf-150var | 18 | 14 | 0.35 | 0 | 0 | 14 | 0.35 |
mB-t2-3qbf-5cnf-50var | 18 | 12 | 0.14 | 0 | 0 | 12 | 0.14 |
mB-t2-5qbf-5cnf-100var | 18 | 8 | 0.18 | 0 | 0 | 8 | 0.18 |
mB-t2-5qbf-5cnf-150var | 18 | 8 | 0.26 | 0 | 0 | 8 | 0.26 |
mB-t2-5qbf-5cnf-50var | 18 | 4 | 0.04 | 0 | 0 | 4 | 0.04 |
MutexP | 7 | 7 | 5.61 | 7 | 5.61 | 0 | 0 |
RobotsD4 | 8 | 1 | 0.13 | 1 | 0.13 | 0 | 0 |
RobotsD5 | 8 | 1 | 0.12 | 1 | 0.12 | 0 | 0 |
s27 | 4 | 1 | 15.49 | 1 | 15.49 | 0 | 0 |
term1 | 8 | 2 | 673.2 | 2 | 673.2 | 0 | 0 |
Toilet | 8 | 2 | 0.01 | 1 | 0.01 | 1 | 0 |
ToiletA | 8 | 3 | 11.37 | 0 | 0 | 3 | 11.37 |
ToiletC | 8 | 5 | 17.44 | 2 | 0.89 | 3 | 16.55 |
ToiletG | 7 | 6 | 12.32 | 6 | 12.32 | 0 | 0 |
Tree | 8 | 1 | 1.09 | 0 | 0 | 1 | 1.09 |
VonNeumann | 8 | 2 | 55.78 | 0 | 0 | 2 | 55.78 |
z4ml | 8 | 8 | 0.17 | 4 | 0.04 | 4 | 0.13 |
Solved Families: 34 |
Solver: qbfl.BS |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
Adder | 8 | 1 | 0.03 | 0 | 0 | 1 | 0.03 |
C432 | 8 | 2 | 0.03 | 2 | 0.03 | 0 | 0 |
C499 | 8 | 1 | 0.04 | 1 | 0.04 | 0 | 0 |
Chain | 8 | 7 | 601.96 | 7 | 601.96 | 0 | 0 |
comp | 8 | 4 | 133.03 | 4 | 133.03 | 0 | 0 |
Connect2 | 8 | 8 | 0.84 | 0 | 0 | 8 | 0.84 |
Connect3 | 8 | 8 | 2.73 | 0 | 0 | 8 | 2.73 |
Connect4 | 8 | 8 | 1.44 | 0 | 0 | 8 | 1.44 |
Connect5 | 8 | 8 | 1.23 | 0 | 0 | 8 | 1.23 |
Connect6 | 8 | 8 | 1.42 | 0 | 0 | 8 | 1.42 |
Connect7 | 8 | 8 | 1.65 | 0 | 0 | 8 | 1.65 |
Connect8 | 8 | 7 | 3.04 | 0 | 0 | 7 | 3.04 |
Connect9 | 3 | 3 | 1.5 | 0 | 0 | 3 | 1.5 |
counter | 8 | 2 | 10.66 | 2 | 10.66 | 0 | 0 |
DFlipFlop | 8 | 8 | 10.66 | 0 | 0 | 8 | 10.66 |
Impl | 8 | 8 | 0.02 | 8 | 0.02 | 0 | 0 |
k_branch_n | 8 | 1 | 0.03 | 1 | 0.03 | 0 | 0 |
k_dum_n | 8 | 2 | 174 | 2 | 174 | 0 | 0 |
k_dum_p | 8 | 1 | 9.32 | 0 | 0 | 1 | 9.32 |
k_lin_n | 8 | 2 | 22.19 | 2 | 22.19 | 0 | 0 |
k_lin_p | 8 | 1 | 0.05 | 0 | 0 | 1 | 0.05 |
k_path_n | 8 | 2 | 258.23 | 2 | 258.23 | 0 | 0 |
k_path_p | 8 | 2 | 7.31 | 0 | 0 | 2 | 7.31 |
k_ph_n | 8 | 3 | 0.09 | 3 | 0.09 | 0 | 0 |
k_ph_p | 8 | 2 | 2.85 | 0 | 0 | 2 | 2.85 |
k_poly_n | 8 | 2 | 45.45 | 2 | 45.45 | 0 | 0 |
k_poly_p | 8 | 1 | 402.26 | 0 | 0 | 1 | 402.26 |
Logn | 4 | 2 | 0.04 | 0 | 0 | 2 | 0.04 |
mA-t2-2qbf-5cnf-100var | 18 | 8 | 67.25 | 2 | 0.03 | 6 | 67.22 |
mA-t2-2qbf-5cnf-150var | 18 | 5 | 1.34 | 2 | 0 | 3 | 1.34 |
mA-t2-2qbf-5cnf-50var | 18 | 12 | 308.94 | 2 | 0.01 | 10 | 308.93 |
mA-t2-3qbf-5cnf-100var | 18 | 8 | 0.09 | 8 | 0.09 | 0 | 0 |
mA-t2-3qbf-5cnf-150var | 18 | 8 | 0.05 | 8 | 0.05 | 0 | 0 |
mA-t2-3qbf-5cnf-50var | 18 | 8 | 0.09 | 8 | 0.09 | 0 | 0 |
mA-t2-4qbf-5cnf-100var | 18 | 4 | 0.02 | 4 | 0.02 | 0 | 0 |
mA-t2-4qbf-5cnf-150var | 18 | 4 | 0.05 | 4 | 0.05 | 0 | 0 |
mA-t2-4qbf-5cnf-50var | 18 | 5 | 0.07 | 5 | 0.07 | 0 | 0 |
mA-t2-5qbf-5cnf-100var | 18 | 9 | 0.07 | 9 | 0.07 | 0 | 0 |
mA-t2-5qbf-5cnf-150var | 18 | 10 | 0.12 | 10 | 0.12 | 0 | 0 |
mA-t2-5qbf-5cnf-50var | 18 | 10 | 0.14 | 10 | 0.14 | 0 | 0 |
mB-t2-2qbf-5cnf-100var | 18 | 17 | 1.35 | 0 | 0 | 17 | 1.35 |
mB-t2-2qbf-5cnf-150var | 18 | 18 | 4.01 | 0 | 0 | 18 | 4.01 |
mB-t2-2qbf-5cnf-50var | 18 | 18 | 0.45 | 1 | 0.14 | 17 | 0.31 |
mB-t2-3qbf-5cnf-100var | 18 | 5 | 720.7 | 2 | 0.01 | 3 | 720.69 |
mB-t2-3qbf-5cnf-150var | 18 | 2 | 3.41 | 1 | 0 | 1 | 3.41 |
mB-t2-3qbf-5cnf-50var | 18 | 18 | 452.05 | 2 | 0.03 | 16 | 452.02 |
mB-t2-4qbf-5cnf-100var | 18 | 7 | 1.72 | 2 | 0.02 | 5 | 1.7 |
mB-t2-4qbf-5cnf-150var | 18 | 6 | 0.56 | 2 | 0.01 | 4 | 0.55 |
mB-t2-4qbf-5cnf-50var | 18 | 18 | 128.17 | 2 | 0.02 | 16 | 128.15 |
mB-t2-5qbf-5cnf-100var | 18 | 4 | 0.33 | 2 | 0.01 | 2 | 0.32 |
mB-t2-5qbf-5cnf-150var | 18 | 3 | 0.09 | 2 | 0.03 | 1 | 0.06 |
mB-t2-5qbf-5cnf-50var | 18 | 11 | 1574.86 | 4 | 0.05 | 7 | 1574.81 |
MutexP | 7 | 7 | 0.21 | 7 | 0.21 | 0 | 0 |
RobotsD2 | 8 | 3 | 0.23 | 3 | 0.23 | 0 | 0 |
RobotsD4 | 8 | 1 | 0.1 | 1 | 0.1 | 0 | 0 |
RobotsD5 | 8 | 1 | 0.06 | 1 | 0.06 | 0 | 0 |
s27 | 4 | 1 | 0.12 | 1 | 0.12 | 0 | 0 |
s3271 | 8 | 8 | 1.9 | 0 | 0 | 8 | 1.9 |
SzymanskiP | 8 | 2 | 1.08 | 0 | 0 | 2 | 1.08 |
term1 | 8 | 4 | 100.64 | 4 | 100.64 | 0 | 0 |
Toilet | 8 | 8 | 552.4 | 5 | 0.15 | 3 | 552.25 |
ToiletA | 8 | 6 | 0.73 | 1 | 0.09 | 5 | 0.64 |
ToiletC | 8 | 8 | 3.13 | 3 | 0.09 | 5 | 3.04 |
ToiletG | 7 | 7 | 0.07 | 7 | 0.07 | 0 | 0 |
Tree | 8 | 7 | 719.64 | 2 | 118.53 | 5 | 601.11 |
VonNeumann | 8 | 8 | 4.04 | 0 | 0 | 8 | 4.04 |
z4ml | 8 | 8 | 0.17 | 4 | 0.08 | 4 | 0.09 |
Solved Families: 67 |
Solver: qbfl.JW |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
Adder | 8 | 1 | 0.03 | 0 | 0 | 1 | 0.03 |
C432 | 8 | 2 | 0.02 | 2 | 0.02 | 0 | 0 |
C499 | 8 | 2 | 288.7 | 2 | 288.7 | 0 | 0 |
Chain | 8 | 7 | 1295.97 | 7 | 1295.97 | 0 | 0 |
comp | 8 | 7 | 262.26 | 4 | 10.7 | 3 | 251.56 |
Connect2 | 8 | 8 | 0.88 | 0 | 0 | 8 | 0.88 |
Connect3 | 8 | 5 | 1.36 | 0 | 0 | 5 | 1.36 |
Connect4 | 8 | 8 | 1.43 | 0 | 0 | 8 | 1.43 |
Connect5 | 8 | 8 | 1.24 | 0 | 0 | 8 | 1.24 |
Connect6 | 8 | 8 | 1.39 | 0 | 0 | 8 | 1.39 |
Connect7 | 8 | 8 | 1.61 | 0 | 0 | 8 | 1.61 |
Connect8 | 8 | 8 | 3.13 | 0 | 0 | 8 | 3.13 |
Connect9 | 3 | 3 | 1.47 | 0 | 0 | 3 | 1.47 |
counter | 8 | 2 | 10.65 | 2 | 10.65 | 0 | 0 |
DFlipFlop | 8 | 8 | 11.65 | 0 | 0 | 8 | 11.65 |
Impl | 8 | 8 | 0.06 | 8 | 0.06 | 0 | 0 |
k_branch_n | 8 | 1 | 0.1 | 1 | 0.1 | 0 | 0 |
k_dum_n | 8 | 1 | 23.99 | 1 | 23.99 | 0 | 0 |
k_dum_p | 8 | 1 | 18.89 | 0 | 0 | 1 | 18.89 |
k_lin_n | 8 | 2 | 56.24 | 2 | 56.24 | 0 | 0 |
k_lin_p | 8 | 1 | 0.05 | 0 | 0 | 1 | 0.05 |
k_path_n | 8 | 1 | 0.05 | 1 | 0.05 | 0 | 0 |
k_path_p | 8 | 2 | 7.2 | 0 | 0 | 2 | 7.2 |
k_ph_n | 8 | 4 | 21.68 | 4 | 21.68 | 0 | 0 |
k_ph_p | 8 | 2 | 1.68 | 0 | 0 | 2 | 1.68 |
k_poly_n | 8 | 2 | 401.93 | 2 | 401.93 | 0 | 0 |
Logn | 4 | 2 | 0.02 | 0 | 0 | 2 | 0.02 |
mA-t2-2qbf-5cnf-100var | 18 | 8 | 9.61 | 2 | 0.01 | 6 | 9.6 |
mA-t2-2qbf-5cnf-150var | 18 | 6 | 228.25 | 2 | 0.04 | 4 | 228.21 |
mA-t2-2qbf-5cnf-50var | 18 | 11 | 608.44 | 2 | 0.02 | 9 | 608.42 |
mA-t2-3qbf-5cnf-100var | 18 | 8 | 0.04 | 8 | 0.04 | 0 | 0 |
mA-t2-3qbf-5cnf-150var | 18 | 8 | 0.08 | 8 | 0.08 | 0 | 0 |
mA-t2-3qbf-5cnf-50var | 18 | 9 | 222.19 | 8 | 0.11 | 1 | 222.08 |
mA-t2-4qbf-5cnf-100var | 18 | 4 | 0.01 | 4 | 0.01 | 0 | 0 |
mA-t2-4qbf-5cnf-150var | 18 | 4 | 0.06 | 4 | 0.06 | 0 | 0 |
mA-t2-4qbf-5cnf-50var | 18 | 7 | 857.92 | 5 | 0.03 | 2 | 857.89 |
mA-t2-5qbf-5cnf-100var | 18 | 9 | 0.08 | 9 | 0.08 | 0 | 0 |
mA-t2-5qbf-5cnf-150var | 18 | 10 | 0.08 | 10 | 0.08 | 0 | 0 |
mA-t2-5qbf-5cnf-50var | 18 | 10 | 0.08 | 10 | 0.08 | 0 | 0 |
mB-t2-2qbf-5cnf-100var | 18 | 18 | 176.75 | 1 | 57.48 | 17 | 119.27 |
mB-t2-2qbf-5cnf-150var | 18 | 18 | 0.36 | 0 | 0 | 18 | 0.36 |
mB-t2-2qbf-5cnf-50var | 18 | 18 | 0.56 | 1 | 0.05 | 17 | 0.51 |
mB-t2-3qbf-5cnf-100var | 18 | 17 | 319.29 | 2 | 0.02 | 15 | 319.27 |
mB-t2-3qbf-5cnf-150var | 18 | 14 | 275.69 | 2 | 0.02 | 12 | 275.67 |
mB-t2-3qbf-5cnf-50var | 18 | 18 | 2.91 | 2 | 0.02 | 16 | 2.89 |
mB-t2-4qbf-5cnf-100var | 18 | 13 | 1111.27 | 2 | 0.01 | 11 | 1111.26 |
mB-t2-4qbf-5cnf-150var | 18 | 6 | 0.08 | 2 | 0 | 4 | 0.08 |
mB-t2-4qbf-5cnf-50var | 18 | 18 | 5.6 | 2 | 0.02 | 16 | 5.58 |
mB-t2-5qbf-5cnf-100var | 18 | 10 | 912.84 | 2 | 0.02 | 8 | 912.82 |
mB-t2-5qbf-5cnf-150var | 18 | 6 | 1206.18 | 2 | 0.02 | 4 | 1206.16 |
mB-t2-5qbf-5cnf-50var | 18 | 13 | 441.89 | 4 | 0.05 | 9 | 441.84 |
MutexP | 7 | 7 | 0.25 | 7 | 0.25 | 0 | 0 |
RobotsD2 | 8 | 4 | 273.28 | 4 | 273.28 | 0 | 0 |
RobotsD3 | 8 | 3 | 314.01 | 3 | 314.01 | 0 | 0 |
RobotsD4 | 8 | 4 | 115.3 | 4 | 115.3 | 0 | 0 |
RobotsD5 | 8 | 3 | 3.51 | 3 | 3.51 | 0 | 0 |
s27 | 4 | 1 | 0.01 | 1 | 0.01 | 0 | 0 |
s3271 | 8 | 7 | 1.65 | 0 | 0 | 7 | 1.65 |
SzymanskiP | 8 | 8 | 386.86 | 0 | 0 | 8 | 386.86 |
term1 | 8 | 4 | 1.06 | 4 | 1.06 | 0 | 0 |
Toilet | 8 | 8 | 507.95 | 5 | 0.13 | 3 | 507.82 |
ToiletA | 8 | 7 | 798.11 | 1 | 0.09 | 6 | 798.02 |
ToiletC | 8 | 8 | 219.34 | 3 | 0.04 | 5 | 219.3 |
ToiletG | 7 | 7 | 0.06 | 7 | 0.06 | 0 | 0 |
Tree | 8 | 6 | 534.37 | 1 | 31.77 | 5 | 502.6 |
VonNeumann | 8 | 8 | 3.99 | 0 | 0 | 8 | 3.99 |
z4ml | 8 | 8 | 0.12 | 4 | 0.05 | 4 | 0.07 |
Solved Families: 67 |
Solver: QMRes |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
Adder | 8 | 6 | 132.57 | 2 | 33.86 | 4 | 98.71 |
Blocks | 8 | 1 | 38.4 | 0 | 0 | 1 | 38.4 |
C499 | 8 | 1 | 760.83 | 1 | 760.83 | 0 | 0 |
Chain | 8 | 8 | 6.57 | 8 | 6.57 | 0 | 0 |
comp | 8 | 8 | 1.13 | 4 | 0.57 | 4 | 0.56 |
Connect2 | 8 | 2 | 4.22 | 0 | 0 | 2 | 4.22 |
Connect4 | 8 | 3 | 572.21 | 0 | 0 | 3 | 572.21 |
Connect5 | 8 | 1 | 773.33 | 0 | 0 | 1 | 773.33 |
Connect6 | 8 | 1 | 597.09 | 0 | 0 | 1 | 597.09 |
counter | 8 | 4 | 130.88 | 4 | 130.88 | 0 | 0 |
DFlipFlop | 8 | 2 | 474.12 | 0 | 0 | 2 | 474.12 |
Impl | 8 | 8 | 0.16 | 8 | 0.16 | 0 | 0 |
jmc_quant | 8 | 3 | 18.68 | 2 | 8.65 | 1 | 10.03 |
jmc_quant_squaring | 8 | 3 | 11.45 | 2 | 4.26 | 1 | 7.19 |
k_branch_n | 8 | 1 | 0.05 | 1 | 0.05 | 0 | 0 |
k_branch_p | 8 | 1 | 3.15 | 0 | 0 | 1 | 3.15 |
k_d4_n | 8 | 8 | 32.64 | 8 | 32.64 | 0 | 0 |
k_d4_p | 8 | 8 | 12.44 | 0 | 0 | 8 | 12.44 |
k_dum_n | 8 | 8 | 3.94 | 8 | 3.94 | 0 | 0 |
k_dum_p | 8 | 8 | 4.76 | 0 | 0 | 8 | 4.76 |
k_grz_n | 8 | 8 | 877.33 | 8 | 877.33 | 0 | 0 |
k_grz_p | 8 | 8 | 9.19 | 0 | 0 | 8 | 9.19 |
k_lin_n | 8 | 4 | 576.81 | 4 | 576.81 | 0 | 0 |
k_lin_p | 8 | 6 | 3.43 | 0 | 0 | 6 | 3.43 |
k_path_n | 8 | 8 | 3.55 | 8 | 3.55 | 0 | 0 |
k_path_p | 8 | 8 | 11.52 | 0 | 0 | 8 | 11.52 |
k_ph_n | 8 | 4 | 16.52 | 4 | 16.52 | 0 | 0 |
k_ph_p | 8 | 2 | 0.16 | 0 | 0 | 2 | 0.16 |
k_poly_n | 8 | 7 | 46.18 | 7 | 46.18 | 0 | 0 |
k_poly_p | 8 | 3 | 255.38 | 0 | 0 | 3 | 255.38 |
k_t4p_n | 8 | 8 | 94.1 | 8 | 94.1 | 0 | 0 |
k_t4p_p | 8 | 8 | 22.92 | 0 | 0 | 8 | 22.92 |
Logn | 4 | 2 | 0.08 | 2 | 0.08 | 0 | 0 |
mA-t2-2qbf-5cnf-100var | 18 | 2 | 1.47 | 2 | 1.47 | 0 | 0 |
mA-t2-2qbf-5cnf-150var | 18 | 2 | 426.04 | 2 | 426.04 | 0 | 0 |
mA-t2-2qbf-5cnf-50var | 18 | 2 | 0.08 | 2 | 0.08 | 0 | 0 |
mA-t2-3qbf-5cnf-100var | 18 | 2 | 0.25 | 2 | 0.25 | 0 | 0 |
mA-t2-3qbf-5cnf-150var | 18 | 2 | 10.31 | 2 | 10.31 | 0 | 0 |
mA-t2-3qbf-5cnf-50var | 18 | 4 | 916.71 | 4 | 916.71 | 0 | 0 |
mA-t2-4qbf-5cnf-100var | 18 | 2 | 0.18 | 2 | 0.18 | 0 | 0 |
mA-t2-4qbf-5cnf-150var | 18 | 2 | 0.65 | 2 | 0.65 | 0 | 0 |
mA-t2-4qbf-5cnf-50var | 18 | 3 | 140.78 | 3 | 140.78 | 0 | 0 |
mA-t2-5qbf-5cnf-100var | 18 | 4 | 92.4 | 4 | 92.4 | 0 | 0 |
mA-t2-5qbf-5cnf-150var | 18 | 2 | 0.47 | 2 | 0.47 | 0 | 0 |
mA-t2-5qbf-5cnf-50var | 18 | 4 | 1.85 | 4 | 1.85 | 0 | 0 |
mB-t2-2qbf-5cnf-100var | 18 | 2 | 0.24 | 1 | 0.11 | 1 | 0.13 |
mB-t2-2qbf-5cnf-150var | 18 | 2 | 54.94 | 0 | 0 | 2 | 54.94 |
mB-t2-2qbf-5cnf-50var | 18 | 4 | 120.92 | 1 | 0.02 | 3 | 120.9 |
mB-t2-3qbf-5cnf-100var | 18 | 15 | 26.82 | 2 | 0.19 | 13 | 26.63 |
mB-t2-3qbf-5cnf-150var | 18 | 14 | 33.97 | 2 | 0.41 | 12 | 33.56 |
mB-t2-3qbf-5cnf-50var | 18 | 17 | 769.57 | 2 | 0.06 | 15 | 769.51 |
mB-t2-4qbf-5cnf-100var | 18 | 2 | 0.24 | 2 | 0.24 | 0 | 0 |
mB-t2-4qbf-5cnf-150var | 18 | 2 | 0.49 | 2 | 0.49 | 0 | 0 |
mB-t2-4qbf-5cnf-50var | 18 | 4 | 1.31 | 2 | 0.06 | 2 | 1.25 |
mB-t2-5qbf-5cnf-100var | 18 | 17 | 1017.01 | 2 | 0.24 | 15 | 1016.77 |
mB-t2-5qbf-5cnf-150var | 18 | 14 | 285.17 | 2 | 0.71 | 12 | 284.46 |
mB-t2-5qbf-5cnf-50var | 18 | 18 | 189.42 | 4 | 0.35 | 14 | 189.07 |
MutexP | 7 | 4 | 127.59 | 4 | 127.59 | 0 | 0 |
RobotsD2 | 8 | 3 | 3.54 | 3 | 3.54 | 0 | 0 |
RobotsD4 | 8 | 1 | 0.95 | 1 | 0.95 | 0 | 0 |
RobotsD5 | 8 | 1 | 0.95 | 1 | 0.95 | 0 | 0 |
s27 | 4 | 4 | 27.62 | 1 | 0.03 | 3 | 27.59 |
s499 | 8 | 1 | 19.92 | 1 | 19.92 | 0 | 0 |
SzymanskiP | 8 | 1 | 0.09 | 0 | 0 | 1 | 0.09 |
term1 | 8 | 6 | 133.77 | 3 | 80.08 | 3 | 53.69 |
Toilet | 8 | 7 | 301.46 | 4 | 297.77 | 3 | 3.69 |
ToiletA | 8 | 6 | 37.22 | 1 | 2.24 | 5 | 34.98 |
ToiletC | 8 | 6 | 188.12 | 1 | 185.17 | 5 | 2.95 |
ToiletG | 7 | 7 | 0.09 | 7 | 0.09 | 0 | 0 |
Tree | 8 | 8 | 0.12 | 2 | 0.03 | 6 | 0.09 |
z4ml | 8 | 8 | 0.16 | 4 | 0.08 | 4 | 0.08 |
Solved Families: 71 |
Solver: quantor-2.1 |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
Adder | 8 | 2 | 27.51 | 1 | 27.12 | 1 | 0.39 |
Blocks | 8 | 8 | 121.69 | 2 | 0.79 | 6 | 120.9 |
C432 | 8 | 6 | 1246.39 | 2 | 0.05 | 4 | 1246.34 |
C499 | 8 | 4 | 18.01 | 2 | 0.08 | 2 | 17.93 |
C5315 | 8 | 4 | 152.4 | 2 | 17.93 | 2 | 134.47 |
Chain | 8 | 8 | 0.22 | 8 | 0.22 | 0 | 0 |
comp | 8 | 8 | 0.41 | 4 | 0.19 | 4 | 0.22 |
Connect2 | 8 | 4 | 0.57 | 1 | 0.1 | 3 | 0.47 |
Connect3 | 8 | 6 | 3.14 | 0 | 0 | 6 | 3.14 |
Connect4 | 8 | 7 | 1.31 | 0 | 0 | 7 | 1.31 |
Connect5 | 8 | 6 | 1.29 | 0 | 0 | 6 | 1.29 |
Connect6 | 8 | 4 | 1.23 | 0 | 0 | 4 | 1.23 |
Connect7 | 8 | 7 | 2.78 | 0 | 0 | 7 | 2.78 |
Connect8 | 8 | 5 | 2.46 | 0 | 0 | 5 | 2.46 |
Connect9 | 3 | 2 | 1.01 | 0 | 0 | 2 | 1.01 |
counter | 8 | 4 | 0.05 | 4 | 0.05 | 0 | 0 |
DFlipFlop | 8 | 8 | 1.76 | 0 | 0 | 8 | 1.76 |
Impl | 8 | 8 | 0.05 | 8 | 0.05 | 0 | 0 |
k_branch_n | 8 | 1 | 0.02 | 1 | 0.02 | 0 | 0 |
k_branch_p | 8 | 1 | 0.57 | 0 | 0 | 1 | 0.57 |
k_d4_p | 8 | 3 | 5.06 | 0 | 0 | 3 | 5.06 |
k_dum_n | 8 | 8 | 0.28 | 8 | 0.28 | 0 | 0 |
k_dum_p | 8 | 6 | 32.26 | 0 | 0 | 6 | 32.26 |
k_grz_n | 8 | 7 | 102.29 | 7 | 102.29 | 0 | 0 |
k_grz_p | 8 | 7 | 117.75 | 0 | 0 | 7 | 117.75 |
k_lin_n | 8 | 5 | 296.05 | 5 | 296.05 | 0 | 0 |
k_lin_p | 8 | 8 | 1.9 | 0 | 0 | 8 | 1.9 |
k_path_n | 8 | 8 | 0.12 | 8 | 0.12 | 0 | 0 |
k_path_p | 8 | 8 | 0.2 | 0 | 0 | 8 | 0.2 |
k_ph_n | 8 | 6 | 0.93 | 6 | 0.93 | 0 | 0 |
k_ph_p | 8 | 3 | 1.31 | 0 | 0 | 3 | 1.31 |
k_poly_n | 8 | 8 | 0.18 | 8 | 0.18 | 0 | 0 |
k_poly_p | 8 | 8 | 0.11 | 0 | 0 | 8 | 0.11 |
k_t4p_n | 8 | 2 | 1.16 | 2 | 1.16 | 0 | 0 |
k_t4p_p | 8 | 4 | 75.35 | 0 | 0 | 4 | 75.35 |
Logn | 4 | 4 | 26.34 | 0 | 0 | 4 | 26.34 |
mA-t2-2qbf-5cnf-100var | 18 | 2 | 0.28 | 2 | 0.28 | 0 | 0 |
mA-t2-2qbf-5cnf-150var | 18 | 2 | 0.17 | 2 | 0.17 | 0 | 0 |
mA-t2-2qbf-5cnf-50var | 18 | 2 | 0.02 | 2 | 0.02 | 0 | 0 |
mA-t2-3qbf-5cnf-100var | 18 | 2 | 0 | 2 | 0 | 0 | 0 |
mA-t2-3qbf-5cnf-150var | 18 | 2 | 0 | 2 | 0 | 0 | 0 |
mA-t2-3qbf-5cnf-50var | 18 | 2 | 0 | 2 | 0 | 0 | 0 |
mA-t2-4qbf-5cnf-100var | 18 | 2 | 0.03 | 2 | 0.03 | 0 | 0 |
mA-t2-4qbf-5cnf-150var | 18 | 2 | 0.01 | 2 | 0.01 | 0 | 0 |
mA-t2-4qbf-5cnf-50var | 18 | 2 | 0.02 | 2 | 0.02 | 0 | 0 |
mA-t2-5qbf-5cnf-100var | 18 | 4 | 0.04 | 4 | 0.04 | 0 | 0 |
mA-t2-5qbf-5cnf-150var | 18 | 4 | 0.03 | 4 | 0.03 | 0 | 0 |
mA-t2-5qbf-5cnf-50var | 18 | 4 | 0.01 | 4 | 0.01 | 0 | 0 |
mB-t2-2qbf-5cnf-100var | 18 | 2 | 0.07 | 1 | 0.03 | 1 | 0.04 |
mB-t2-2qbf-5cnf-150var | 18 | 2 | 1.7 | 0 | 0 | 2 | 1.7 |
mB-t2-2qbf-5cnf-50var | 18 | 4 | 2.75 | 1 | 0 | 3 | 2.75 |
mB-t2-3qbf-5cnf-100var | 18 | 16 | 62.3 | 2 | 0.02 | 14 | 62.28 |
mB-t2-3qbf-5cnf-150var | 18 | 10 | 76.39 | 2 | 0.02 | 8 | 76.37 |
mB-t2-3qbf-5cnf-50var | 18 | 18 | 0.5 | 2 | 0.01 | 16 | 0.49 |
mB-t2-4qbf-5cnf-100var | 18 | 3 | 38.11 | 2 | 0.01 | 1 | 38.1 |
mB-t2-4qbf-5cnf-150var | 18 | 2 | 0.02 | 2 | 0.02 | 0 | 0 |
mB-t2-4qbf-5cnf-50var | 18 | 4 | 0.09 | 2 | 0.01 | 2 | 0.08 |
mB-t2-5qbf-5cnf-100var | 18 | 9 | 71.27 | 2 | 0.01 | 7 | 71.26 |
mB-t2-5qbf-5cnf-150var | 18 | 7 | 2.11 | 2 | 0.02 | 5 | 2.09 |
mB-t2-5qbf-5cnf-50var | 18 | 13 | 7.83 | 4 | 0.02 | 9 | 7.81 |
MutexP | 7 | 3 | 0.19 | 3 | 0.19 | 0 | 0 |
RobotsD2 | 8 | 3 | 0.45 | 3 | 0.45 | 0 | 0 |
RobotsD3 | 8 | 1 | 1.87 | 1 | 1.87 | 0 | 0 |
RobotsD4 | 8 | 3 | 4.6 | 3 | 4.6 | 0 | 0 |
RobotsD5 | 8 | 3 | 41.56 | 3 | 41.56 | 0 | 0 |
s27 | 4 | 4 | 3.04 | 1 | 0.01 | 3 | 3.03 |
s298 | 8 | 1 | 452.96 | 1 | 452.96 | 0 | 0 |
s3330 | 8 | 1 | 154.87 | 1 | 154.87 | 0 | 0 |
s499 | 8 | 3 | 70.41 | 3 | 70.41 | 0 | 0 |
s641 | 8 | 1 | 350.81 | 1 | 350.81 | 0 | 0 |
s713 | 8 | 1 | 287.14 | 1 | 287.14 | 0 | 0 |
SzymanskiP | 8 | 2 | 7.75 | 0 | 0 | 2 | 7.75 |
term1 | 8 | 6 | 64.49 | 4 | 62.81 | 2 | 1.68 |
Toilet | 8 | 8 | 261.16 | 5 | 260.61 | 3 | 0.55 |
ToiletA | 8 | 7 | 33.2 | 1 | 0.09 | 6 | 33.11 |
ToiletC | 8 | 8 | 1.7 | 3 | 1.16 | 5 | 0.54 |
ToiletG | 7 | 7 | 0.05 | 7 | 0.05 | 0 | 0 |
Tree | 8 | 8 | 0.01 | 2 | 0.01 | 6 | 0 |
VonNeumann | 8 | 8 | 16.58 | 0 | 0 | 8 | 16.58 |
z4ml | 8 | 8 | 0.1 | 4 | 0.04 | 4 | 0.06 |
Solved Families: 80 |
Solver: openqbf |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
Adder | 8 | 1 | 0.29 | 0 | 0 | 1 | 0.29 |
Blocks | 8 | 1 | 23.3 | 0 | 0 | 1 | 23.3 |
C432 | 8 | 3 | 671.47 | 2 | 10.11 | 1 | 661.36 |
C499 | 8 | 2 | 2.31 | 2 | 2.31 | 0 | 0 |
Chain | 8 | 6 | 723.11 | 6 | 723.11 | 0 | 0 |
comp | 8 | 4 | 66.09 | 4 | 66.09 | 0 | 0 |
Connect2 | 8 | 8 | 23.45 | 5 | 21.26 | 3 | 2.19 |
Connect3 | 8 | 7 | 102.55 | 0 | 0 | 7 | 102.55 |
Connect4 | 8 | 7 | 6.27 | 0 | 0 | 7 | 6.27 |
Connect5 | 8 | 7 | 139.85 | 0 | 0 | 7 | 139.85 |
Connect6 | 8 | 4 | 4.71 | 0 | 0 | 4 | 4.71 |
Connect7 | 8 | 7 | 9.77 | 0 | 0 | 7 | 9.77 |
Connect8 | 8 | 5 | 7.81 | 0 | 0 | 5 | 7.81 |
Connect9 | 3 | 2 | 3.24 | 0 | 0 | 2 | 3.24 |
counter | 8 | 2 | 3.09 | 2 | 3.09 | 0 | 0 |
DFlipFlop | 8 | 8 | 9.17 | 0 | 0 | 8 | 9.17 |
Impl | 8 | 8 | 48.44 | 8 | 48.44 | 0 | 0 |
k_branch_n | 8 | 1 | 0.68 | 1 | 0.68 | 0 | 0 |
k_d4_p | 8 | 1 | 290.98 | 0 | 0 | 1 | 290.98 |
k_dum_n | 8 | 1 | 24.53 | 1 | 24.53 | 0 | 0 |
k_dum_p | 8 | 1 | 1.84 | 0 | 0 | 1 | 1.84 |
k_lin_n | 8 | 2 | 220 | 2 | 220 | 0 | 0 |
k_lin_p | 8 | 1 | 0.88 | 0 | 0 | 1 | 0.88 |
k_path_n | 8 | 2 | 20.53 | 2 | 20.53 | 0 | 0 |
k_path_p | 8 | 2 | 2.08 | 0 | 0 | 2 | 2.08 |
k_ph_n | 8 | 3 | 120.74 | 3 | 120.74 | 0 | 0 |
k_ph_p | 8 | 2 | 2.85 | 0 | 0 | 2 | 2.85 |
k_poly_n | 8 | 1 | 0.54 | 1 | 0.54 | 0 | 0 |
k_poly_p | 8 | 8 | 2.64 | 0 | 0 | 8 | 2.64 |
k_t4p_p | 8 | 1 | 38.17 | 0 | 0 | 1 | 38.17 |
Logn | 4 | 2 | 0.5 | 0 | 0 | 2 | 0.5 |
mA-t2-2qbf-5cnf-100var | 18 | 4 | 174.18 | 0 | 0 | 4 | 174.18 |
mA-t2-2qbf-5cnf-150var | 18 | 4 | 4.16 | 0 | 0 | 4 | 4.16 |
mA-t2-2qbf-5cnf-50var | 18 | 11 | 412.15 | 2 | 1.93 | 9 | 410.22 |
mA-t2-3qbf-5cnf-100var | 18 | 4 | 1.3 | 4 | 1.3 | 0 | 0 |
mA-t2-3qbf-5cnf-150var | 18 | 4 | 1.02 | 4 | 1.02 | 0 | 0 |
mA-t2-3qbf-5cnf-50var | 18 | 10 | 694.01 | 6 | 6.87 | 4 | 687.14 |
mA-t2-4qbf-5cnf-100var | 18 | 2 | 0.41 | 2 | 0.41 | 0 | 0 |
mA-t2-4qbf-5cnf-150var | 18 | 2 | 0.46 | 2 | 0.46 | 0 | 0 |
mA-t2-4qbf-5cnf-50var | 18 | 10 | 1800.87 | 4 | 166.98 | 6 | 1633.89 |
mA-t2-5qbf-5cnf-100var | 18 | 6 | 1.41 | 6 | 1.41 | 0 | 0 |
mA-t2-5qbf-5cnf-150var | 18 | 6 | 1.62 | 6 | 1.62 | 0 | 0 |
mA-t2-5qbf-5cnf-50var | 18 | 6 | 1.21 | 6 | 1.21 | 0 | 0 |
mB-t2-2qbf-5cnf-100var | 18 | 18 | 159.36 | 1 | 146.88 | 17 | 12.48 |
mB-t2-2qbf-5cnf-150var | 18 | 18 | 9.73 | 0 | 0 | 18 | 9.73 |
mB-t2-2qbf-5cnf-50var | 18 | 18 | 7.01 | 1 | 0.46 | 17 | 6.55 |
mB-t2-3qbf-5cnf-100var | 18 | 18 | 19.15 | 2 | 0.36 | 16 | 18.79 |
mB-t2-3qbf-5cnf-150var | 18 | 17 | 858.23 | 2 | 0.4 | 15 | 857.83 |
mB-t2-3qbf-5cnf-50var | 18 | 18 | 4.01 | 2 | 0.35 | 16 | 3.66 |
mB-t2-4qbf-5cnf-100var | 18 | 18 | 8.79 | 2 | 0.43 | 16 | 8.36 |
mB-t2-4qbf-5cnf-150var | 18 | 18 | 366.32 | 2 | 0.41 | 16 | 365.91 |
mB-t2-4qbf-5cnf-50var | 18 | 18 | 5.42 | 2 | 0.38 | 16 | 5.04 |
mB-t2-5qbf-5cnf-100var | 18 | 16 | 900.74 | 2 | 0.45 | 14 | 900.29 |
mB-t2-5qbf-5cnf-150var | 18 | 13 | 11.93 | 2 | 0.42 | 11 | 11.51 |
mB-t2-5qbf-5cnf-50var | 18 | 18 | 82.5 | 4 | 0.76 | 14 | 81.74 |
MutexP | 7 | 3 | 83.76 | 3 | 83.76 | 0 | 0 |
RobotsD2 | 8 | 4 | 408.3 | 4 | 408.3 | 0 | 0 |
RobotsD3 | 8 | 3 | 701.99 | 3 | 701.99 | 0 | 0 |
RobotsD4 | 8 | 4 | 306 | 4 | 306 | 0 | 0 |
RobotsD5 | 8 | 3 | 14.03 | 3 | 14.03 | 0 | 0 |
s27 | 4 | 1 | 0.3 | 1 | 0.3 | 0 | 0 |
SzymanskiP | 8 | 8 | 596.66 | 0 | 0 | 8 | 596.66 |
term1 | 8 | 2 | 3.77 | 2 | 3.77 | 0 | 0 |
Toilet | 8 | 4 | 147.29 | 2 | 58.25 | 2 | 89.04 |
ToiletA | 8 | 7 | 1145.93 | 1 | 1.98 | 6 | 1143.95 |
ToiletC | 8 | 8 | 381.73 | 3 | 375.33 | 5 | 6.4 |
ToiletG | 7 | 7 | 1.5 | 7 | 1.5 | 0 | 0 |
Tree | 8 | 6 | 212.79 | 2 | 2.09 | 4 | 210.7 |
VonNeumann | 8 | 7 | 21.09 | 0 | 0 | 7 | 21.09 |
z4ml | 8 | 8 | 1.92 | 4 | 0.83 | 4 | 1.09 |
Solved Families: 70 |
Solver: qsat |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
Adder | 8 | 1 | 0 | 0 | 0 | 1 | 0 |
Blocks | 8 | 8 | 3.49 | 2 | 0.11 | 6 | 3.38 |
C432 | 8 | 4 | 174.5 | 2 | 0.95 | 2 | 173.55 |
C499 | 8 | 1 | 0.51 | 1 | 0.51 | 0 | 0 |
Chain | 8 | 8 | 245.49 | 8 | 245.49 | 0 | 0 |
comp | 8 | 6 | 9.61 | 3 | 1.06 | 3 | 8.55 |
Connect2 | 8 | 8 | 177.99 | 5 | 177.3 | 3 | 0.69 |
Connect3 | 8 | 3 | 836.6 | 0 | 0 | 3 | 836.6 |
Connect4 | 8 | 5 | 0.6 | 0 | 0 | 5 | 0.6 |
Connect5 | 8 | 5 | 0.66 | 0 | 0 | 5 | 0.66 |
Connect6 | 8 | 3 | 0.75 | 0 | 0 | 3 | 0.75 |
Connect7 | 8 | 5 | 2.09 | 0 | 0 | 5 | 2.09 |
Connect8 | 8 | 1 | 0.37 | 0 | 0 | 1 | 0.37 |
counter | 8 | 3 | 35.64 | 3 | 35.64 | 0 | 0 |
DFlipFlop | 8 | 8 | 308.23 | 0 | 0 | 8 | 308.23 |
Impl | 8 | 6 | 188.48 | 6 | 188.48 | 0 | 0 |
k_branch_n | 8 | 1 | 0.02 | 1 | 0.02 | 0 | 0 |
k_branch_p | 8 | 8 | 111.29 | 0 | 0 | 8 | 111.29 |
k_d4_p | 8 | 8 | 0.08 | 0 | 0 | 8 | 0.08 |
k_dum_n | 8 | 5 | 230.01 | 5 | 230.01 | 0 | 0 |
k_dum_p | 8 | 2 | 119.83 | 0 | 0 | 2 | 119.83 |
k_grz_n | 8 | 2 | 72.53 | 2 | 72.53 | 0 | 0 |
k_lin_n | 8 | 5 | 537.88 | 5 | 537.88 | 0 | 0 |
k_lin_p | 8 | 8 | 0.85 | 0 | 0 | 8 | 0.85 |
k_path_n | 8 | 4 | 313.06 | 4 | 313.06 | 0 | 0 |
k_path_p | 8 | 8 | 0.41 | 0 | 0 | 8 | 0.41 |
k_ph_n | 8 | 7 | 34.58 | 6 | 12.36 | 1 | 22.22 |
k_ph_p | 8 | 5 | 371.61 | 0 | 0 | 5 | 371.61 |
k_poly_n | 8 | 2 | 884.75 | 2 | 884.75 | 0 | 0 |
k_poly_p | 8 | 7 | 0.11 | 0 | 0 | 7 | 0.11 |
k_t4p_n | 8 | 1 | 132.35 | 1 | 132.35 | 0 | 0 |
k_t4p_p | 8 | 1 | 2.01 | 0 | 0 | 1 | 2.01 |
Logn | 4 | 4 | 0.34 | 0 | 0 | 4 | 0.34 |
mA-t2-2qbf-5cnf-100var | 18 | 9 | 0.23 | 0 | 0 | 9 | 0.23 |
mA-t2-2qbf-5cnf-150var | 18 | 11 | 311.11 | 0 | 0 | 11 | 311.11 |
mA-t2-2qbf-5cnf-50var | 18 | 11 | 81.78 | 0 | 0 | 11 | 81.78 |
mA-t2-3qbf-5cnf-100var | 18 | 12 | 382.11 | 4 | 0.06 | 8 | 382.05 |
mA-t2-3qbf-5cnf-150var | 18 | 11 | 324.1 | 5 | 249.13 | 6 | 74.97 |
mA-t2-3qbf-5cnf-50var | 18 | 15 | 190.31 | 7 | 180.05 | 8 | 10.26 |
mA-t2-4qbf-5cnf-100var | 18 | 8 | 14.48 | 2 | 0.02 | 6 | 14.46 |
mA-t2-4qbf-5cnf-150var | 18 | 10 | 95.24 | 2 | 0.02 | 8 | 95.22 |
mA-t2-4qbf-5cnf-50var | 18 | 10 | 1.92 | 2 | 0.01 | 8 | 1.91 |
mA-t2-5qbf-5cnf-100var | 18 | 6 | 0.29 | 6 | 0.29 | 0 | 0 |
mA-t2-5qbf-5cnf-150var | 18 | 6 | 20.05 | 6 | 20.05 | 0 | 0 |
mA-t2-5qbf-5cnf-50var | 18 | 7 | 46.53 | 6 | 0.25 | 1 | 46.28 |
mB-t2-2qbf-5cnf-100var | 18 | 14 | 457.89 | 0 | 0 | 14 | 457.89 |
mB-t2-2qbf-5cnf-150var | 18 | 16 | 504.58 | 0 | 0 | 16 | 504.58 |
mB-t2-2qbf-5cnf-50var | 18 | 17 | 31.01 | 0 | 0 | 17 | 31.01 |
mB-t2-3qbf-5cnf-100var | 18 | 18 | 5.66 | 2 | 0.02 | 16 | 5.64 |
mB-t2-3qbf-5cnf-150var | 18 | 18 | 17.85 | 2 | 0.01 | 16 | 17.84 |
mB-t2-3qbf-5cnf-50var | 18 | 18 | 0.91 | 2 | 0.01 | 16 | 0.9 |
mB-t2-4qbf-5cnf-100var | 18 | 18 | 2.42 | 2 | 0.02 | 16 | 2.4 |
mB-t2-4qbf-5cnf-150var | 18 | 16 | 6.58 | 2 | 0 | 14 | 6.58 |
mB-t2-4qbf-5cnf-50var | 18 | 18 | 0.42 | 2 | 0.02 | 16 | 0.4 |
mB-t2-5qbf-5cnf-100var | 18 | 18 | 366.35 | 2 | 0 | 16 | 366.35 |
mB-t2-5qbf-5cnf-150var | 18 | 16 | 576.21 | 2 | 0.02 | 14 | 576.19 |
mB-t2-5qbf-5cnf-50var | 18 | 18 | 53.15 | 4 | 0.03 | 14 | 53.12 |
MutexP | 7 | 2 | 2.4 | 2 | 2.4 | 0 | 0 |
RobotsD2 | 8 | 3 | 1.86 | 3 | 1.86 | 0 | 0 |
RobotsD3 | 8 | 1 | 28.87 | 1 | 28.87 | 0 | 0 |
RobotsD4 | 8 | 3 | 23.7 | 3 | 23.7 | 0 | 0 |
RobotsD5 | 8 | 3 | 182.3 | 3 | 182.3 | 0 | 0 |
s27 | 4 | 2 | 115.23 | 1 | 0.02 | 1 | 115.21 |
s3271 | 8 | 2 | 773.11 | 0 | 0 | 2 | 773.11 |
term1 | 8 | 4 | 202.62 | 4 | 202.62 | 0 | 0 |
Toilet | 8 | 8 | 19.48 | 5 | 1.28 | 3 | 18.2 |
ToiletA | 8 | 5 | 44.88 | 1 | 4.43 | 4 | 40.45 |
ToiletC | 8 | 7 | 24.82 | 2 | 0.31 | 5 | 24.51 |
ToiletG | 7 | 7 | 0.07 | 7 | 0.07 | 0 | 0 |
Tree | 8 | 6 | 823.26 | 1 | 26.76 | 5 | 796.5 |
VonNeumann | 8 | 4 | 1336.24 | 0 | 0 | 4 | 1336.24 |
z4ml | 8 | 8 | 0.06 | 4 | 0.01 | 4 | 0.05 |
Solved Families: 72 |
Solver: semprop |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
Adder | 8 | 1 | 0 | 0 | 0 | 1 | 0 |
Blocks | 8 | 3 | 19.74 | 2 | 18.33 | 1 | 1.41 |
C432 | 8 | 6 | 788.4 | 3 | 0.13 | 3 | 788.27 |
C499 | 8 | 3 | 275.17 | 3 | 275.17 | 0 | 0 |
C6288 | 8 | 1 | 3.93 | 1 | 3.93 | 0 | 0 |
C880 | 8 | 2 | 7.39 | 2 | 7.39 | 0 | 0 |
Chain | 8 | 8 | 0.29 | 8 | 0.29 | 0 | 0 |
comp | 8 | 7 | 190.42 | 4 | 0.06 | 3 | 190.36 |
Connect2 | 8 | 8 | 4.71 | 5 | 3.93 | 3 | 0.78 |
Connect3 | 8 | 7 | 72.5 | 0 | 0 | 7 | 72.5 |
Connect4 | 8 | 7 | 2.85 | 0 | 0 | 7 | 2.85 |
Connect5 | 8 | 7 | 215.74 | 0 | 0 | 7 | 215.74 |
Connect6 | 8 | 4 | 2.71 | 0 | 0 | 4 | 2.71 |
Connect7 | 8 | 7 | 5.99 | 0 | 0 | 7 | 5.99 |
Connect8 | 8 | 5 | 5.23 | 0 | 0 | 5 | 5.23 |
Connect9 | 3 | 2 | 1.95 | 0 | 0 | 2 | 1.95 |
counter | 8 | 4 | 1.49 | 4 | 1.49 | 0 | 0 |
DFlipFlop | 8 | 8 | 4.62 | 0 | 0 | 8 | 4.62 |
Impl | 8 | 8 | 0.08 | 8 | 0.08 | 0 | 0 |
k_branch_n | 8 | 4 | 269.06 | 4 | 269.06 | 0 | 0 |
k_branch_p | 8 | 3 | 2.73 | 0 | 0 | 3 | 2.73 |
k_d4_n | 8 | 1 | 195.55 | 1 | 195.55 | 0 | 0 |
k_d4_p | 8 | 7 | 1263.09 | 0 | 0 | 7 | 1263.09 |
k_dum_n | 8 | 8 | 0.33 | 8 | 0.33 | 0 | 0 |
k_dum_p | 8 | 8 | 7.29 | 0 | 0 | 8 | 7.29 |
k_grz_n | 8 | 7 | 1488.06 | 7 | 1488.06 | 0 | 0 |
k_grz_p | 8 | 4 | 128.13 | 0 | 0 | 4 | 128.13 |
k_lin_n | 8 | 8 | 18.75 | 8 | 18.75 | 0 | 0 |
k_lin_p | 8 | 2 | 88.16 | 0 | 0 | 2 | 88.16 |
k_path_n | 8 | 8 | 6.14 | 8 | 6.14 | 0 | 0 |
k_path_p | 8 | 5 | 91.77 | 0 | 0 | 5 | 91.77 |
k_ph_n | 8 | 6 | 10.26 | 6 | 10.26 | 0 | 0 |
k_ph_p | 8 | 2 | 0.08 | 0 | 0 | 2 | 0.08 |
k_poly_n | 8 | 8 | 0.63 | 8 | 0.63 | 0 | 0 |
k_poly_p | 8 | 8 | 370.49 | 0 | 0 | 8 | 370.49 |
k_t4p_n | 8 | 2 | 350.15 | 2 | 350.15 | 0 | 0 |
k_t4p_p | 8 | 2 | 2.32 | 0 | 0 | 2 | 2.32 |
Logn | 4 | 4 | 5.31 | 2 | 0 | 2 | 5.31 |
mA-t2-2qbf-5cnf-100var | 18 | 12 | 26.04 | 1 | 15.59 | 11 | 10.45 |
mA-t2-2qbf-5cnf-150var | 18 | 11 | 894.27 | 2 | 894.1 | 9 | 0.17 |
mA-t2-2qbf-5cnf-50var | 18 | 15 | 668.25 | 2 | 0.03 | 13 | 668.22 |
mA-t2-3qbf-5cnf-100var | 18 | 13 | 4.28 | 6 | 0.04 | 7 | 4.24 |
mA-t2-3qbf-5cnf-150var | 18 | 15 | 987.34 | 7 | 389.13 | 8 | 598.21 |
mA-t2-3qbf-5cnf-50var | 18 | 18 | 94.55 | 9 | 18.68 | 9 | 75.87 |
mA-t2-4qbf-5cnf-100var | 18 | 13 | 0.96 | 2 | 0.02 | 11 | 0.94 |
mA-t2-4qbf-5cnf-150var | 18 | 13 | 4.32 | 2 | 0.02 | 11 | 4.3 |
mA-t2-4qbf-5cnf-50var | 18 | 16 | 2.18 | 4 | 1.6 | 12 | 0.58 |
mA-t2-5qbf-5cnf-100var | 18 | 14 | 250.94 | 8 | 229.29 | 6 | 21.65 |
mA-t2-5qbf-5cnf-150var | 18 | 12 | 67.46 | 6 | 0.06 | 6 | 67.4 |
mA-t2-5qbf-5cnf-50var | 18 | 16 | 55.34 | 9 | 54.15 | 7 | 1.19 |
mB-t2-2qbf-5cnf-100var | 18 | 18 | 11.5 | 1 | 11.22 | 17 | 0.28 |
mB-t2-2qbf-5cnf-150var | 18 | 18 | 0.16 | 0 | 0 | 18 | 0.16 |
mB-t2-2qbf-5cnf-50var | 18 | 18 | 0.13 | 1 | 0.03 | 17 | 0.1 |
mB-t2-3qbf-5cnf-100var | 18 | 18 | 0.13 | 2 | 0.01 | 16 | 0.12 |
mB-t2-3qbf-5cnf-150var | 18 | 18 | 0.2 | 2 | 0 | 16 | 0.2 |
mB-t2-3qbf-5cnf-50var | 18 | 18 | 0.1 | 2 | 0 | 16 | 0.1 |
mB-t2-4qbf-5cnf-100var | 18 | 18 | 0.16 | 2 | 0.01 | 16 | 0.15 |
mB-t2-4qbf-5cnf-150var | 18 | 18 | 0.19 | 2 | 0.01 | 16 | 0.18 |
mB-t2-4qbf-5cnf-50var | 18 | 18 | 0.16 | 2 | 0.01 | 16 | 0.15 |
mB-t2-5qbf-5cnf-100var | 18 | 18 | 0.2 | 2 | 0.01 | 16 | 0.19 |
mB-t2-5qbf-5cnf-150var | 18 | 18 | 0.26 | 2 | 0.01 | 16 | 0.25 |
mB-t2-5qbf-5cnf-50var | 18 | 18 | 0.16 | 4 | 0.04 | 14 | 0.12 |
MutexP | 7 | 3 | 6.17 | 3 | 6.17 | 0 | 0 |
RobotsD2 | 8 | 4 | 252.56 | 3 | 0.11 | 1 | 252.45 |
RobotsD3 | 8 | 2 | 619.83 | 1 | 0.49 | 1 | 619.34 |
RobotsD4 | 8 | 6 | 822.02 | 4 | 258.15 | 2 | 563.87 |
RobotsD5 | 8 | 6 | 1817.93 | 3 | 57.93 | 3 | 1760 |
s27 | 4 | 3 | 39.21 | 1 | 0.01 | 2 | 39.2 |
s3271 | 8 | 8 | 369.09 | 0 | 0 | 8 | 369.09 |
SzymanskiP | 8 | 2 | 207.68 | 0 | 0 | 2 | 207.68 |
term1 | 8 | 7 | 135.94 | 4 | 0.19 | 3 | 135.75 |
Toilet | 8 | 6 | 65.11 | 3 | 6.18 | 3 | 58.93 |
ToiletA | 8 | 7 | 29.78 | 1 | 5.9 | 6 | 23.88 |
ToiletC | 8 | 8 | 1.59 | 3 | 0.9 | 5 | 0.69 |
ToiletG | 7 | 7 | 0.04 | 7 | 0.04 | 0 | 0 |
Tree | 8 | 8 | 0.08 | 2 | 0.02 | 6 | 0.06 |
VonNeumann | 8 | 8 | 34.79 | 0 | 0 | 8 | 34.79 |
z4ml | 8 | 8 | 0.08 | 4 | 0.04 | 4 | 0.04 |
Solved Families: 78 |
Solver: ssolve |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
Adder | 8 | 1 | 0.02 | 0 | 0 | 1 | 0.02 |
Blocks | 8 | 2 | 0.13 | 1 | 0.09 | 1 | 0.04 |
C432 | 8 | 3 | 63.95 | 2 | 0.86 | 1 | 63.09 |
C499 | 8 | 2 | 0.03 | 2 | 0.03 | 0 | 0 |
Chain | 8 | 8 | 116.97 | 8 | 116.97 | 0 | 0 |
comp | 8 | 7 | 1431.6 | 4 | 173.78 | 3 | 1257.82 |
Connect2 | 8 | 8 | 4.28 | 5 | 3.46 | 3 | 0.82 |
Connect3 | 8 | 7 | 29.05 | 0 | 0 | 7 | 29.05 |
Connect4 | 8 | 7 | 2.18 | 0 | 0 | 7 | 2.18 |
Connect5 | 8 | 7 | 26.57 | 0 | 0 | 7 | 26.57 |
Connect6 | 8 | 4 | 1.98 | 0 | 0 | 4 | 1.98 |
Connect7 | 8 | 7 | 4.27 | 0 | 0 | 7 | 4.27 |
Connect8 | 8 | 5 | 3.96 | 0 | 0 | 5 | 3.96 |
Connect9 | 3 | 2 | 1.62 | 0 | 0 | 2 | 1.62 |
counter | 8 | 2 | 0.04 | 2 | 0.04 | 0 | 0 |
DFlipFlop | 8 | 8 | 1.81 | 0 | 0 | 8 | 1.81 |
Impl | 8 | 7 | 266.52 | 7 | 266.52 | 0 | 0 |
k_branch_n | 8 | 1 | 0.01 | 1 | 0.01 | 0 | 0 |
k_branch_p | 8 | 1 | 0.02 | 0 | 0 | 1 | 0.02 |
k_d4_p | 8 | 1 | 0.2 | 0 | 0 | 1 | 0.2 |
k_dum_n | 8 | 6 | 713.67 | 6 | 713.67 | 0 | 0 |
k_dum_p | 8 | 3 | 365.03 | 0 | 0 | 3 | 365.03 |
k_grz_n | 8 | 3 | 5.99 | 3 | 5.99 | 0 | 0 |
k_lin_n | 8 | 7 | 378.27 | 7 | 378.27 | 0 | 0 |
k_lin_p | 8 | 7 | 0.06 | 0 | 0 | 7 | 0.06 |
k_path_n | 8 | 5 | 803.47 | 5 | 803.47 | 0 | 0 |
k_path_p | 8 | 3 | 37.44 | 0 | 0 | 3 | 37.44 |
k_ph_n | 8 | 6 | 0.74 | 6 | 0.74 | 0 | 0 |
k_ph_p | 8 | 3 | 50.21 | 0 | 0 | 3 | 50.21 |
k_poly_n | 8 | 2 | 143.24 | 2 | 143.24 | 0 | 0 |
k_poly_p | 8 | 8 | 0.08 | 0 | 0 | 8 | 0.08 |
k_t4p_n | 8 | 1 | 333.46 | 1 | 333.46 | 0 | 0 |
k_t4p_p | 8 | 1 | 0.4 | 0 | 0 | 1 | 0.4 |
Logn | 4 | 4 | 15.18 | 0 | 0 | 4 | 15.18 |
mA-t2-2qbf-5cnf-100var | 18 | 17 | 446.33 | 2 | 0.01 | 15 | 446.32 |
mA-t2-2qbf-5cnf-150var | 18 | 14 | 45.42 | 2 | 0 | 12 | 45.42 |
mA-t2-2qbf-5cnf-50var | 18 | 18 | 9.81 | 3 | 0.11 | 15 | 9.7 |
mA-t2-3qbf-5cnf-100var | 18 | 16 | 26.12 | 7 | 25.94 | 9 | 0.18 |
mA-t2-3qbf-5cnf-150var | 18 | 13 | 2.03 | 5 | 0.09 | 8 | 1.94 |
mA-t2-3qbf-5cnf-50var | 18 | 18 | 219.2 | 9 | 216.11 | 9 | 3.09 |
mA-t2-4qbf-5cnf-100var | 18 | 16 | 1.44 | 4 | 0.01 | 12 | 1.43 |
mA-t2-4qbf-5cnf-150var | 18 | 17 | 79.86 | 5 | 2.08 | 12 | 77.78 |
mA-t2-4qbf-5cnf-50var | 18 | 18 | 91.3 | 6 | 0.03 | 12 | 91.27 |
mA-t2-5qbf-5cnf-100var | 18 | 13 | 94.45 | 7 | 93.81 | 6 | 0.64 |
mA-t2-5qbf-5cnf-150var | 18 | 12 | 0.29 | 6 | 0.08 | 6 | 0.21 |
mA-t2-5qbf-5cnf-50var | 18 | 15 | 9.67 | 8 | 8.37 | 7 | 1.3 |
mB-t2-2qbf-5cnf-100var | 18 | 18 | 0.29 | 1 | 0.07 | 17 | 0.22 |
mB-t2-2qbf-5cnf-150var | 18 | 18 | 0.22 | 0 | 0 | 18 | 0.22 |
mB-t2-2qbf-5cnf-50var | 18 | 18 | 0.11 | 1 | 0.01 | 17 | 0.1 |
mB-t2-3qbf-5cnf-100var | 18 | 18 | 0.16 | 2 | 0 | 16 | 0.16 |
mB-t2-3qbf-5cnf-150var | 18 | 18 | 0.22 | 2 | 0.02 | 16 | 0.2 |
mB-t2-3qbf-5cnf-50var | 18 | 18 | 0.17 | 2 | 0.02 | 16 | 0.15 |
mB-t2-4qbf-5cnf-100var | 18 | 18 | 0.18 | 2 | 0.01 | 16 | 0.17 |
mB-t2-4qbf-5cnf-150var | 18 | 18 | 0.33 | 2 | 0.02 | 16 | 0.31 |
mB-t2-4qbf-5cnf-50var | 18 | 18 | 0.11 | 2 | 0.02 | 16 | 0.09 |
mB-t2-5qbf-5cnf-100var | 18 | 18 | 0.2 | 2 | 0.02 | 16 | 0.18 |
mB-t2-5qbf-5cnf-150var | 18 | 18 | 0.24 | 2 | 0.03 | 16 | 0.21 |
mB-t2-5qbf-5cnf-50var | 18 | 18 | 0.15 | 4 | 0.01 | 14 | 0.14 |
MutexP | 7 | 7 | 0.13 | 7 | 0.13 | 0 | 0 |
RobotsD2 | 8 | 7 | 924.06 | 6 | 158.53 | 1 | 765.53 |
RobotsD3 | 8 | 3 | 93.64 | 3 | 93.64 | 0 | 0 |
RobotsD4 | 8 | 5 | 54.63 | 5 | 54.63 | 0 | 0 |
RobotsD5 | 8 | 7 | 1171.39 | 4 | 35.65 | 3 | 1135.74 |
s27 | 4 | 1 | 0 | 1 | 0 | 0 | 0 |
SzymanskiP | 8 | 8 | 246.58 | 0 | 0 | 8 | 246.58 |
term1 | 8 | 4 | 56.59 | 4 | 56.59 | 0 | 0 |
Toilet | 8 | 8 | 5.99 | 5 | 2.08 | 3 | 3.91 |
ToiletA | 8 | 7 | 456.76 | 1 | 0.46 | 6 | 456.3 |
ToiletC | 8 | 8 | 10.35 | 3 | 8.5 | 5 | 1.85 |
ToiletG | 7 | 7 | 0.05 | 7 | 0.05 | 0 | 0 |
Tree | 8 | 8 | 900.01 | 2 | 0.06 | 6 | 899.95 |
VonNeumann | 8 | 8 | 13.93 | 0 | 0 | 8 | 13.93 |
z4ml | 8 | 8 | 0.08 | 4 | 0.04 | 4 | 0.04 |
Solved Families: 73 |
Solver: WalkQSAT |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
Adder | 8 | 1 | 0.02 | 0 | 0 | 1 | 0.02 |
C432 | 8 | 2 | 0.04 | 2 | 0.04 | 0 | 0 |
C499 | 8 | 1 | 0.15 | 1 | 0.15 | 0 | 0 |
C5315 | 8 | 1 | 0.1 | 1 | 0.1 | 0 | 0 |
C880 | 8 | 2 | 11.14 | 2 | 11.14 | 0 | 0 |
Chain | 8 | 7 | 762.48 | 7 | 762.48 | 0 | 0 |
comp | 8 | 3 | 645.35 | 2 | 0.04 | 1 | 645.31 |
Connect2 | 8 | 6 | 2.27 | 2 | 1.32 | 4 | 0.95 |
Connect3 | 8 | 2 | 0.6 | 0 | 0 | 2 | 0.6 |
Connect4 | 8 | 5 | 1.28 | 0 | 0 | 5 | 1.28 |
Connect5 | 8 | 6 | 1.66 | 0 | 0 | 6 | 1.66 |
Connect6 | 8 | 6 | 37.91 | 0 | 0 | 6 | 37.91 |
Connect7 | 8 | 6 | 51.85 | 0 | 0 | 6 | 51.85 |
Connect8 | 8 | 2 | 4.5 | 0 | 0 | 2 | 4.5 |
counter | 8 | 2 | 0.14 | 2 | 0.14 | 0 | 0 |
DFlipFlop | 8 | 7 | 2.15 | 0 | 0 | 7 | 2.15 |
Impl | 8 | 8 | 0.03 | 8 | 0.03 | 0 | 0 |
jmc_quant | 8 | 1 | 754.37 | 1 | 754.37 | 0 | 0 |
k_branch_n | 8 | 1 | 0.02 | 1 | 0.02 | 0 | 0 |
k_d4_p | 8 | 1 | 1.57 | 0 | 0 | 1 | 1.57 |
k_dum_n | 8 | 5 | 94.57 | 5 | 94.57 | 0 | 0 |
k_dum_p | 8 | 3 | 49.37 | 0 | 0 | 3 | 49.37 |
k_grz_n | 8 | 5 | 746.15 | 5 | 746.15 | 0 | 0 |
k_grz_p | 8 | 4 | 646.67 | 0 | 0 | 4 | 646.67 |
k_lin_n | 8 | 3 | 17.31 | 3 | 17.31 | 0 | 0 |
k_lin_p | 8 | 1 | 0.03 | 0 | 0 | 1 | 0.03 |
k_path_n | 8 | 5 | 869.11 | 5 | 869.11 | 0 | 0 |
k_path_p | 8 | 3 | 846.72 | 0 | 0 | 3 | 846.72 |
k_ph_n | 8 | 6 | 0.82 | 6 | 0.82 | 0 | 0 |
k_poly_n | 8 | 2 | 544.2 | 2 | 544.2 | 0 | 0 |
k_t4p_n | 8 | 1 | 132.39 | 1 | 132.39 | 0 | 0 |
k_t4p_p | 8 | 1 | 2.27 | 0 | 0 | 1 | 2.27 |
mA-t2-2qbf-5cnf-100var | 18 | 6 | 1068.07 | 2 | 1067.93 | 4 | 0.14 |
mA-t2-2qbf-5cnf-150var | 18 | 3 | 425.58 | 1 | 425.47 | 2 | 0.11 |
mA-t2-2qbf-5cnf-50var | 18 | 6 | 492.09 | 2 | 0.1 | 4 | 491.99 |
mA-t2-3qbf-5cnf-100var | 18 | 7 | 2.47 | 6 | 0.04 | 1 | 2.43 |
mA-t2-3qbf-5cnf-150var | 18 | 5 | 1.49 | 5 | 1.49 | 0 | 0 |
mA-t2-3qbf-5cnf-50var | 18 | 15 | 602.91 | 8 | 15.61 | 7 | 587.3 |
mA-t2-4qbf-5cnf-100var | 18 | 9 | 665.49 | 2 | 0.02 | 7 | 665.47 |
mA-t2-4qbf-5cnf-150var | 18 | 6 | 898 | 2 | 0.03 | 4 | 897.97 |
mA-t2-4qbf-5cnf-50var | 18 | 15 | 98.96 | 4 | 13.59 | 11 | 85.37 |
mA-t2-5qbf-5cnf-100var | 18 | 6 | 0.1 | 6 | 0.1 | 0 | 0 |
mA-t2-5qbf-5cnf-150var | 18 | 6 | 0.08 | 6 | 0.08 | 0 | 0 |
mA-t2-5qbf-5cnf-50var | 18 | 16 | 1206.51 | 9 | 371.99 | 7 | 834.52 |
mB-t2-2qbf-5cnf-100var | 18 | 18 | 371.36 | 1 | 365.51 | 17 | 5.85 |
mB-t2-2qbf-5cnf-150var | 18 | 18 | 1.24 | 0 | 0 | 18 | 1.24 |
mB-t2-2qbf-5cnf-50var | 18 | 18 | 0.78 | 1 | 0.05 | 17 | 0.73 |
mB-t2-3qbf-5cnf-100var | 18 | 18 | 0.14 | 2 | 0.02 | 16 | 0.12 |
mB-t2-3qbf-5cnf-150var | 18 | 18 | 0.25 | 2 | 0 | 16 | 0.25 |
mB-t2-3qbf-5cnf-50var | 18 | 18 | 0.17 | 2 | 0.02 | 16 | 0.15 |
mB-t2-4qbf-5cnf-100var | 18 | 18 | 0.33 | 2 | 0.02 | 16 | 0.31 |
mB-t2-4qbf-5cnf-150var | 18 | 18 | 0.41 | 2 | 0.03 | 16 | 0.38 |
mB-t2-4qbf-5cnf-50var | 18 | 18 | 0.28 | 2 | 0.02 | 16 | 0.26 |
mB-t2-5qbf-5cnf-100var | 18 | 18 | 0.45 | 2 | 0.01 | 16 | 0.44 |
mB-t2-5qbf-5cnf-150var | 18 | 18 | 0.71 | 2 | 0.03 | 16 | 0.68 |
mB-t2-5qbf-5cnf-50var | 18 | 18 | 0.18 | 4 | 0.01 | 14 | 0.17 |
MutexP | 7 | 3 | 2.18 | 3 | 2.18 | 0 | 0 |
s27 | 4 | 2 | 172.99 | 1 | 0.09 | 1 | 172.9 |
SzymanskiP | 8 | 6 | 6.63 | 0 | 0 | 6 | 6.63 |
term1 | 8 | 2 | 2.84 | 2 | 2.84 | 0 | 0 |
Toilet | 8 | 6 | 0.13 | 5 | 0.12 | 1 | 0.01 |
ToiletA | 8 | 7 | 44.52 | 1 | 0.44 | 6 | 44.08 |
ToiletC | 8 | 8 | 1.01 | 3 | 0.07 | 5 | 0.94 |
ToiletG | 7 | 7 | 0.06 | 7 | 0.06 | 0 | 0 |
Tree | 8 | 6 | 803.97 | 1 | 173.14 | 5 | 630.83 |
VonNeumann | 8 | 2 | 0.87 | 0 | 0 | 2 | 0.87 |
z4ml | 8 | 5 | 0.07 | 4 | 0.05 | 1 | 0.02 |
Solved Families: 67 |
Solver: yquaffle |
FAMILY | TOTAL | SOLVED | TIME | SAT | SAT TIME | UNSAT | UNSAT TIME |
Adder | 8 | 1 | 0.13 | 0 | 0 | 1 | 0.13 |
Blocks | 8 | 7 | 264.94 | 2 | 0.7 | 5 | 264.24 |
C432 | 8 | 5 | 399.92 | 3 | 130.86 | 2 | 269.06 |
C499 | 8 | 4 | 40.21 | 3 | 1.86 | 1 | 38.35 |
C5315 | 8 | 3 | 527.79 | 2 | 139.47 | 1 | 388.32 |
C880 | 8 | 1 | 0.1 | 1 | 0.1 | 0 | 0 |
Chain | 8 | 5 | 315.09 | 5 | 315.09 | 0 | 0 |
comp | 8 | 8 | 30.91 | 4 | 0.07 | 4 | 30.84 |
Connect2 | 8 | 8 | 19.36 | 5 | 17.62 | 3 | 1.74 |
Connect3 | 8 | 6 | 10.42 | 0 | 0 | 6 | 10.42 |
Connect4 | 8 | 7 | 4.66 | 0 | 0 | 7 | 4.66 |
Connect5 | 8 | 6 | 3.81 | 0 | 0 | 6 | 3.81 |
Connect6 | 8 | 4 | 3.56 | 0 | 0 | 4 | 3.56 |
Connect7 | 8 | 7 | 7.67 | 0 | 0 | 7 | 7.67 |
Connect8 | 8 | 5 | 8.33 | 0 | 0 | 5 | 8.33 |
Connect9 | 3 | 2 | 3.73 | 0 | 0 | 2 | 3.73 |
counter | 8 | 4 | 0.46 | 4 | 0.46 | 0 | 0 |
DFlipFlop | 8 | 8 | 2.89 | 0 | 0 | 8 | 2.89 |
Impl | 8 | 8 | 0.08 | 8 | 0.08 | 0 | 0 |
k_branch_n | 8 | 1 | 0.01 | 1 | 0.01 | 0 | 0 |
k_branch_p | 8 | 1 | 1.38 | 0 | 0 | 1 | 1.38 |
k_d4_p | 8 | 1 | 0.13 | 0 | 0 | 1 | 0.13 |
k_dum_n | 8 | 4 | 249.14 | 4 | 249.14 | 0 | 0 |
k_dum_p | 8 | 4 | 550 | 0 | 0 | 4 | 550 |
k_grz_n | 8 | 2 | 74.71 | 2 | 74.71 | 0 | 0 |
k_grz_p | 8 | 3 | 437.31 | 0 | 0 | 3 | 437.31 |
k_lin_n | 8 | 5 | 165.37 | 5 | 165.37 | 0 | 0 |
k_lin_p | 8 | 8 | 3.47 | 0 | 0 | 8 | 3.47 |
k_path_n | 8 | 3 | 28.07 | 3 | 28.07 | 0 | 0 |
k_path_p | 8 | 3 | 165.42 | 0 | 0 | 3 | 165.42 |
k_ph_n | 8 | 7 | 180.16 | 7 | 180.16 | 0 | 0 |
k_ph_p | 8 | 3 | 2.35 | 0 | 0 | 3 | 2.35 |
k_poly_n | 8 | 1 | 0.03 | 1 | 0.03 | 0 | 0 |
k_poly_p | 8 | 8 | 0.15 | 0 | 0 | 8 | 0.15 |
k_t4p_p | 8 | 1 | 0.14 | 0 | 0 | 1 | 0.14 |
Logn | 4 | 4 | 0.89 | 2 | 0.04 | 2 | 0.85 |
mA-t2-2qbf-5cnf-100var | 18 | 5 | 14.67 | 1 | 1.06 | 4 | 13.61 |
mA-t2-2qbf-5cnf-150var | 18 | 3 | 70.73 | 0 | 0 | 3 | 70.73 |
mA-t2-2qbf-5cnf-50var | 18 | 12 | 223.88 | 1 | 0.01 | 11 | 223.87 |
mA-t2-3qbf-5cnf-100var | 18 | 5 | 120.77 | 3 | 37.68 | 2 | 83.09 |
mA-t2-3qbf-5cnf-150var | 18 | 2 | 0.97 | 2 | 0.97 | 0 | 0 |
mA-t2-3qbf-5cnf-50var | 18 | 11 | 46.51 | 7 | 44.9 | 4 | 1.61 |
mA-t2-4qbf-5cnf-100var | 18 | 2 | 6.55 | 2 | 6.55 | 0 | 0 |
mA-t2-4qbf-5cnf-50var | 18 | 5 | 875.8 | 3 | 32.58 | 2 | 843.22 |
mA-t2-5qbf-5cnf-100var | 18 | 2 | 0.43 | 2 | 0.43 | 0 | 0 |
mA-t2-5qbf-5cnf-150var | 18 | 1 | 6.6 | 1 | 6.6 | 0 | 0 |
mA-t2-5qbf-5cnf-50var | 18 | 5 | 9.01 | 5 | 9.01 | 0 | 0 |
mB-t2-2qbf-5cnf-100var | 18 | 11 | 13.45 | 0 | 0 | 11 | 13.45 |
mB-t2-2qbf-5cnf-150var | 18 | 11 | 927.59 | 0 | 0 | 11 | 927.59 |
mB-t2-2qbf-5cnf-50var | 18 | 15 | 73.31 | 1 | 29.49 | 14 | 43.82 |
mB-t2-3qbf-5cnf-100var | 18 | 15 | 6.83 | 1 | 6.61 | 14 | 0.22 |
mB-t2-3qbf-5cnf-150var | 18 | 14 | 0.3 | 0 | 0 | 14 | 0.3 |
mB-t2-3qbf-5cnf-50var | 18 | 17 | 24.69 | 2 | 0.15 | 15 | 24.54 |
mB-t2-4qbf-5cnf-100var | 18 | 6 | 0.1 | 0 | 0 | 6 | 0.1 |
mB-t2-4qbf-5cnf-150var | 18 | 7 | 0.32 | 0 | 0 | 7 | 0.32 |
mB-t2-4qbf-5cnf-50var | 18 | 11 | 735.68 | 1 | 1.12 | 10 | 734.56 |
mB-t2-5qbf-5cnf-100var | 18 | 12 | 0.23 | 0 | 0 | 12 | 0.23 |
mB-t2-5qbf-5cnf-150var | 18 | 12 | 0.28 | 0 | 0 | 12 | 0.28 |
mB-t2-5qbf-5cnf-50var | 18 | 13 | 7.92 | 2 | 7.53 | 11 | 0.39 |
MutexP | 7 | 2 | 46.31 | 2 | 46.31 | 0 | 0 |
RobotsD2 | 8 | 8 | 243.88 | 6 | 19.59 | 2 | 224.29 |
RobotsD3 | 8 | 7 | 2411.01 | 6 | 1692.64 | 1 | 718.37 |
RobotsD4 | 8 | 5 | 6.42 | 5 | 6.42 | 0 | 0 |
RobotsD5 | 8 | 7 | 218.65 | 4 | 5.51 | 3 | 213.14 |
s27 | 4 | 1 | 0.12 | 1 | 0.12 | 0 | 0 |
s3271 | 8 | 8 | 15.02 | 0 | 0 | 8 | 15.02 |
term1 | 8 | 7 | 146.79 | 4 | 0.3 | 3 | 146.49 |
Toilet | 8 | 6 | 68.71 | 3 | 36.75 | 3 | 31.96 |
ToiletA | 8 | 8 | 3.36 | 1 | 0.16 | 7 | 3.2 |
ToiletC | 8 | 8 | 1.74 | 3 | 1.44 | 5 | 0.3 |
ToiletG | 7 | 7 | 0.11 | 7 | 0.11 | 0 | 0 |
Tree | 8 | 8 | 39.2 | 2 | 39.17 | 6 | 0.03 |
VonNeumann | 8 | 8 | 28.88 | 0 | 0 | 8 | 28.88 |
z4ml | 8 | 8 | 0.03 | 4 | 0.01 | 4 | 0.02 |
Solved Families: 74 |