this global requirement that makes TSP a hard problem. The MTZ and DFJ formulations differ in how they express this final requirement as linear constraints. Miller–Tucker–Zemlin formulation In addition to the variables as above, there is for each a dummy variable that keeps track of the order in which the cities are visited, counting from city ; the interpretation is that implies city is visited before city . For a given tour (as encoded into values of the variables), one may find satisfying values for the variables by making equal to the number of edges along that tour, when going from city to city . Because linear programming favours non-strict inequalities () over strict (), we would like to impose constraints to the effect that if . Merely requiring would not achieve that, because this also requires when , which is not correct. Instead MTZ use the linear constraints for all distinct where the constant term provides sufficient slack that does not impose a relation between and . The way that the variables then enforce that a single tour visits all cities is that they increase by (at least) for each step along a tour, with a decrease only allowed where the tour passes through city . That constraint would be violated by every tour which does not pass through city , so the only way to satisfy it is that the tour passing city also passes through all other cities. The MTZ formulation of TSP is thus the following integer linear programming problem: The first set of equalities requires that each city is arrived at from exactly one other city, and the second set of equalities requires that from each city there is a departure to exactly one other city. The last constraints enforce that there is only a single tour covering all cities, and not two or more disjointed tours that only collectively cover all cities. To prove this, it is shown below (1) that every feasible solution contains only one closed sequence of cities, and (2) that for every single tour covering all cities, there are values for the dummy variables that satisfy the constraints. To prove that every feasible solution contains only one closed sequence of cities, it suffices to show that every subtour in a feasible solution passes through city 1 (noting that the equalities ensure there can only be one such tour). For if