Search code examples
minizinctransitive-closure

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

I am trying to solve an exercise in MiniZinc in which a partial ordering relation is given by a 2-D array:

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

The above just implements the following tree and a predicate that asks whether node a is ancestor of node d.

Tree

However, I feel answering the predicate ancestor_descendant/2 can become expensive for large edge arrays, which might be a hindrance if the predicate is called a lot during optimization.

Should I expect MiniZinc to memoize/cache the (immutable) predicate results by itself? Should I do so myself? Although I don't see how to avoid setting up an (card(NODE)^2)*2 sized array of true and false (unlike in Prolog where I would just keep the positive answers of the predicate in the database).

Solution

  • MiniZinc does indeed implement memoization for any decision variable expression in the model, as a form of Common Sub-expression Elimintation (CSE). This should make sure that the result of the calls and the results of the exists for any two nodes will only exists once.

    In general, it has been found that CSE through memoization is not worth it for parameter expressions, since it is costly in memory and parameter expressions are generally quick in MiniZinc. So if you are running into problems during the flattening stage, then I would suggest computing the descendants explicitly beforehand.