Add support for NotEqualTo !=

[LebedevRI]

These are perhaps not very high on anyone's priority list,
and models can avoid needing them, but they come up,
so i wonder if these would be welcomed? (if someone contributes them)?

1. Vector Set "monotonic": @constraint(model, [i=2:length(x)], x[i] <= x[x-i]) (configurable predicate)
2. Bridge (Int) x != 0 -> c ? (x >= 1) : (x <= -1)
3. Bridge (Int) x != y -> z = x - y; z != 0
4. Bridge x != y -> (x, y) in MOI.AllDifferent
5. Bridge x >= y -> x > y and x != y (configurable predicate)

[odow]

Let me comment on each case separately.

But 1), 2), and 3) are likely a "no." 4) is a possible. I don't understand why 5) would be useful.

Vector Set "monotonic": @constraint(model, [i=2:length(x)], x[i] <= x[x-i]) (configurable predicate)

For this, we'd need to introduce a new type Monotonic <: AbstractVectorSet end, and then a bridge from Monotonoic to Nonnegatives . This is pretty straight forward. But there is a trade off to consider. Each extra set in MOI requires code, tests, documentation, and on-going maintenance. I don't know if that is worth it just so that at the the JuMP level someone can write @variable(model, x[1:4] in Monotonic().

Bridge (Int) x != 0 -> c ? (x >= 1) : (x <= -1)

This would rewrite a MOI.NotEqualSet, which we don't have. I assume you mean the constraint to imply c in {0, 1}, c --> {x >= 1} and !c --> {x <= -1}. This is do-able, but it requires quite a lot of code. We'd also need to add the operator != to JuMP.

Bridge (Int) x != y -> z = x - y; z != 0

if you did the x != 0 case, then this would automatically be handled by the SlackBridge.

Bridge x != y -> (x, y) in MOI.AllDifferent

Okay. This has merit. Instead of adding a MOI.NotEqual set, we could just leverage the existing AllDifferent, which already has a bridge to MILP. It would mean adding support for a != b --> [a, b] in MOI.AllDifferent(2) at the JuMP level.

But that's easy. Reified is a good example to follow, replacing Val{:(<-->)} with Val{:(!=)}:

https://github.com/jump-dev/JuMP.jl/blob/a55edea07f2c3bb026d89f4e7fe88ae4755a810f/src/reified.jl#L6-L31

Bridge x >= y -> x > y and x != y (configurable predicate)

Which solver is this transformation needed for?

[LebedevRI]

@odow thank you for taking a look!

Vector Set "monotonic": @constraint(model, [i=2:length(x)], x[i] <= x[x-i]) (configurable predicate)

For this, we'd need to introduce a new type Monotonic <: AbstractVectorSet end, and then a bridge from Monotonoic to Nonnegatives . This is pretty straight forward. But there is a trade off to consider. Each extra set in MOI requires code, tests, documentation, and on-going maintenance. I don't know if that is worth it just so that at the the JuMP level someone can write @variable(model, x[1:4] in Monotonic().

My main motivation is what we've just discussed in jump-dev/JuMP.jl#3651,
it results in rather more readable model print, and is somewhat easier to write.
But let's leave that for later.

<...>

Bridge (Int) x != y -> z = x - y; z != 0

if you did the x != 0 case, then this would automatically be handled by the SlackBridge.

Aha! Okay.

Bridge x != y -> (x, y) in MOI.AllDifferent

Okay. This has merit. Instead of adding a MOI.NotEqual set, we could just leverage the existing AllDifferent, which already has a bridge to MILP. It would mean adding support for a != b --> [a, b] in MOI.AllDifferent(2) at the JuMP level.

My main problem is that said bridge (CountDistinctToMILPBridge) looks scary.

MathOptInterface.jl/src/Bridges/Constraint/bridges/count_distinct.jl

Lines 29 to 30 in 873d219

	Then, we introduce new binary variables ``y_j``, which are ``1`` if a variable
	takes the value ``j`` in the optimal solution and ``0`` otherwise.

so if in x != 0, x is known to be in [-100, 100], we introduce at least ~201 variables,
and it doesn't work at all if the range is unknown?
... while 2. would just work and only require a single new variable.

So while i do agree that this general bridge
is good as a generalization, it may not optimal.

Perhaps 4. can be an intermediate solution,
with 2. being an improvement later on?

Bridge x >= y -> x > y and x != y (configurable predicate)

Which solver is this transformation needed for?

Err, i, of course, meant x > y -> x >= y and x != y :)

[LebedevRI]

So while i do agree that this general bridge
is good as a generalization, it may not optimal.

(IOW it looks to me almost as if those alldifferent/count MLIP bridges should use this 2. trick.)

[odow]

There's certainly room to have improved formulations for the ToMILP bridges. I wrote very basic reformulations for correctness and to get something working, not because it is necessarily the best reformulation.

One design consideration that I think we agree on is that we want to, as far as possible, limit the number of functions and sets in MOI and JuMP. We don't want to turn into constraint programming where there are N different ways of writing something, and the modeling language supports M different functions, but each solver supports only a very small amount.

Normally, a good rule of thumb is that we only introduce a set if a solver has native support for it.

Perhaps as a compromise, there's room for a package of JuMP reformulations. This would make the models easier to write:

julia> module JuMPReformulations

       using JuMP

       function monotonic(x::Vector{VariableRef})
           @constraint(owner_model(first(x)), x[1:end-1] .<= x[2:end])
           return
       end

       function not_equal(x::VariableRef, y::VariableRef)
           @assert is_integer(x) && is_integer(y)
           @assert owner_model(x) === owner_model(y)
           model = owner_model(x)
           z = @variable(model, z)
           @constraint(model, z --> {x >= y + 1})
           @constraint(model, !z --> {x <= y - 1})
           return
       end

       end
WARNING: replacing module JuMPReformulations.
Main.JuMPReformulations

julia> using JuMP

julia> model = Model();

julia> @variable(model, x[1:2], Int);

julia> JuMPReformulations.monotonic(x)

julia> JuMPReformulations.not_equal(x[1], x[2])

julia> print(model)
Feasibility
Subject to
 x[1] - x[2] ≤ 0
 !z --> {x[1] - x[2] ≤ -1}
 x[1] integer
 x[2] integer
 z --> {x[1] - x[2] ≥ 1}

[LebedevRI]

Yes, i very much understand being vary of adding ever more stuff to support.
I'm bringing this up because these seem to not be too "outland-ish special-cases",
that keep coming up. I'm sure i've seen ordering being mentioned at least once
on discuss, and i've personally found it to be generally useful to severely constrain
the problem space. And non-equality / strict inequality is a rather known limitation of LP,
that we can easily sidestep for integers.

Again, everyone's mileage may vary, not everything will be useful for everyone,
i'm just really hoping that these can be recognized as worthwhile having.

To summarize, let me look into the seemingly least controversial one,

Bridge x != y -> (x, y) in MOI.AllDifferent

[odow]

because these seem to not be too outland-ish special-cases

True, except that the reformulations often perform poorly. I'm hesitant to add something like != to JuMP because people will miss-use it. I can see people asking why x and y need to be integer, or why a model with != runs so much slower than ==. It's also a reason why we haven't added >, because people really, really want to use x > 0 and yet solvers cannot support that.

In some ways, forcing people to write an expansion for != forces them to think about what it is they are trying to model.

[LebedevRI]

Ack, i've actually thought/wondered about that, but in the more general sense:
now that there's generic non-linear support, is there any way to opt-out of it? :)
Not that there is a specific need, but just because.

As for performance, sure, but i can't imagine
c in {0, 1}, c --> {x >= 1} and !c --> {x <= -1} would perform that bad.

[odow]

now that there's generic non-linear support, is there any way to opt-out of it?

No

c in {0, 1}, c --> {x >= 1} and !c --> {x <= -1} would perform that bad.

The other issue is that it's very sensitive to the formulation being able to detect that x is integer:

model = Model()
@variable(model, x, Int)
@variable(model, y)
@constraint(model, x == y)
@constraint(model, x != 0)  # Works
@constraint(model, 2x != 2)  # Fails
@constraint(model, y != 0)  # Fails

[LebedevRI]

The other issue is that it's very sensitive to the formulation being able to detect that x is integer:

So we'd make it picky in so that it's operands must be [Binary] variables.