minizinc logic to ortools CP

I created a model in minizinc that I am translating to ortools CP (sat). My main variable is

q_shifts[starts_at][length]

which is an array of 2D, first is starts_at and 2nd is length, thus is the quantity of shifts with a certain start_at and certain length. Start at and length are fixed, the variable is the quantity used of those.

q_shift[1, 3] = 2, means there are 2 shifts that start at time 1 with length 3.

So, in order to avoid symmetries, I want that all consecutive shifts are sorted by length. A consecutive shift of for instance one that start at 1, with length 3, is one that starts at 4. So what I want is that the length of the consecutive one is <= than the length of the first one.

    % pseudocode
    if q_shifts[1,3] > 0 and q_shift[4, l2] > 0 then l2 <= 3.

Now, be aware that l2 is not a variable, the variable is q_shift. This is just a problem formulation that you can do in Minizinc:

% minizinc 
% consecutives shifts should have len sorted
constraint forall(t in 1.. times-1)(
    forall(l1, l2 in LENGTH)(
        if q_shifts[t, l1] > 0 /\ q_shifts[t+l1, l2] > 0 then l1 >= l2 endif )
        );

When I want to apply the same in ortools, I thought I could be using something like:

    for t in range(min(times), max(times)):
         lens_t = q_shifts[t].keys()
         for l1, l2 in product(lens_t, lens_t):
             if (t+l1 + l2 -1 <= max(times)):
                 model.Add(l1 >= l2).OnlyEnforceIf(
                          q_shifts[t][l1] > 0, q_shifts[t+l1][l2] > 0)

But this does not work since l1 and l2 are not variables, right?

In other words, it cannot exist q_shift with positive values for 2 consecutive shifts, having length of 2nd shift > length of 1st shift.

    % pseudocode
        if q_shifts[1,3] > 0 and l2 in q_shift[4, l2] and l2 > 3 
           then q_shift[4, l2] = 0.

So I managed to do:

for t in range(min(times), max(times)):
    lens_t = q_shifts[t].keys()
    for l1, l2 in product(lens_t, lens_t):
        if (t + l1 + l2 - 1 <= max(times)) and (l1 < l2):
            has_shifts_t_l1 = model.NewBoolVar("has_shifts_t1_l1")
            model.Add(q_shifts[t][l1] >= 0).OnlyEnforceIf(has_shifts_t_l1)
            model.Add(q_shifts[t][l1] == 0).OnlyEnforceIf(has_shifts_t_l1.Not())

            has_shifts_t2_l2 = model.NewBoolVar("has_shifts_t2_l2")
            model.Add(q_shifts[t + l1][l2] >= 0).OnlyEnforceIf(has_shifts_t2_l2)
            model.Add(q_shifts[t + l1][l2] == 0).OnlyEnforceIf(
                        has_shifts_t2_l2.Not()
                    )

            model.AddBoolOr(has_shifts_t_l1.Not(), has_shifts_t2_l2.Not())

which I find terribly verbose. Is there any better solution?

Thanks.

Solution

Yes, CP-SAT supports such relationships between variables via “channeling”:
https://github.com/google/or-tools/blob/stable/ortools/sat/docs/channeling.md
Not sure I understand you correctly.
To sort inside the CP-SAT model, we can do this:
(pseudo code)

for i in LENGTH-1:
    model.add(q_shifts[t][i] <= q_shifts[t][i+1])

Edit:

IIRC, minizinc supports ortools as one of the solver options, so basically it is not necessary to translate the minizinc code to run it with ortools
see, e.g., here:
Efficiency of MiniZinc + CP-SAT (from OR-Tools) compared to CP-SAT alone

Edit 2:

Thanks for the update. It’s more clear to me now.

# this “line”:
model.Add(l1 >= l2) \
    .OnlyEnforceIf(q_shifts[t][l1] > 0, q_shifts[t+l1][l2] > 0) 

# … should look like this:
model.Add(l1 >= l2) \
    .OnlyEnforceIf(has_shifts_t_l1, has_shifts_t2_l2)

# with the “channeling” you already did:
has_shifts_t_l1 = model.NewBoolVar("has_shifts_t1_l1")
model.Add(q_shifts[t][l1] >= 0) \
    .OnlyEnforceIf(has_shifts_t_l1)
model.Add(q_shifts[t][l1] == 0) \
    .OnlyEnforceIf(has_shifts_t_l1.Not())

has_shifts_t2_l2 = model.NewBoolVar("has_shifts_t2_l2")
model.Add(q_shifts[t + l1][l2] >= 0) \
    .OnlyEnforceIf(has_shifts_t2_l2)
model.Add(q_shifts[t + l1][l2] == 0) \
    .OnlyEnforceIf(has_shifts_t2_l2.Not())

model.Add(l1 >= l2).OnlyEnforceIf(has_shifts_t_l1, has_shifts_t2_l2)

is half-reified and covers only the case both auxiliary bools are TRUE.
… it’s not shorter than your current solution, but “matches” with yours, as we see in its alternative (pseudo-code) formulation: model.AddBoolOr(has_shifts_t_l1.Not(), has_shifts_t2_l2.Not(), l1 >= l2)