Note: this problem is based on a similar one from the
Logic in Information Technology subject at Barcelona School of Informatics.
Solve the following exercise by means of a reduction to
SAT:
- A league comprises of $n$ teams (with $n$ even) and $n-1$ rounds.
At each round, each team plays with another team, so that in the end every
team has played with every other team once. Each team has a stadium. Matches
can be played either at home (in its own stadium) or away (in the opponent’s
stadium). Furthermore, we have the following constraints:
- Fairness: every team must play either $n/2$ or $n/2-1$ games away.
- No tripititions: no team should play at home or away three times in a row.
- Stadium availability: certain stadiums are not available at certain
rounds, so the corresponding teams must play away that round.
- Shared stadium: certain pairs of teams share a stadium, so they cannot
play both at home at the same round. When they play against each other, one
of them takes the role of home team and the other away team. Shared stadiums
are never unavailable.
The input of the exercise and the output with the solution (when the input is
solvable) are as follows: