graph - MiniZincを使用して、グラフの2つの頂点を結ぶパスがあるかどうかを確認します

Question

グラフに頂点Aから頂点Bへのパスがあるかどうかを確認する制約を作成しようとしています。パス自体を返す制約を既に作成しましたが、パスが存在するかどうかを示すboolを返す関数も必要です。

私はすでにそれに多くの時間を費やしましたが、私の試みはどれも成功しませんでした...

誰かが私に何ができるか考えていますか?

パス自体を返す関数を次に示します。ここで、グラフは隣接行列であり、ソースとターゲットは頂点Aと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;

そして、ここで、上記のコードを適応させる私の試みの1つ:

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] )
);

次のモデルを使用して制約をテストしています。

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)];

そしてここに、いくつかのサンプルデータがあります:

/* 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  |];

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

ありがとう！