I am given two formulations, that is, two integer programs
$ (IP1)\quad \min \{c^tx \mid Ax\geq a, x\in Z^n\} $
and
$ (IP2)\quad \min \{d^ty \mid By\geq b, y\in Z^m\} $
and I wish to check whether they describe the same problem. That is, I wish to know, whether the set of integer feasible points for both models is the same. This is, however, complicated by the fact that $x$ and $y$ variables may live in totally different spaces (think of the one-constraint binary program for 0-1 knapsack, and the equivalent longest-path flow formulation that mimics the dynamic program --- toootally different models, same problem).
I know that I need a transformation/projection between $(P1)$ and $(P2)$, and for the above knapsack example (and many others), I know how to do this. But I am interested in a generic answer.
I expect that, even when this can be settled in theory (which I assume to be very hard already), computationally doing the "proof" is totally intractable -- and I am ultimately interested in doing a computational check of the equivalence of the two models. Therefore, I can do with a "high probability" argument. What we currently do it to (a) have a reference formulation, (b) explicitly prescribe the transformation (a set of variables that has to be used by every formulation, maybe by explicitly modeling the projection), then (c) use specific instances, (d) put "random" objective functions, (e) solve to optimality, and (f) check whether the same (?) solution occurs -- well, there can be many optimal solutions... so, all this is not so trivial.
I cannot help it but I think of Benders here as well.