Consider supporting some more of MiniZinc's Graph sets

[LebedevRI]

It would be good if there would be a set/sets that would allow to encode that two specific nodes of a graph (modelled as a NxN boolean adjacency matrix) are / are not reachable from one another.

This is an obvious thing given an actual, non-symbolic, graph e.g. by simply looking at the graph reachability matrix, which can be computed by raising the boolean adjacency matrix to a certain power (by performing matrix self-multiplication multiple times). but that doesn't so nicely translate to JuMP.

Its easy to model with quadratic constraints, but the performance, even on the most toy examples seems unsatisfactory.

Its straight-forward to model binary matrix multiplication with linear constraints, but the number of constraints scales with cube of the number of graph nodes, so even on the most toy example that results in millions of constraints, and while the solver performance seems better, it's still unsatisfactory. I haven't looked deeper, but even just creating those constraints via @constraint can take minutes.

I haven't looked into modelling it as a NLP problem, partly because that iface is still unsupported by both HiGHS and SCIP, and i'm not sure if there even is any solver that supports said new iface and (MI)LP constraints.

Thus, the only thing left to check is constraint programming. https://docs.minizinc.dev/en/stable/lib-globals-graph.html#mzn-globals-graph-reachable seems useful, but i'm not sure about the inverse (non-reachability).

[odow]

I'm not averse to this, but I'm also not strongly in favor either.

It might be better if we found a way to communicate arbitrary MiniZinc constraints in MiniZinc.jl directly.

[LebedevRI]

It might be better if we found a way to communicate arbitrary MiniZinc constraints in MiniZinc.jl directly.

Yes indeed, i've thought about that too.

[odow]

I have transferred this issue to MiniZinc.jl.

If we come up with something that is broadly useful, we can consider adding it to MOI.

[odow]

So perhaps the right approach is to define a bunch of MOI sets in MiniZinc.jl

predicate reachable(int: N,
                        int: E,
                        array [int] of int: from,
                        array [int] of int: to,
                        var int: r,
                        array [int] of var bool: ns,
                        array [int] of var bool: es)

would become something like:

"""

## Usage

@constraint(model, [r; ns; es] in MiniZinc.Reachable(...))

"""
struct Reachable <: MOI.AbstractVectorSet
    N::Int
    E::Int
    from::Vector{Int}
    to::Vector{Int}
end

function _write_constraint(
    io::IO,
    predicates::Set,
    variables::Dict,
    f::MOI.VectorOfVariables,
    s::Reachable,
)
    # something here
    return
end

[LebedevRI]

One more thing i hadn't checked yet, was User-defined operators (UserDefinedFunction), but apparently out of all the (non-Comm.) solvers that supports (MI)LP, none support UserDefinedFunction. Oh well...

[odow]

MiniZinc.jl cannot support user-defined functions because it is a file-based I/O. The user-defined functions supply only callback oracles in Julia.

[blegat]

The adjacency matrix is a matrix of boolean JuMP variables and the nodes are fixed ? Can't you do a sort of MAX-FLOW/MIN-CUT formulation ? Nodes are unreachable is equivalent to the MAX-FLOW/MIN-CUT being zero. If you make the classical formulation and you force the flow for each edge to be zero if the boolean of the adjacency matrix is false (or the corresponding action for MIN-CUT), then is should probably work