Minizinc: how can I make the union of a set in this situation (fix point algorithm?)

Question

I have an array of sets that means that the items inside the set must finish before the actual one starts. For example:

before = [ {},
      {1},
      {},
      {},
      {2}];

I'm looking to make each line include the ones who go before recursively. So in this case, it should end up like this:

abans = [ {},
      {1},
      {},
      {},
      {1,2}];

I've tried generating a variable and creating the sets from blank, but I didn't manage to do it. Any ideas how I could do this?

Answer 1

CASE 1: before is a variable.

Let's take the following list of tasks:

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

We declare an array before to hold the set of blocking tasks for each task:

array [TASKS] of var set of TASKS: before;

A task should never block on itself:

constraint forall(i in index_set(before))
    (
        not (i in before[i])
    );

A task i inherits the block-set of each task j blocking task i:

constraint forall(taskset in before)
    (
        forall(task in taskset)
        (
            before[task] subset taskset
        )
    );

You can append:

 solve satisfy;

And find all possible solutions:

~$ minizinc test.mzn --all-solutions
before = array1d(TASKS, [{}, {A}, {A, B}, {A, B, C}, {A, B, C, D}]);
----------
before = array1d(TASKS, [{B}, {}, {A, B}, {A, B, C}, {A, B, C, D}]);
----------
before = array1d(TASKS, [{}, {}, {A, B}, {A, B, C}, {A, B, C, D}]);
----------
before = array1d(TASKS, [{}, {A, C}, {A}, {A, B, C}, {A, B, C, D}]);
----------
before = array1d(TASKS, [{}, {A}, {A}, {A, B, C}, {A, B, C, D}]);
----------
before = array1d(TASKS, [{}, {}, {A}, {A, B, C}, {A, B, C, D}]);
----------
before = array1d(TASKS, [{B, C}, {}, {B}, {A, B, C}, {A, B, C, D}]);
----------
before = array1d(TASKS, [{B}, {}, {B}, {A, B, C}, {A, B, C, D}]);
----------
before = array1d(TASKS, [{}, {}, {B}, {A, B, C}, {A, B, C, D}]);
----------
before = array1d(TASKS, [{C}, {A, C}, {}, {A, B, C}, {A, B, C, D}]);
----------
before = array1d(TASKS, [{}, {A, C}, {}, {A, B, C}, {A, B, C, D}]);
----------
before = array1d(TASKS, [{}, {A}, {}, {A, B, C}, {A, B, C, D}]);
...

---

CASE 2: before is an input parameter.

A task i belongs to abans[j] if it is contained in before[j], or there exists a task k in abans[j] such that i is in before[j].

Encoding:

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

array [TASKS] of set of TASKS: before = 
    [{C}, {A}, {D}, {}, {B}];

array [TASKS] of var set of TASKS: abans;

constraint forall(i, j in TASKS)
    (
        i in abans[j] <->
        (
            i in before[j]
            \/
            exists(k in abans[j])
            (
                i in before[k]
            )
        )
        % circular dependencies are not allowed!
        /\ not(j in abans[j])
    );

solve satisfy;

Output:

~$ minizinc test.mzn --all-solutions
abans = array1d(TASKS, [{C, D}, {A, C, D}, {D}, {}, {A, B, C, D}]);
----------
==========