MTZ-style decomposition of Circuit

[IgnaceBleukx]

Ok, so I could not help myself and implement a custom decomposition for the Circuit constraint in linearize_constraint.
Its inspired by TSP models for MIP: https://how-to.aimms.com/Articles/332/332-Miller-Tucker-Zemlin-formulation.html

This allows us to run all of the examples with gurobi within 20s, so I think its a nice quality of life improvement for us :).

[JoD]

MTZ is a weakened form of the existing decomposition (happy to show the derivation) that assumes the circuit is at top level. In other words, the decomposition is not a "top level definition" + local constraints. There is a way to use these, but right now it will be incorrect under negation.

[JoD]

(nonetheless, kudos for being on the lookout out for the most efficient decomposition!)

[Wout4]

I think it's weird to decompose in other places than decompose_globals, I know we discussed this a bit elsewhere as well but if a global has multiple decompositions the right place for those decompositions are in the global itself (so a decompose_linear which defaults to the normal decomposition making it backwards compatibel)

[Wout4]

So I did some testing, and this decomposition is indeed about 3x faster for gurobi, but only works in the non reified case.
Also checked the Alldifferent decomposition in linearize (it has a todo about performance) and it is actually twice as slow as the normal decomposition and also does not work in reified case.

[Dimosts]

Made some tests with room assignment problems that have many alldifferents.

What you say seems true in small problems with just a few alldifferent constraints, but when I created a larger problem (with 88 alldifferent constraints). I have the following results:

With linear decomposition of alldifferent constraints:

• Transformations time: 21.3196222782135
• Solve time: 3.688000202178955

With the normal decomposition of alldifferent constraints:

• Transformations time: 31.12852382659912
• Solve time: 13.422210454940796

Thus, the linear decomposition is much more efficient in solving (which is the important part) and even faster in the transformations.

[tias]

This should be reconsidered as part of, or after #836