decibyte badminton plan

output

('Aske', 'Kylling', 'Bamse', 'Luna', 'ForlænsBaglæns')
('Aske', 'Bamse', 'ForlænsBaglæns', 'Luna', 'Kylling')
('Aske', 'Kylling', 'Bamse', 'ForlænsBaglæns', 'Luna')
('Aske', 'Bamse', 'ForlænsBaglæns', 'Kylling', 'Luna')
('Aske', 'Luna', 'Bamse', 'ForlænsBaglæns', 'Kylling')
('Aske', 'Kylling', 'ForlænsBaglæns', 'Luna', 'Bamse')
('Bamse', 'ForlænsBaglæns', 'Kylling', 'Luna', 'Aske')
('Aske', 'Luna', 'ForlænsBaglæns', 'Kylling', 'Bamse')
('Aske', 'Bamse', 'Kylling', 'Luna', 'ForlænsBaglæns')
('Aske', 'ForlænsBaglæns', 'Bamse', 'Kylling', 'Luna')
('Bamse', 'Luna', 'ForlænsBaglæns', 'Kylling', 'Aske')
('Aske', 'Luna', 'Bamse', 'Kylling', 'ForlænsBaglæns')
('Aske', 'ForlænsBaglæns', 'Bamse', 'Luna', 'Kylling')
('Bamse', 'Kylling', 'ForlænsBaglæns', 'Luna', 'Aske')
('Aske', 'ForlænsBaglæns', 'Kylling', 'Luna', 'Bamse')

solve.py

"""z3 based solution to the challenge posted in
https://twitter.com/decibyte/status/1283846230238527488

I.e., for a given collection of badminton players, find a match plan for double
badminton matches so that all possible matches take place, and moreover, no
team of two players play together for two matches in a row.
"""
from itertools import permutations

from z3 import Int, Or, Solver


players = ['Bamse', 'Kylling', 'Aske', 'Luna', 'ForlænsBaglæns']

# We first determine all possible matches between the players and get rid of
# all duplicate matches. Doing so amounts to taking /all/ permutations of the
# players and breaking the relevant symmetries: Order the players the players
# in each team to avoid getting solutions that are identical up to the team
# members being swapped, then order the teams themselves to avoid solutions
# where the teams are swapped, and finally, order all benched players to avoid
# having solutions that only differ by where on the bench the benched players
# are sitting.
# In the case of 5 players, for example, the result contains only 15 of the
# total 120 permutations.
perms = [p for p in permutations(players)
         if p[0] < p[1] and p[2] < p[3]
         and p[0] < p[2]
         and list(p[4:]) == sorted(p[4:])]

# Now all that remains is reordering the permutations above to enforce the
# constraint that no two players play together two matches in a row. Without
# even looking at the structure of the problem, we notice that we can solve
# this as an instance of the Hamiltonian path problem: Consider the graph where
# vertices are the permutations above, and where there is an edge between two
# vertices only if the corresponding vertices represent matches that can follow
# immediately after each other. Then a solution to the problem is a path in the
# graph that visits every vertex exactly once.
# We use the integer indices of the permutations to represent the vertices in
# the graph, and represent the entire graph as a dictionary
# { v: list of all vertices sharing an edge with v }
g = {i: [j for j, p2 in enumerate(perms)
         if p1[0:2] != p2[0:2]
         and p1[2:4] != p2[2:4]
         and p1[0:2] != p2[2:4]
         and p1[2:4] != p2[0:2]]
     for i, p1 in enumerate(perms)}

# The Hamiltonian path problem can be solved in numerous ways (even if no
# efficient solutions are known as the problem is, in general, NP-complete).
# Here, mostly to showcase its capabilities and illustrate how the problem can
# be solved with only a few lines of code, we treat the problem as a constraint
# satisfaction problem (CSP) and solve it with z3 (which is marketed as a
# theorem prover/satisfiability modulo theories solver, but works just fine for
# our purposes as well). Otherwise, for small problems, the easier algorithm to
# understand is probably backtracking search: Iteratively add one match to the
# plan at a time in a depth-first fashion, and if constraint violations occur,
# move back to a point where there are still options to try.
n = len(g)  # Number of vertices; 15 in the five player case.
# We follow
# https://github.com/Z3Prover/z3/blob/master/examples/python/hamiltonian/hamiltonian.py
# and create n integer variables that represent the resulting order: if j is a
# permutation, then m[j] represents the place in the match plan that j will be
# taking place. That is, if m[0] is 10, then the first permutation will be the
# eleventh match overall.
m = list(map(Int, range(n)))
s = Solver()

# Time to add the constraints
for i in range(n):
    # The index of each map is an element in range(n).
    s.add(m[i] >= 0, m[i] < n)
    for j in range(i + 1, n):
        # All match indices are different. Typically in CSP solvers this is
        # handled by adding an "all-different" constraint, but here we just add
        # the constraints by hand.
        s.add(m[i] != m[j])
    # And finally the main one: If permutation i has index m[i], then the
    # permutation whose index is m[i] + 1 must be one of the matches that can
    # be reached from i; i.e. m[i] + 1 is m[j] for some j in g[i], which can
    # be represented by an or-constraint. One edge-case is the final match
    # in the plan where we make no requirement on the following match (as
    # opposed to what would be the case if this were a Hamiltonian /cycle/
    # problem).
    s.add(Or([m[j] == m[i] + 1 for j in g[i]] + [m[i] == n - 1]))

# In z3, we first check satisfiability, then get the actual solution (a "model"
# in logic terminology).
s.check()
model = s.model()

# At the end of the day, we want the matches in order of increasing index where
# m contains them in order of increasing permutation. We just consider the
# result as a permutation of range(n) and invert that permutation to get our
# desired result.
res = [model[m[i]] for i in range(n)]
for match in range(n):
    print(perms[res.index(match)])