About extended reformulation for integer linear programming, you can be interested in this lecture by Vanderbeck and Wolsey, and the corresponding research report. They formalize reformulations, especially what are good reformulations, and described techniques to build them systematically. They give many examples of reformulations for some well-known discrete optimization problems.
There is also some research about reformulations of quadratic binary programs. For example, look at the work of Billionnet, Elloumi, and Lambert.
As well said in the comment, formulating problems mathematically is more than science. Now, formulating and reformulating problems to be solved at best by solvers is an experimental work. The designers of solvers generally give some modeling guidelines and illustrate them on example problems. But sometimes, even the designers of the solvers themselves cannot say what formulations will be better solved by an optimization engine. Just because optimization engines are complex systems and, like any complex system, their outputs are not fully predictable.
Modeling techniques are generally less emphasized in research and teaching in comparison with solving techniques. At LocalSolver, we love implementing and improving solving techniques in a very agnostic fashion. But we are also convinced that "modeling is the master and computation the servant" as John Hooker nicely wrote. In particular, we are convinced that the classical Boolean modeling approach, traditionally used in integer linear programming, is not the best one to capture the structure of combinatorial problems, which is critical to solving them efficiently in practice. We have introduced fresh-new modeling features to model discrete problems like routing, scheduling, packing, or clustering problems. For example, for the TSP you cited in your question, ideas are given in previous posts like this one.
