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:

• n: int
  unavailable_stadiums: array of array [2] of int
  shared_stadiums: array of array [2] of int
  

  The input details the number $n$ of teams, the list of pairs $(i,j)$ indicating that the stadium of team $i\in\{0,\ldots,n-1\}$ at round $j\in\{0,\ldots,n-2\}$ is unavailable, and the list of pairs $(i,j)$ indicating whether the distinct teams $i,j\in\{0,\ldots,n-1\}$ share a stadium.

• matches: array of array of struct {
     opponent: int
     visitant: int
  }
  

  The output contains the details of the matches. It is a two-dimensional array with one row per team ($n$ rows in total) and one column per round ($n-1$ columns in total). The entry $(i,j)$ is a struct with two fields. The field matches[i][j].opponent is the identifier of the team against which the team with identifier $i$ played in the round $j$. The field matches[i][j].visitant is either $0$ or $1$, a $0$ meaning that the team $i$ played at home in the round $j$, whereas a $1$ meaning that it played away.