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

[IgnaceBleukx]

Merged current master into this PR, and update the decomposition with the new style (e.g, avoid making aux vars).
Turns out it was not too complicated to make it work in reified contexts too! (Verified using solveAll() on both positive and negative constraint)

Also a noticeable speedup compared to the standard decomposition -- examples/tsp.py runs in 0.3s instead of 5s on master.

There is a bizarre bug in Exact/the Exact interface which causes the CI to fail

[tias]

the regular decompose does an _no_partial_functions on order, while the linear decompose does not. An omission? or is the regular one too strict?

[IgnaceBleukx]

In the linear one, we only index with constants, so no need to safen here : )
There is also the bounds-restricting constraint in the linear decompose, which also ensures the constraint fails when one of the sucessors is invalid

[tias]

I see, its good to explain and be explicit on such things...

e.g. that we need no partial becuase we are indexing with an expression that could be out of bounds (updated doc)

also, explaining the new decomposition, e.g. that one forbids self-loops and the other enforces an increasing counter/topological order by which loops are not allowed because they would point to a lower order-nr (udpated doc)

assuming you agree with the doc comments added, do merge

[IgnaceBleukx]

Hmm enabling the "not_circuit" test for all solvers reveals some problems... Will investigate and request for a re-review when fixed

[tias]

forgot to commit the second doc update, on the order part.

[IgnaceBleukx]

So as it turns out, the modifications I made to the MTZ encoding don't work for negative contexts after all...
I tried a bunch of things to make it work, but all of them turn ugly very quickly...
Actually, even for positive context, I cannot get the solution counts to match...

E.g.., cp.Model(bv.implies(cp.Circuit(x)), bv == False)).solveAll() should get the exponential number of solutions for all values of x, but it generates many more as the aux vars are not totally defined by the user variables.

So in summary, the decomposition works but in limited cases:

• Toplevel: all fine
• Nested positive: generates more solutions (in aux vars, correct for user vars)
• Nested negative: wrong

How should we proceed? We could use this PR to introduce the "decompose_positive" function for globals after all? Then the future MDD-decomp can build on this one.

[IgnaceBleukx]

Converting this PR to draft again, as we first need a way for determining which decomposition to call at toplevel/positive/nested contexts.
Will re-open after

[tias]

re-implemented as part of #1006