Minizinc. Подсчитать количество смен в цикле

Question

Продолжаем с другим постом ( Minizinc: сгенерировать действительный сдвиг ). Я пытаюсь иметь максимум 2 часа между двойными лс. Делать это с обычным ограничением довольно сложно, поскольку таблица переходов будет довольно большой (слишком много путей). Есть ли способ решить это? Я пробовал это, но это дает мне ошибки:

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;

Привет, Патрик ... Я снова застрял ... Я продолжил разработку регулярного выражения, но я поднялся до 55 состояний ... потом я остановилсяЯ пробовал другой подход, который заключается в создании множества часов отдыха между последовательными рабочими днями. Например: mmmtnllmmlttlnnlllm (каждое утро с 6 до 13; m с утра начинается с 7 до 14; t с вечера с 14 до 21; ночь с 22 до 7 утра; l в день отдыха; o офис с 10 до 14; я по вызову с 6 до 14;в вечерние звонки с 13 по 22; ino в вечерние звонки с 21 по 7) должен создать массив, подобный 17,17,24,24,48,48,17,48,48,16 ... который является начальным временем смены [день +1] - (время начала смены [день] + продолжительность смены [день]). Это закодировано. Между последовательными рабочими сменами должно быть 12 часов или более.

Когда есть день отдыха (l), я собираюсь повторить последний период отдыха (48,48 в примере). Это я не знаю, как это сделать. Идея состоит в том, чтобы посчитать рабочие дни между циклами, чтобы проверить следующее: - Не менее 12 часов между последовательными рабочими сменами - Цикл до того, как 48-часовой или более отдых имеют максимум 5 рабочих дней. - Цикл до 54-часового отдыха или более имеет максимум 6 рабочих дней.

Ограничения по ночам (48 часов после ночи, за исключением тех случаев, когда это еще одна ночь или день отдыха, 54 часа после двух ночей) я сделалэто с ограничениями, или я могу сделать это с помощью регулярных выражений ... это нормально

Есть идеи?

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

На самом деле все еще возможно использовать глобальное ограничение normal для этой задачи, поскольку для DFA требуется только 5 состояний:

Здесь im0 - начальное состояние, а все состояния также являются конечными состояниями:

• im0: нет im с момента последнего ll илис начала
• im1_l0: получен один im
• im1_l1: получен один l после im;Здесь мы видим, принадлежит ли это l к последовательности сброса ll или нет.
• im2_l0: получено два im, с этого момента im не может быть входом вплоть до ll получено
• im2_l1: получено два im и один l;Здесь мы видим, принадлежит ли это l к последовательности сброса ll или нет.

Кодирование ограничения в качестве предиката следующее:

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:

Здесь я включаю расширенную версию примера MiniZinc с обычным глобальным ограничением, которое я указал в своем ответе на предыдущий вопрос. Я исправил предыдущее ограничение, чтобы оно было совместимо с новым значением im, и добавил новую часть. Чтобы сделать проблему интересной, я включил некоторые дополнительные ограничения.

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;

Мне не удалось использовать Gecode для решения этой модели в разумные сроки. Однако OptiMathSAT возвращает ответ довольно быстро:

~$ 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

(примечание: перевод mzn2fzn отображает значения перечисления в числа, поэтому OptiMathSAT может тольковыведите числа, связанные с m, im, o и l)