Minizinc: generate a valid shift

问题:

Hope someone can help me with this!

The original problem is to generate valid shifts like explained below:

I have arrays like this [m,m,m,o,o,l,l,m,m,m,l,m,m,m] with a fixed length (S) where m is work, o is office and l free. What I need to make sure is that at least every 6m I have two l together (ll). The o does not count as work or as free. Examples:

mmlmmlmmmll is not valid (7 ms without two ls)
mmlmmlmmll is valid
mmomomommll is valid

What I was trying is to create an array with 0 (for ls) and 1 (for ms) but removing from the array all the o and the non consecutive ls. So, for the above examples would be:

mmlmmlmmmll -> 111111100
mmlmmlmmll -> 11111100
mmomomommll -> 11111100

This way I could use a sliding_sum or at_least constraint to solve it. However, I cannot manage to create this new array as it would have a different size than the original (S). A valid option is to pad at the end with 0 the remaining slots until S.

Any help is appreciated

Edit. This is the code so far:

enum TypeOfShift = {l,m,o};
enum Staff = {John, Mike, Mary};
array[Staff, 1..30] of TypeOfShift: Roster=[|
m,  m,  m,  l,  l,  o,  m,  m,  m,  m,  l,  l,  l,  m,  m,  m,  m,  m,  m,  l,  l,  m,  m,  m,  m,  m,  l,  l,  l,  l|
l,  l,  l,  l,  l,  m,  m,  m,  o,  o,  l,  l,  l,  m,  m,  m,  m,  m,  l,  l,  l,  m,  m,  m,  m,  m,  l,  l,  m,  m|
m,  m,  l,  l,  m,  o,  m,  m,  m,  m,  l,  l,  l,  m,  m,  m,  m,  m,  m,  m,  m,  m,  m,  m,  m,  m,  l,  l,  l,  m|];
array[Staff, 1..30] of var 0..2: RosterCalculated = array2d(Staff, 1..30,[if (Roster[i,d]==l) then 0 else (if (Roster[i,d]==o) then 2 else 1 endif) endif | i in Staff, d in 1..30]);
output[if (d==1) then "\n\(i) " ++ " " ++ show(RosterCalculated[i,d]) ++ " " else show(RosterCalculated[i,d]) ++ " " endif | i in Staff, d in 1..30];

回答1:

This answer provides a simple & effective solution for the problem stated in the question, that is, how to determine if a given shift is valid or not. [Note that in this case it is not necessary (actually, it is counterproductive) to declare the content of any array as var $T].

---

One option is to:

• determine the starting position of all ll in the array (array double_l_pos)
• determine the position of each o in the array (array has_o)
• determine the cumulative number of o in the array from the beginning (array cum_has_o)
• fix the position of all ll so that it ignores any o preceding it (array fixed_double_l_pos)
• determine the distance between all ll starting positions (array double_l_distance)
• require that no distance value is larger than 6

Example:

include "globals.mzn";

enum TypeOfShift = {l,m,o};
enum Staff = {John, Mike, Mary};

array[Staff, 1..30] of TypeOfShift: Roster=[|
    m,  m,  m,  l,  l, o,  m,  m,  m,  m,  l,  l,  l,  m,  m,  m,  m,  m,  m,  l,  l,  m,  m,  m,  m,  m,  l,  l,  l,  l|
    l,  l,  l,  l,  l,  m,  m,  m,  o,  o,  l,  l,  l,  m,  m,  m,  m,  m,  l,  l,  l,  m,  m,  m,  m,  m,  l,  l,  m,  m|
    m,  m,  l,  l,  m,  o,  m,  m,  m,  m,  l,  l,  l,  m,  m,  m,  m,  m,  m,  m,  m,  m,  m,  m,  m,  m,  l,  l,  l,  m|];

constraint forall (s in Staff)
(
    let {
        array[int] of TypeOfShift: shifts = [Roster[s, i] | i in 1..30];
        array[int] of int: double_l_pos = [ i - 1 | i in index_set(shifts) where
                                                    i > 1 /\
                                                    shifts[i-1] == l /\
                                                    shifts[i] == l];
        array[int] of int: has_o = [ if el == o then 1 else 0 endif | el in shifts ];
        array[int] of int: cum_has_o = [
                              sum ( j in index_set(shifts) where j <= i) ( has_o[j] )
                              | i in index_set(has_o) ];
        array[int] of int: fixed_double_l_pos = [ pos - cum_has_o[pos] | pos in double_l_pos ];
        array[int] of int: double_l_distance = [fixed_double_l_pos[1]] ++
            [fixed_double_l_pos[i] - fixed_double_l_pos[i-1] - 1 - 1
            | i in index_set(fixed_double_l_pos) where i > 1];
    } in
        forall(dist in double_l_distance) (
            dist <= 6
        )
);

solve satisfy;

Everything here is statically computed, so the model inconsistency can be detected even before the actual solving is started.

---

Addendum: since this is a roster problem, you may want to read in detail the roster and the on-call-rostering models in the MiniZinc benchmarks repository. Those files may contain better approaches for dealing with your problem.

回答2:

This new answer deals with the more general problem of generating a valid schedule. In this case we are dealing with decision variables so the other approach cannot be easily implemented.

My suggestion is to use the regular global constraint to deal with counting the number of m and l. This ensures that the provided solution does not place more than 6 sub-sequent m (ignoring o and single l) in a sequence.

Example:

include "globals.mzn";

enum TypeOfShift = {l,m,o};

% sat:
%array[1..30] of var TypeOfShift: shift = [m,  m,  m,  l,  l,  o,  m,  m,  m,  m,  l,  l,  l,  m,  m,  m,  m,  m,  m,  l,  l,  m,  m,  m,  m,  m,  l,  l,  l,  l];

% sat:
%array[1..30] of var TypeOfShift: shift = [l,  l,  l,  l,  l,  m,  m,  m,  o,  o,  l,  l,  l,  m,  m,  m,  m,  m,  l,  l,  l,  m,  m,  m,  m,  m,  l,  l,  m,  m];

% unsat: too many m
% array[1..30] of var TypeOfShift: shift = [m,  m,  l,  l,  m,  o,  m,  m,  m,  m,  l,  l,  l,  m,  m,  m,  m,  m,  m,  m,  m,  m,  m,  m,  m,  m,  l,  l,  l,  m];

% unsat: o breaks double l
% array[1..30] of var TypeOfShift: shift = [l,  l,  l,  l,  l,  m,  m,  m,  o,  o,  l,  l,  l,  m,  m,  m,  m,  m,  l,  o,  l,  m,  m,  m,  m,  m,  l,  l,  m,  m];

% free assignment
% [NOTE: this will give a trivial answer because of missing constraints]
array[1..30] of var TypeOfShift: shift;

%          |   1     2     3   <= Input Values
%          |   m     o     l
% ---------------------------- 
%  1 m0_l0 | m1_l0 m0_l0 m0_l1
%  2 m1_l0 | m2_l0 m1_l0 m1_l1
%  3 m2_l0 | m3_l0 m2_l0 m2_l1
%  4 m3_l0 | m4_l0 m3_l0 m3_l1
%  5 m4_l0 | m5_l0 m4_l0 m4_l1
%  6 m5_l0 | m6_l0 m5_l0 m5_l1
%  7 m6_l0 |   -   m6_l0 m6_l1
%  8 m0_l1 | m1_l0 m0_l0 m0_l0
%  9 m1_l1 | m2_l0 m1_l0 m0_l0
% 10 m2_l1 | m3_l0 m2_l0 m0_l0
% 11 m3_l1 | m4_l0 m3_l0 m0_l0
% 12 m4_l1 | m5_l0 m4_l0 m0_l0
% 13 m5_l1 | m6_l0 m5_l0 m0_l0
% 14 m6_l1 |   -   m6_l0 m0_l0
% ^
% states
array[1..14, 1..3] of 0..14: transition_relation =
    [|  2,  1,  8,  % m0_l0
     |  3,  2,  9,  % m1_l0
     |  4,  3, 10,  % m2_l0
     |  5,  4, 11,  % m3_l0
     |  6,  5, 12,  % m4_l0
     |  7,  6, 13,  % m5_l0
     |  0,  7, 14,  % m6_l0
     |  2,  1,  1,  % m0_l1
     |  3,  2,  1,  % m0_l2
     |  4,  3,  1,  % m0_l3
     |  5,  4,  1,  % m0_l4
     |  6,  5,  1,  % m0_l5
     |  7,  6,  1,  % m0_l6
     |  0,  7,  1,  % m0_l7
    |];

constraint regular(
    [ if s == m then 1 else
      if s == o then 2 else
                     3 endif
                       endif
      | s in shift],                % sequence of input values
    14,                             % number of states
    card(TypeOfShift),              % number of different input values of state machine
    transition_relation,            % transition relation
    1,                              % initial state
    1..14,                          % final states
 );

solve satisfy;

Important Notes:

• this can also be used to verify existing solutions;

• one should place the regular constraint within a predicate, so that it can be easily applied to all members of the Staff without code duplication;

• MiniZinc prints a trivial answer for this model only because there is no other constraint on the shifts array (i.e. the minimum number of m required in a month).