如何在MiniZinc中强制约束数组元素按行优先级排列

你的原始方案效率低的核心原因是forall嵌套exists的结构会产生大量重复的存在性检查，约束传播能力弱，求解器需要大量回溯才能满足约束。以下是两种效率更高的实现方案：

方案1：直接绑定行范围（最高效） #

直接给每个决策变量的取值范围绑定到对应行允许的位置区间，求解器在预处理阶段就能直接裁剪变量域，几乎没有运行时开销：

set of int: people = 1..10;
int: row = 3;
include "alldifferent.mzn";

% 预计算每行的人数、区间起始和结束值
set of int: row_ids = 0..row-1;
array[row_ids] of int: row_member_count = [ sum(p in people)(p mod row == r) | r in row_ids ];
array[row_ids] of int: row_min_pos = [ sum(s in 0..r-1)(row_member_count[s]) + 1 | r in row_ids ];
array[row_ids] of int: row_max_pos = [ sum(s in 0..r)(row_member_count[s]) | r in row_ids ];

array[people] of var people: position;
constraint alldifferent(position);

% 直接限定每个人员的position只能在对应行的范围内
constraint forall(p in people)(
    position[p] in row_min_pos[p mod row] .. row_max_pos[p mod row]
);

这个方案完全避免了跨人员的关联检查，约束传播强度最高，求解速度最快。

方案2：跨行大小约束 #

如果需要保留更灵活的行内排序逻辑，可以用两层forall替代嵌套的exists，同样能大幅提升效率：

array[people] of int: row_of = [ p mod row | p in people ];
constraint forall(p1 in people, p2 in people where row_of[p1] < row_of[p2])(
    position[p1] < position[p2]
);

这个方案的逻辑更直观，只要是前排人员的position就一定小于后排所有人员的position，完全满足业务规则，且没有exists带来的搜索开销。

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