预先计算 MiniZinc 中关系的传递闭包：Y/N?

Question

我正在尝试解决 MiniZinc 中的一个练习，其中偏序关系由二维数组给出：

enum NODE = { A, B, C, D, E };

int : SOURCE = 1;
int : TARGET = 2;

array[int,1..2] of NODE: edge =
   [| A, B        % edge 1, source & edge 1, target
    | A, E        % edge 2, source & edge 2, target
    | B, C        % edge 3, source & edge 3, target
    | B, D |];    % edge 4, source & edge 4, target
  
set of int: EDGES = index_set_1of2(edge);  

output ["EDGES is \(EDGES)\n"];

predicate ancestor_descendant(NODE: a, NODE: d) =
   exists(edge_num in EDGES)(edge[edge_num,SOURCE]=a /\ edge[edge_num,TARGET]=d)
   \/
   exists(edge_num in EDGES)(
      exists(m in NODE)(
         edge[edge_num,SOURCE]=a 
         /\
         edge[edge_num,TARGET]=m
         /\
         ancestor_descendant(m,d)));
   
constraint assert(fix(ancestor_descendant(A,B)),"Failed a->b");
constraint assert(fix(ancestor_descendant(A,E)),"Failed a->e");
constraint assert(fix(ancestor_descendant(B,C)),"Failed b->c");
constraint assert(fix(ancestor_descendant(B,D)),"Failed b->d");
constraint assert(fix(ancestor_descendant(A,C)),"Failed a->c"); % transitive
constraint assert(fix(ancestor_descendant(A,D)),"Failed a->d"); % transitive
constraint assert(not(fix(ancestor_descendant(E,D))),"Failed a->d"); 
constraint assert(not(fix(ancestor_descendant(A,A))),"Failed a->a");

上面只是实现了下面的树和一个判断节点是否存在的谓词 a 是节点 d 的祖先。

但是，我觉得回答谓词 ancestor_descendant/2 对于大型 edge 数组来说可能会变得很昂贵，如果在优化过程中经常调用谓词，这可能会成为一个障碍。

我是否应该期望 MiniZinc memoize/cache（不可变的）谓词结果本身？我应该自己这样做吗？尽管我看不出如何避免设置 true 和 false 的 (card(NODE)^2)*2 大小的数组（不像在 Prolog 中，我只保留数据库中的谓词）。

Answer 1

MiniZinc 确实以 Common Sub-expression Elimintation (CSE) 的形式为模型中的任何决策变量表达式实现了记忆化。这应该确保任何两个节点的调用结果和存在结果只存在一次。

总的来说，已经发现通过记忆的 CSE 对于参数表达式来说不值得，因为它在内存中是昂贵的并且参数表达式在 MiniZinc 中通常很快。因此，如果您运行在扁平化阶段遇到问题，那么我建议您事先明确计算后代。

Answer 2

树形拓扑是一个典型的示例，您不一定需要缓存。

而是一个好的程序转换可以完成这项工作，分别来自
的定理传递闭包，即左右传递闭包相同。

我正在使用 edge/2 和 edge2/2，因此测试也有效
对于只有第一个参数索引的 Prolog 系统：

setup :- between(1,1024,N), M is N//2, assertz(edge(M,N)), fail.
setup :- edge(M,N), assertz(edge2(N,M)), fail.
setup.

anc(X,Y) :- edge(X, Y).
anc(X,Y) :- edge(X, Z), anc(Z, Y).

anc2(X,Y) :- edge2(Y, X).
anc2(X,Y) :- edge2(Y, Z), anc2(X, Z).

您可以运行 setup 一次。稍后你会得到非常戏剧性的结果：

?- time((between(1,1000,_), anc(0,1024), fail; true)).
% 3,076,001 inferences, 0.178 CPU in 0.181 seconds (98% CPU, 17298884 Lips)
true.

?- time((between(1,1000,_), anc2(0,1024), fail; true)).
% 37,001 inferences, 0.003 CPU in 0.003 seconds (99% CPU, 14659667 Lips)
true.

所以反复调用新鲜anc2/2应该没问题。对于具有 n 个节点的平衡二叉树，它只需要 O(log(n)) 时间，不像 anc/2 需要 O(n) 时间。

预先计算 MiniZinc 中关系的传递闭包：Y/N?

Precompute transitive closure of a relation in MiniZinc: Y/N?

transitive-closure

minizinc