Minizinc：生成有效的转变

希望有人能帮助我解决这个问题！

最初的问题是生成有效的班次，如下所述：

我有这样的数组 [m,m,m,o,o,l,l,m,m,m,l,m,m,m] 具有固定长度（S），其中 m 是工作，o 是办公室，我自由了。我需要确保至少每 6m 就有两个 l 在一起 (ll)。 o 不算作工作或免费。例子：

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

我试图创建一个包含 0（表示 ls）和 1（表示 ms）的数组，但从数组中删除所有 o 和非连续的 ls。因此，对于上面的例子来说：

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

这样我就可以使用 slider_sum 或 at_least 约束来解决它。但是，我无法创建这个新数组，因为它的大小与原始数组 (S) 不同。一个有效的选项是在末尾用 0 填充剩余的槽，直到 S。

任何帮助表示赞赏

编辑。这是到目前为止的代码：

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];

这个答案提供了一个简单有效问题中所述问题的解决方案，即如何确定是否给定班次是否有效。 [注意，在这种情况下，不需要（其实是适得其反）将任何数组的内容声明为var $T].

一种选择是：

• 确定所有的起始位置ll在数组中（数组double_l_pos)
• 确定每个的位置o在数组中（数组has_o)
• 确定累计数量o从头开始在数组中（数组cum_has_o)
• 固定所有的位置ll这样它就会忽略任何o在它之前（数组fixed_double_l_pos)
• 确定所有之间的距离ll起始位置（数组double_l_distance)
• 要求距离值不大于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;

这里的一切都是静态计算的，因此即使在实际求解开始之前也可以检测到模型的不一致。

附录：因为这是一个roster问题，您可能需要详细阅读roster https://github.com/MiniZinc/minizinc-benchmarks/tree/master/roster和待命排班 https://github.com/MiniZinc/minizinc-benchmarks/tree/master/on-call-rostering模型在MiniZinc基准存储库。这些文件可能包含处理您的问题的更好方法。