Minizinc. Count number of shifts in a cycle

Question

Continuing with the other post ( Minizinc: generate a valid shift ). I am trying to have a maximum of 2 im between double ls. Doing this with a regular constraint is quite hard as the transition table would be quite big (too many paths). Is there any way to solve it? I have tried this, but it is giving me errors:

include "globals.mzn";

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

%array[1..30] of TypeOfShift: Roster=[m,  m,  m,  l,  l, o,  im,  m,  m,  m,  l,  l,  l,  im,  m,  m,  m,  m,  im,  l,  l,  m,  m,  m,  m,  m,  l,  l,  l,  l];
array[Staff,1..30] of var TypeOfShift: Roster;
array[Staff, 1..30] of var 1..4: RosterForIm = array2d(Staff, 1..30,[if (Roster[i,d]==l) then 1 
      else (if (Roster[i,d]==o) then 2 else (if (Roster[i,d]==im) then 3 else 4 endif) endif) endif| i in Staff, d in 1..30]);


predicate TwoOsPerCycle(array[int] of int: shifts) = 
   let {
        array[int] of var opt int: double_l_pos = [ i - 1 | i in index_set(shifts) where
                                                    i > 1 /\
                                                    shifts[i-1] == l /\
                                                    shifts[i] == l];

        array[int] of var opt int: double_l_distance = [double_l_pos[1]] ++
            [double_l_pos[i] - double_l_pos[i-1] - 1 - 1
            | i in index_set(double_l_pos) where i > 1];
    } in
  (forall(j in double_l_pos) 
    (at_most(2,[shifts[ciclo] | ciclo in j..j+1],3))); %3 code for im, 2 number of max permited in a cycle

constraint forall(i in Staff) (TwoOsPerCycle([RosterForIm[i,j] | j in 1..30]));

solve satisfy;

Hi Patrick ... I'm stuck again... I continued developing the regular expression but I went up to 55 states... then I stopped. I was trying a different approach which is to build up an array of resting hours between consecutive working days. For example: mmmtnllmmlttlnnlllm (m1 eary morning 6 to 13; m morning start at 7 to 14; t evening 14 to 21; night 22 to 7am; l resting day; o office 10 to 14; im on call morning 6 to 14; it on call evening 13 to 22; ino on call night 21 to 7) should create an array like 17,17,24,24,48,48,17,48,48,16... which is StartTime of shift [day+1] - (StartTime of shift [day] + Duration of shift[day]). This is coded. Between consecutive working shifts has to be 12 hours or more.

When there is a resting day (l) I intend to repit the last resting period (48,48 in the example). This I don´t know how to do it. The idea then is to count the working days in between cycles to check the following: - At least 12 hours between consecutive working shifts - Cycle before a 48h or more rest has a maximum of 5 working days. - Cycle before a 54h rest or more has a maximum of 6 working days.

The restrictions of the nights (48h after a night except if it is another night o rest day, 54h after two nights) I have done it with constraints or I can do it with regular expressions... that's fine

Any ideas?

include "globals.mzn";


%Definitions
enum TypeOfShift = {l,m1,m,t,n,im,it,ino,o};  %Types of shifts
array[TypeOfShift] of float: StartTypeOfShift=[10, 6, 7, 14, 22, 5, 13, 21, 10]; %Starting hour
array[TypeOfShift] of float: DurationTypeOfShift=[1, 7, 7, 7, 9, 8, 8, 10, 4]; %Duration of shifts (hours)


enum Staff={AA,BB,CC,DD,EE,FF,GG,HH,II,JJ,KK,LL,MM,NN,OO,PP,QQ,RR,SS,TT,UU,VV};
int: NumberWorkers = card(Staff); 
array[int] of int: DaysInRoster=[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15];

array[1..NumDaysInRoster,TypeOfShift] of int: Configuration = array2d(1..NumDaysInRoster,TypeOfShift,[1 |  d in 1..NumDaysInRoster, shift in TypeOfShift ]);

int: NumDaysInRoster=length(DaysInRoster); 


% Variables
array[Staff, 1..NumDaysInRoster] of var TypeOfShift: RosterCalculated;
array[Staff, 1..NumDaysInRoster-1] of var float: RosterCalculatedRests = array2d(Staff, 1..NumDaysInRoster-1,[(24*(d)+StartTypeOfShift[RosterCalculated[i,d+1]]) - (24*(d-1)+StartTypeOfShift[RosterCalculated[i,d]] + DurationTypeOfShift[RosterCalculated[i,d]]) | i in Staff, d in 1..NumDaysInRoster-1]);


% Satisfy configuration
constraint forall(d in 1..NumDaysInRoster) 
              (((sum(i in Staff) (RosterCalculated[i,d] == m)) == Configuration[d,m]) /\ ((sum(i in Staff) (RosterCalculated[i,d] == m1)) == Configuration[d,m1]) /\ 
              ((sum(i in Staff) (RosterCalculated[i,d] == t)) == Configuration[d,t]) /\  ((sum(i in Staff) (RosterCalculated[i,d] == n)) == Configuration[d,n]));


% Time between two shifts >= 12h
constraint forall(i in Staff, d in 1..NumDaysInRoster-1)
              ((RosterCalculated[i,d+1] != l ) -> (24*(d-1)+StartTypeOfShift[RosterCalculated[i,d]] + DurationTypeOfShift[RosterCalculated[i,d]] + 12 <= 24*d+StartTypeOfShift[RosterCalculated[i,d+1]]));


% Rest after night or on call night (could be changed by regular constraint) 48h or more 
constraint forall(i in Staff, d in 1..NumDaysInRoster-3)
              (((RosterCalculated[i,d] == n) \/ (RosterCalculated[i,d] == ino)) -> ((RosterCalculated[i,d+1]==l \/ RosterCalculated[i,d+1]==n \/ RosterCalculated[i,d+1]==ino) /\
              (RosterCalculated[i,d+2]==l \/ RosterCalculated[i,d+2]==n \/ RosterCalculated[i,d+2]==ino) /\
              (StartTypeOfShift[RosterCalculated[i,d+3]] >= 7.5 \/ RosterCalculated[i,d+3]==l)));  


% Rest after double night has to be 54h or more (could be changed by regular constraint)
constraint forall(i in Staff, d in 1..NumDaysInRoster-4)
              ((((RosterCalculated[i,d] == n) \/ (RosterCalculated[i,d] == ino)) /\ ((RosterCalculated[i,d+1] == n) \/ (RosterCalculated[i,d+1] == ino))) -> ((RosterCalculated[i,d+2]==l) /\
              (RosterCalculated[i,d+3]==l) /\
              (StartTypeOfShift[RosterCalculated[i,d+4]] >= 13.5 \/ RosterCalculated[i,d+4]==l)));  

% Rest after a night free night has to be 54h or more (could be changed by regular constraint)
constraint forall(i in Staff, d in 1..NumDaysInRoster-5)
              ((((RosterCalculated[i,d] == n) \/ (RosterCalculated[i,d] == ino)) /\ (RosterCalculated[i,d+1] == l) /\ ((RosterCalculated[i,d+2] == n) \/ (RosterCalculated[i,d+2] == ino))) -> ((RosterCalculated[i,d+3]==l) /\
              (RosterCalculated[i,d+4]==l) /\
              (StartTypeOfShift[RosterCalculated[i,d+5]] >= 13.5 \/ RosterCalculated[i,d+5]==l)));


predicate Max6WorkingDays(array[int] of var TypeOfShift: shift) =
    let {
        array[1..35, 1..6] of 0..35: transition_relation =  % Complex matrix and not coping with all possibilities!! mlt has 48 hours rest; tln as well
           [|
1, 1, 2, 2, 7, 17
|13, 2, 3, 3, 8, 17
|14, 3, 4, 4, 9, 17
|15, 4, 5, 5, 10, 17
|16, 5, 6, 6, 11, 17
|24, 6, 0, 0, 12, 18
|13, 7, 0, 0, 8, 17
|14, 8, 0, 0, 9, 17
|15, 9, 0, 0, 10, 17
|16, 10, 0, 0, 11, 17
|35, 11, 0, 0, 12, 18
|23, 12, 0, 0, 0, 0
|1, 29, 25, 25, 8, 17
|1, 30, 26, 26, 9, 17
|1, 31, 27, 27, 10, 17
|1, 32, 28, 28, 11, 17
|21, 0, 0, 0, 0, 18
|19, 0, 0, 0, 0, 0
|20, 0, 0, 0, 0, 0
|1, 0, 0, 0, 7, 17
|22, 0, 0, 0, 0, 18
|1, 1, 2, 0, 7, 17
|1, 12, 0, 0, 0, 0
|1, 34, 0, 0, 12, 18
|14, 25, 26, 26, 9, 17
|15, 26, 27, 27, 10, 17
|16, 27, 28, 28, 11, 17
|35, 28, 33, 33, 12, 18
|13, 29, 25, 25, 8, 17
|14, 30, 26, 26, 9, 17
|15, 31, 27, 27, 10, 17
|16, 32, 28, 28, 11, 18
|23, 33, 0, 0, 0, 0
|24, 34, 0, 0, 12, 18
|1, 28, 33, 33, 12, 18|];
    } in
        regular(
            [ if (s == l) then 1 else
              if (s ==  o) then 2 else
              if (s == m) then 3 else
              if ((s == m1) \/ (s == im)) then 4 else
              if ((s == t) \/ (s == it)) then 5 else
                              6 endif %n, in
                                endif
                                endif
                                endif
                                endif
              | s in shift],                % sequence of input values
            35,                             % number of states
            6,                              % number of different input values of state machine
            transition_relation,            % transition relation
            1,                              % initial state
            1..35,                          % final states
         );         



constraint forall(i in Staff)
            (Max6WorkingDays([RosterCalculated[i,j] | j in 1..NumDaysInRoster]));                                                              


% Two on calls per cycle as max
/*predicate Max2OnCall(array[int] of var TypeOfShift: shift) =
    let {
        array[1..5, 1..4] of 0..5: transition_relation =
            [| 1, 2, 1, 1 % im0 (start)
             | 2, 4, 2, 3 % im1_l0
             | 2, 4, 2, 1 % im1_l1
             | 4, 0, 4, 5 % im2_l0
             | 4, 0, 4, 1 % im2_l1
            |];
    } in
        regular(
            [ if ((s == m1) \/ (s == m) \/ (s == t) \/ (s == n)) then 1 else
              if ((s == im) \/ (s == it) \/ (s == ino)) then 2 else
              if s ==  o then 3 else
                              4 endif
                                endif
                                endif
              | s in shift],                % sequence of input values
            5,                              % number of states
            4,                              % number of different input values of state machine
            transition_relation,            % transition relation
            1,                              % initial state
            1..5,                           % final states
         );

constraint forall(i in Staff)
            (Max2OnCall([RosterCalculated[i,j] | j in 1..NumDaysInRoster]));
*/
% Maximo de 5Ms seguidas . NO NECESARIOS CON MATRIZ V4 (MAS LENTO)
/*predicate MaxMsPerCycle(array[int] of var TypeOfShift: shift) =
    let {
        array[1..13, 1..4] of 0..13: transition_relation =
            [| 
              2,    7,  1,  1|
              3,    7,  8,  2|
              4,    7,  9,  3|
              5,    7,  10, 4|
              6,    7,  11, 5|
              0,    7,  12, 6|
              7,    7,  13, 7|
              3,    7,  1,  2|
              4,    7,  1,  3|
              5,    7,  1,  4|
              6,    7,  1,  5|
              0,    7,  1,  6|
              7,    7,  1,  7
            |];
    } in
        regular(
            [ if ((s == m1) \/ (s == m) \/ (s == im)) then 1 else
              if ((s == t) \/ (s == it) \/ (s == n) \/ (s == ino)) then 2 else
              if ((s ==  l)) then 3 else
                              4 endif
                                endif
                                endif
              | s in shift],                % sequence of input values
            13,                             % number of states
            4,                              % number of different input values of state machine
            transition_relation,            % transition relation
            1,                              % initial state
            1..13,                          % final states
         );

constraint forall(i in Staff)
            (MaxMsPerCycle([RosterCalculated[i,j] | j in 1..NumDaysInRoster]));
*/

solve satisfy;


output[if (d==1) then "\n\(i) " ++ " " ++ show(RosterCalculatedRests[i,d]) ++ " " else show(RosterCalculatedRests[i,d]) ++ " " endif | i in Staff, d in 1..NumDaysInRoster-1]++["\n"]; % Inamovibles



output[";;"]++["\(DaysInRoster[d]);" | d in 1..NumDaysInRoster];
output[if (d==1) then "\n"++"O3;\(i) " ++ ";" ++ show(RosterCalculated[i,d]) ++ ";" else show(RosterCalculated[i,d]) ++ ";" endif | i in Staff, d in 1..NumDaysInRoster]; % Roster calculado

Answer 1

It is actually still possible to use the regular global constraint for this task, since the DFA requires only 5 states:

Here, im0 is the initial state and all states are also final states:

• im0: no im since the last ll or since the start
• im1_l0: received one im
• im1_l1: received one l after an im; Here, we see if this l belongs to a resetting ll sequence or not.
• im2_l0: received two im, from now on im cannot be an input up until ll is received
• im2_l1: received two im and one l; Here, we see if this l belongs to a resetting ll sequence or not.

The encoding of the constraint as a predicate follows:

predicate at_most_two_im(array[int] of var TypeOfShift: shift) =
    let {
        array[1..5, 1..4] of 0..5: transition_relation =
            [| 1, 2, 1, 1 % im0 (start)
             | 2, 4, 2, 3 % im1_l0
             | 2, 4, 2, 1 % im1_l1
             | 4, 0, 4, 5 % im2_l0
             | 4, 0, 4, 1 % im2_l1
            |];
    } in
        regular(
            [ if s ==  m then 1 else
              if s == im then 2 else
              if s ==  o then 3 else
                              4 endif
                                endif
                                endif
              | s in shift],                % sequence of input values
            5,                              % number of states
            card(TypeOfShift),              % number of different input values of state machine
            transition_relation,            % transition relation
            1,                              % initial state
            1..5,                           % final states
         );

---

MiniZinc Example:

Here, I include an extended version of the MiniZinc example with the regular global constraint I provided in my answer to your previous question. I fixed the previous constraint to be compatible with the new im value, and I added the new part. In order to make the problem interesting, I included some additional constraints.

include "globals.mzn";

    %%%%%%%%%%%%%%%%%%
    %%% PARAMETERS %%%
    %%%%%%%%%%%%%%%%%%

enum TypeOfShift = { m, im, o, l };

enum Staff = { Henry, Martin, Theresa, Peshek, Radzig, Capon };

array[Staff, 1..30] of TypeOfShift: roster = [|
    % sat:
    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:
    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
    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
    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|
    % sat:
    m, m, m, l, l, o, m, im,  m,  m, l, l, l, m, m, im, im, m, m, l, l, m, m, m, im, m, l, l, l, l|
    % unsat: too many im
    m, m, m, l, l, o, m, im, im, im, l, l, l, m, m, im,  m, m, m, l, l, m, m, m,  m, m, l, l, l, l|];

    %%%%%%%%%%%%%%%%%
    %%% VARIABLES %%%
    %%%%%%%%%%%%%%%%%

% freely assigned
array[1..30] of var TypeOfShift: free_shift;

    %%%%%%%%%%%%%%%%%%
    %%% PREDICATES %%%
    %%%%%%%%%%%%%%%%%%

predicate at_most_six_m(array[int] of var TypeOfShift: shift) =
    let {
        array[1..14, 1..4] of 0..14: transition_relation =
            [|  2,  2,  1,  8 % m0_l0
             |  3,  3,  2,  9 % m1_l0
             |  4,  4,  3, 10 % m2_l0
             |  5,  5,  4, 11 % m3_l0
             |  6,  6,  5, 12 % m4_l0
             |  7,  7,  6, 13 % m5_l0
             |  0,  0,  7, 14 % m6_l0
             |  2,  2,  1,  1 % m0_l1
             |  3,  3,  2,  1 % m1_l2
             |  4,  4,  3,  1 % m2_l3
             |  5,  5,  4,  1 % m3_l4
             |  6,  6,  5,  1 % m4_l5
             |  7,  7,  6,  1 % m5_l6
             |  0,  0,  7,  1 % m6_l7
            |];
    } in
        regular(
            [ if s ==  m then 1 else
              if s == im then 2 else
              if s ==  o then 3 else
                              4 endif
                                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
         );

predicate at_most_two_im(array[int] of var TypeOfShift: shift) =
    let {
        array[1..5, 1..4] of 0..5: transition_relation =
            [| 1, 2, 1, 1 % im0 (start)
             | 2, 4, 2, 3 % im1_l0
             | 2, 4, 2, 1 % im1_l1
             | 4, 0, 4, 5 % im2_l0
             | 4, 0, 4, 1 % im2_l1
            |];
    } in
        regular(
            [ if s ==  m then 1 else
              if s == im then 2 else
              if s ==  o then 3 else
                              4 endif
                                endif
                                endif
              | s in shift],                % sequence of input values
            5,                              % number of states
            card(TypeOfShift),              % number of different input values of state machine
            transition_relation,            % transition relation
            1,                              % initial state
            1..5,                           % final states
         );


    %%%%%%%%%%%%%%%%%%%
    %%% CONSTRAINTS %%%
    %%%%%%%%%%%%%%%%%%%

% CHECK VALIDITY

%constraint forall (s in Staff)
%(
%    let {
%        array[int] of TypeOfShift: shift = [ roster[s, i] | i in 1..30 ];
%    } in
%        at_most_six_m(shift)
%);

%constraint forall (s in Staff where s in { Capon })
%(
%    let {
%        array[int] of TypeOfShift: shift = [ roster[s, i] | i in 1..30 ];
%    } in
%        at_most_two_im(shift)
%);

% GENERATE VALID ASSIGNMENT

constraint at_most_six_m(free_shift);
constraint at_most_two_im(free_shift);

% (additional constraints to make the problem interesting)
constraint 10 == sum(i in 1..30) ( free_shift[i] == m );
constraint  5 == sum(i in 1..30) ( free_shift[i] == im );

    %%%%%%%%%%%%
    %%% GOAL %%%
    %%%%%%%%%%%%

solve satisfy;

I was unable to use Gecode to solve this model within a reasonable time limit. However, OptiMathSAT returns an answer pretty quickly:

~$ mzn2fzn test.mzn
~$ time optimathsat -input=fzn < test.fzn 
free_shift = array1d(1..30, [3, 3, 3, 3, 4, 4, 4, 4, 4, 2, 2, 4, 4, 2, 4, 4, 2, 2, 1, 1, 1, 1, 4, 4, 1, 1, 1, 1, 1, 1]);
----------

real    0m1.733s
user    0m1.712s
sys 0m0.020s

(note: the mzn2fzn translation maps the enum values into numbers, so OptiMathSAT can only print the numbers associated with m, im, o and l)