MiniZinc实现：确保数组中指定元素至少连续出现2次

需求说明 #

需在MiniZinc中实现约束，确保数组中若存在元素1，其每一次出现都必须至少紧跟一个1（即1不能单独出现，需连续至少2次）：

• 有效示例：
  • [1, 1, 0, 0, 0, 0, 0, 0, 0, 0]
  • [1, 1, 1, 0, 0, 0, 0, 0, 0, 0]
  • [2, 3, 1, 1, 4, 5, 6, 7, 1, 1]
• 无效示例：
  • [0, 1, 0, 0, 0, 0, 0, 0, 0, 0]
  • [2, 1, 3, 4, 5, 1, 8, 9, 9, 1]

原代码问题分析 #

你提供的代码仅能处理1恰好出现2次的场景，核心问题在于通过i mod 2 == 0的条件强制偶数位置与前一位置绑定1，这种逻辑限制了1的出现形式，无法支持3个及以上连续的1，也不具备通用性。

解决方案 #

以下是满足需求的通用约束实现，核心逻辑是确保任何一个1都属于至少长度为2的连续序列：

% 定义数组参数
int: n = 10; % 数组长度
array[1..n] of var 0..5: arr; % 示例数组，元素范围0-5

% 核心约束：禁止单独出现的1
constraint forall(i in 1..n) (
    arr[i] = 1 -> (
        (i > 1 /\ arr[i-1] = 1) \/ (i < n /\ arr[i+1] = 1)
    )
);

% 可选约束：若需要强制数组中存在1，可取消注释
% constraint exists(i in 1..n) (arr[i] = 1);

solve satisfy;

output [show(arr)];

约束逻辑解释 #

该约束的含义是：

• 对于数组中的每个元素，若其值为1，则要么前一个元素也是1（说明它是连续1序列的中间或结尾），要么后一个元素也是1（说明它是连续1序列的开头或中间）。
• 这就彻底避免了单独的1：数组首尾的1必须有相邻的1，中间的1不可能前后都不是1。

验证效果 #

• 有效示例中的多连续1场景会被允许，比如[1,1,1,...]里的每个1都满足相邻有1的条件；
• 无效示例中的单独1会被约束排除，比如[0,1,0,...]里的1前后都不是1，违反约束。

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