Miller–Tucker–Zemlin (MTZ) derivation ¹:

1. Introduce a time of visitation \(t_i \in \{1, \ldots, n - 1\}\).

   \begin{align*} x_{ij} = 1 & \implies t_i < t_j && \text{\(i\) visited before \(j\)} \\ & \implies t_j > t_i &&\text{swap sides} \\ & \implies t_j \geq t_i + 1 && \text{favor \(\geq\) over \(>\)} \\ \end{align*}

2. Linearize the implication with the Big-M trick.

   \begin{equation*} t_j \geq t_i + 1 - M \cdot (1 - x_{ij}) \end{equation*}

3. Half-way there!

   \begin{align*} x_{ij} = 1 & \stackrel{\checkmark}{\implies} t_j \geq t_i + 1 \\ x_{ij} = 0 & \stackrel{?}{\implies} t_j \geq t_i + 1 - M \end{align*}

4. Find the smallest \(M\) that works for all \(t_i\) and \(t_j\).

   \begin{equation*} M = n \end{equation*}

5. Substitute \(M\) for \(n\).

   \begin{equation*} t_j \geq t_i + 1 - n (1 - x_{ij}) \end{equation*}

for i in range(n):
    for j in range(1, n):
        if i != j:
            model.add(t[j] >= t[i] + 1 - n * (1 - x[i][j]))