Check if there is a path that connects two vertices in a graph using MiniZinc

Question

I'm trying to make a constraint to check if there is a path from a vertex A to a vertex B in a graph. I've already made a constraint that returns the path itself, but I also need a function that returns a bool indicating if the path exists or not.

I've already spent a lot of time on it, but none of my tries was successful...

Does anyone has any idea of what could I do?

Here is the function that I've made that returns the path itself, wherein graph is an adjacency matrix and source and target are the vertexes A and B:

function array [int] of var int: path(array[int,int] of int: graph, int: source, int: target)::promise_total =
let {
    set of int: V = index_set_1of2(graph);
    int: order = card(V);
    set of int: indexes = 1..order;
    array[indexes] of var (V union {-1}): path_array;
    var indexes: path_nodes_count; % the 'size' of the path

    constraint assert(index_set_1of2(graph) = index_set_2of2(graph), "The adjacency matrix is not square", true);
    constraint assert({source, target} subset V, "Source and target must be vertexes", true);

    constraint path_array[1] == source;
    constraint path_array[path_nodes_count] == target;

    constraint forall(i in 2..path_nodes_count) ( graph[ path_array[i-1], path_array[i] ] != 0 );

    constraint forall(i in indexes, where i > path_nodes_count) ( path_array[i] = -1 );

    constraint forall(i,j in indexes, where i<j /\ j<=path_nodes_count) ( path_array[i] != path_array[j] );
} in path_array;

And here, one of my tries of adapting the code above:

predicate exists_path(array[int,int] of int: graph, int: source, int: target)::promise_total =
let {
    set of int: V = index_set_1of2(graph);
    int: order = card(V);
    set of int: indexes = 1..order;
    array[indexes] of var (V union {-1}): path_array;

    constraint assert(index_set_1of2(graph) = index_set_2of2(graph), "The adjacency matrix is not square", true);
    constraint assert({source, target} subset V, "Source and target must be vertexes", true);
}
in
exists(path_nodes_count in indexes) (
    path_array[1] == source /\
    path_array[path_nodes_count] == target /\
    forall(i in 2..path_nodes_count) ( graph[ path_array[i-1], path_array[i] ] != 0 ) /\
    forall(i,j in indexes, where i<j /\ j<=path_nodes_count) ( path_array[i] != path_array[j] )
);

I'm testing the constraints using the following model:

int: N;
array[1..N, 1..N] of 0..1: adj_mat;
array[1..N] of var int: path;

% These should work:
constraint exists_path(adj_mat, 1, 3) = true;
constraint exists_path(adj_mat, 4, 1) = false;

% These should raise =====UNSATISFIABLE=====
constraint exists_path(adj_mat, 1, 3) = false;
constraint exists_path(adj_mat, 4, 1) = true;

solve satisfy;

% If you want to check the working constraint:
% constraint path = path(adj_mat, 1, 3);
% constraint path = path(adj_mat, 4, 1); <- This finds out that the model is unsatisfiable
% output[show(path)];

And here, some example data:

/* 1 -> 2 -> 3 -> 4 */

N=4;
adj_mat = [|
    0, 1, 0, 0,|
    0, 0, 1, 0,|
    0, 0, 0, 1,|
    0, 0, 0, 0 |];

%---------------------------------*/

/* Disconnected graph

1---2---6     4
 \ /          |
  3           5   */

N=6;
adj_mat = [|
    0, 1, 1, 0, 0, 0, |
    1, 0, 1, 0, 0, 1, |
    1, 1, 0, 0, 0, 0, |
    0, 0, 0, 0, 1, 0, |
    0, 0, 0, 1, 0, 0, |
    0, 1, 0, 0, 0, 0  |];

%---------------------------------*/

Thanks!

Answer 1

Here is what I do:

include "globals.mzn";
int: N;
array[1..N, 1..N] of 0..1: adj_mat;
array[1..N] of var 0..N: path;
solve satisfy;
constraint exists_path(1,3);

N=4;  
adj_mat = [|
    0, 1, 0, 0,|
    0, 0, 1, 0,|
    0, 0, 0, 1,|
    0, 0, 0, 0 |];

constraint alldifferent_except_0(path);
predicate exists_path_length(int: s, int: t, int: len) = 
          path[1]=s /\ path[len]=t /\ forall(i in len+1..N)(path[i]=0) /\          
          forall(i in 1..len-1)( adj_mat[path[i],path[i+1]]=1);
predicate exists_path(int: s, int: t) = exists(len in 2..N)(exists_path_length(s,t,len));

Note: (1) it's important to restrict the path's domains (in my code I set it to 0..N), otherwise MiniZinc can run forever due to huge number of decision choices. (2) Ideally, the global constraint alldifferent_except_0 should be put inside exists_path_length but it is done like this to avoid the problem of reification (check out Coursera courses on MiniZinc for more info).