[Bridge] implement special case for x != y in CountDistinctToMILPBridge

[odow]

Closes #2405

This PR implements a much stronger reformulation for the special case of [2, x ,y] in CountDistinct which is created by [x, y] in AllDifferent(2), a.k.a. x != y.

[odow]

I don't know why you can't see the coverage: https://app.codecov.io/github/JuMP-dev/MathOptInterface.jl/pull/2416

[LebedevRI]

@odow FWIW, thank you for looking into this!
It will be unfortunate if this expansion will still not handle the bound-less case, but if that is what you think is best...

[odow]

but if that is what you think is best...

Can you provide a reformulation that would let us write this as a MILP (excluding indicator constraints) without knowing the bounds?

[LebedevRI]

Speaking of proofs, can you show the proof?
Are bounds inclusive or exclusive?
This doesn't quite proof for me: https://godbolt.org/z/3nEEdr1hj https://alive2.llvm.org/ce/z/tUeBwc
https://godbolt.org/z/Mc87q4cjf https://alive2.llvm.org/ce/z/otmnsE

[odow]

I don't understand the relevance of the links.

We're looking for a MILP reformulation of

| x | >= 1

where x is free, and we can't choose an arbitrary big-M like M = 1e6

[LebedevRI]

I don't understand the relevance of the links.

Link 1 shows the true variant of the constraint (src), and naive re-implementation of this constraint in C (tgt),
Link 2 feeds the implementations to an SMT solver, which says that they are not equivalent.

[odow]

Ugh. I can't read or type. I typed z-1 instead of 1-z at the top and then blindly followed through without thinking.

[LebedevRI]

but if that is what you think is best...

Can you provide a reformulation that would let us write this as a MILP (excluding indicator constraints) without knowing the bounds?

Back when writing that comment, i didn't quite noticed that this was using yet another reformulation,
one without indicator constraints. I don't know if this one can be formulated without bounds.

It would be nice to either see either an exhaustive (correctness) test for this, or a non-manual proof.
But please feel free to ignore me on that! :)

[odow]

It would be nice to either see either an exhaustive (correctness) test for this, or a non-manual proof.

This hints at a much larger issue. We don't have any tools to check the correctness of JuMP models, and it is very easy (as just demonstrated) to make small mistakes. I'll open a JuMP issue.

[odow]

See jump-dev/JuMP.jl#3664