使用MiniZinc检查图中是否有连接两个顶点的路径

Question

我试图做出约束，以检查图中是否存在从顶点A到顶点B的路径。我已经做了一个约束，返回了路径本身，但是我还需要一个函数，该函数返回一个布尔值，指示路径是否存在。

我已经花了很多时间，但是我的尝试都没有成功...

有谁知道我该怎么办？

这是我制作的返回路径本身的函数，其中graph是一个邻接矩阵，source和target是顶点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;

在这里，我尝试修改上面的代码之一：

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

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

谢谢！

Answer 1

这是我所做的：

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

注意：（1）限制路径的域很重要（在我的代码中我将其设置为 0..N），否则 MiniZinc 可能会由于大量的决策选择而永远运行。(2) 理想情况下，全局约束all different_ except_0应该放在contains_path_length内，但这样做是为了避免具体化问题（查看 MiniZinc 上的 Coursera 课程了解更多信息）。