继续另一篇文章( Minizinc: generate a valid shift )。我试图在双 ls 之间最多保留 2 im。使用常规约束执行此操作非常困难，因为转换表会很大(路径太多)。有什么办法可以解决吗？我已经尝试过这个，但它给了我错误:
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 (m1 早上 6 点到 13 点；m 早上 7 点到 14 点开始；t 晚上 14 点到 21 点；晚上 22 点到早上 7 点；l 休息日；o 办公室 10 点到 14 点；im on call 早上 6 点到 14 点；it on call night 13 to 22; ino on call night 21 to 7)应该创建一个像17,17,24,24,48,48,17,48,48,16这样的数组...这是轮类的StartTime [day+ 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
最佳答案
实际上仍然可以使用常规全局约束来完成此任务，因为DFA仅需要 5 个状态:
这里，im0是初始状态，所有状态也是最终状态:
im0:自上次ll或开始以来没有imim1_l0:收到一个imim1_l1:在im之后收到一个l；在这里，我们看看这个l是否属于重置ll序列。im2_l0:收到两个im，从现在起im不能作为输入，直到收到llim2_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)
关于迷你锌。计算一个周期内的类次次数，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/58573379/