如何在MiniZinc中构建有向图的连通性矩阵（传递闭包）

问题分析 #

你最初的约束仅规定了传递性和包含直接边，但缺少最小性约束，导致全true的矩阵也能满足条件。使用dpath时出现错误，是因为MiniZinc不支持将dpath作为reified约束直接赋值给变量。

下面提供两种可行的解决方案：

方案一：补充最小性约束（基于原始传递性约束扩展） #

这种方法在你原有代码基础上，添加约束确保VariantIsUpwardOf是满足条件的最小集合，不会出现多余的true值。

% 自定义节点枚举
enum Variants = {N1,N2,N3};

% 已知的直接边矩阵
array[Variants, Variants] of bool : VariantIsDirectlyUpwardOf = [
    | false, true, false  % N1 -> N2
    | false, false, true  % N2 -> N3
    | false, false, false
];

% 要构建的传递闭包矩阵
array[Variants, Variants] of var bool : VariantIsUpwardOf;

% 约束1：所有直接边必须包含在闭包中
constraint forall(v1 in Variants, v2 in Variants)(
    VariantIsDirectlyUpwardOf[v1,v2] -> VariantIsUpwardOf[v1,v2]
);

% 约束2：传递性
constraint forall(v1 in Variants, v2 in Variants, v3 in Variants)(
    VariantIsUpwardOf[v1,v2] /\ VariantIsUpwardOf[v2,v3] -> VariantIsUpwardOf[v1,v3]
);

% 约束3：最小性（关键！避免多余的true）
% 闭包中的边要么是直接边，要么可通过某个中间节点的直接边扩展得到
constraint forall(v1 in Variants, v2 in Variants)(
    VariantIsUpwardOf[v1,v2] -> (
        VariantIsDirectlyUpwardOf[v1,v2] 
        \/ exists(k in Variants)(VariantIsUpwardOf[v1,k] /\ VariantIsDirectlyUpwardOf[k,v2])
    )
);

% 可选：如果需要包含自环（v到v的路径长度为0），添加以下约束
constraint forall(v in Variants)(VariantIsUpwardOf[v,v] = true);

output [show(VariantIsUpwardOf)];

方案二：使用路径约束直接关联闭包值 #

通过提取直接边为列表，利用dpath谓词（非reified形式）直接定义闭包矩阵的每个值，同时避免reified约束的错误。

include "path.mzn";

% 自定义节点枚举
enum Variants = {N1,N2,N3};

% 已知的直接边矩阵
array[Variants, Variants] of bool : VariantIsDirectlyUpwardOf = [
    | false, true, false
    | false, false, true
    | false, false, false
];

% 提取所有直接边到EdgeFrom和EdgeTo数组
array[int] of Variants: EdgeFrom = [v1 | v1 in Variants, v2 in Variants where VariantIsDirectlyUpwardOf[v1,v2]];
array[int] of Variants: EdgeTo = [v2 | v1 in Variants, v2 in Variants where VariantIsDirectlyUpwardOf[v1,v2]];

% 要构建的传递闭包矩阵
array[Variants, Variants] of var bool : VariantIsUpwardOf;

% 对每个节点对，闭包值等于是否存在路径
constraint forall(v1 in Variants, v2 in Variants)(
    if VariantIsUpwardOf[v1,v2] then
        dpath(EdgeFrom, EdgeTo, v1, v2, [true | _ in Variants], [true | _ in EdgeFrom])
    else
        not dpath(EdgeFrom, EdgeTo, v1, v2, [true | _ in Variants], [true | _ in EdgeFrom])
    endif
);

% 可选：自环约束
constraint forall(v in Variants)(VariantIsUpwardOf[v,v] = true);

output [show(VariantIsUpwardOf)];

注意事项 #

• 若你的MiniZinc版本仍不支持上述dpath的条件用法，可以改用path库中的reachable谓词（如果可用），或手动实现基于广度优先搜索的存在性约束。
• 若VariantIsDirectlyUpwardOf是常量数组而非变量，也可以预先用Floyd-Warshall算法计算传递闭包（在MiniZinc外或用初始化逻辑），无需动态约束。

内容的提问来源于stack exchange，提问作者Iver Bailly-Salins