在MiniZinc中计算无效工时：统计数组首尾1之间的0的数量

错误原因分析 #

• 第一个错误：arg_max.mzn提供的arg_max函数仅支持常量数组，无法处理var 0..1类型的变量数组，因此直接调用会触发类型不匹配错误。
• 第二个错误：MiniZinc不允许使用变量值作为数组切片的范围索引（比如arg_max(x)+1是变量表达式），这是约束求解器的底层限制。

正确实现方案 #

我们可以通过直接统计满足条件的元素数量来规避数组切片的限制，核心思路是：

1. 找到数组中第一个值为1的位置first_1
2. 找到数组中最后一个值为1的位置last_1
3. 统计所有位于first_1和last_1之间（包含两端）且值为0的元素数量，即为无效工时

以下是完整的可运行代码：

array[1..6] of var 0..1: arr = [0, 1, 0, 0, 1, 1];

function int: waste(array[int] of var 0..1: x) =
    let {
        int: len = length(x);
        % 定义第一个1的位置，若全为0则设为len+1（不影响后续计算）
        var int: first_1 = min(i in index_set(x) where x[i] == 1) i;
        % 定义最后一个1的位置，若全为0则设为0（不影响后续计算）
        var int: last_1 = max(i in index_set(x) where x[i] == 1) i;
    } in
    if sum(x) == 0 then
        0
    else
        % 统计first_1到last_1之间值为0的元素数量
        sum(i in index_set(x) where i >= first_1 /\ i <= last_1 /\ x[i] == 0) 1
    endif;

output ["wasted hours = \(waste(arr))"];

代码说明 #

• first_1：通过min(i in index_set(x) where x[i] == 1) i找到第一个值为1的索引，当数组全为0时，结合sum(x)==0的判断直接返回0。
• last_1：通过max(i in index_set(x) where x[i] == 1) i找到最后一个值为1的索引。
• 无效工时计算：遍历数组所有索引，只统计位于first_1和last_1之间且值为0的元素，用sum累加计数。

测试结果 #

运行上述代码，输入数组[0,1,0,0,1,1]会输出：

wasted hours = 2

与示例预期结果一致。

内容的提问来源于stack exchange，提问作者cnzo