MiniZinc.jl icon indicating copy to clipboard operation
MiniZinc.jl copied to clipboard

Consider supporting some more of MiniZinc's Graph sets

Open LebedevRI opened this issue 1 year ago • 7 comments

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).

LebedevRI avatar Jul 18 '24 03:07 LebedevRI

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.

odow avatar Jul 18 '24 04:07 odow

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.

LebedevRI avatar Jul 18 '24 04:07 LebedevRI

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 avatar Jul 18 '24 23:07 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

odow avatar Jul 19 '24 04:07 odow

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...

LebedevRI avatar Jul 19 '24 22:07 LebedevRI

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.

odow avatar Jul 22 '24 04:07 odow

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

blegat avatar Jul 23 '24 17:07 blegat