请求优化MiniZinc大规模调度求解：24队8工位场景提速

某活动调度需求：8个工位、24支队伍，每个工位每轮容纳3支队伍，共8轮轮换。要求：

1. 每支队伍8轮遍历所有工位，无重复访问
2. 每轮所有队伍都处于某个工位
3. 任意两支队伍全程碰面不超过1次

原MiniZinc代码如下：

include "alldifferent.mzn";

int: num_teams = 24;         % Number of teams
int: num_stations = 8;       % Number of stations
int: num_rotations = 8;      % Number of rotations
int: teams_per_station = 3;  % Teams per station per rotation

% Decision variable: station assignments
array[1..num_teams, 1..num_rotations] of var 1..num_stations: station;

% Constraints
constraint
    % Each team visits exactly one station in each rotation
    forall(t in 1..num_teams, r in 1..num_rotations) (
        station[t, r] >= 1 /\ station[t, r] <= num_stations
    )
    /\
    % No team visits the same station more than once
    forall(t in 1..num_teams, s in 1..num_stations) (
        sum([station[t, r] == s | r in 1..num_rotations]) <= 1
    )
    /\
    % Each station accommodates exactly teams_per_station teams per rotation
    forall(r in 1..num_rotations, s in 1..num_stations) (
        sum([station[t, r] == s | t in 1..num_teams]) == teams_per_station
    )
    /\
    % Teams do not see each other more than once
    forall(t1 in 1..num_teams, t2 in 1..num_teams where t1 != t2) (
        sum([station[t1, r] == station[t2, r] | r in 1..num_rotations]) <= 1
    );

% Objective: Maximize team diversity by minimizing the number of repeat encounters
solve satisfy;

% Output the station assignments
output [
    "Team " ++ show(t) ++ ": " ++ show([station[t, r] | r in 1..num_rotations]) ++ "\n"
    | t in 1..num_teams
];

该代码在小规模场景下可正常求解，但24队8工位的场景耗时极长，以下是针对性优化方案：

1. 替换冗余约束，强化排列特性 #

原代码前两个约束可合并：由于轮数等于工位数，每支队伍的工位分配本质是1-8的排列，直接用alldifferent约束替代sum判断，求解器会利用排列优化算法大幅减少计算量：

% 替换原前两个约束
forall(t in 1..num_teams) (
    alldifferent([station[t, r] | r in 1..num_rotations])
)

2. 削减重复的碰面约束 #

原约束中t1和t2成对重复检查（如t1=1,t2=2与t1=2,t2=1），改为仅检查t1 < t2，直接减少一半约束数量：

% 替换原碰面约束
forall(t1 in 1..num_teams, t2 in t1+1..num_teams) (
    sum([station[t1, r] == station[t2, r] | r in 1..num_rotations]) <= 1
)

3. 添加对称性破缺约束 #

问题存在大量对称解（工位编号互换、队伍编号互换等），通过固定部分变量值剪枝搜索空间：

• 固定第一支队伍的工位顺序，消除工位编号对称：

constraint forall(r in 1..num_rotations) (station[1, r] = r);

• 固定第一轮的队伍分组，消除初始分配的对称分支：

% 示例：第一轮工位1分配队伍1-3，工位2分配队伍4-6，以此类推
constraint sum([station[t, 1] == 1 | t in 1..3]) = 3;
constraint sum([station[t, 1] == 2 | t in 4..6]) = 3;
constraint sum([station[t, 1] == 3 | t in 7..9]) = 3;
% ... 继续固定剩余工位的第一轮队伍

4. 优化求解器配置 #

• 选择Gecode或Chuffed这类针对组合优化的高效求解器，替代默认求解器；
• 指定搜索策略，引导求解器优先剪枝无效分支：

solve :: int_search(station, first_fail, indomain_min, complete) satisfy;

• 开启求解器的并行搜索功能（若支持），利用多核CPU加速计算。

5. 构造初始解缩小搜索范围 #

手动构造部分轮次的合法调度作为初始解，减少求解器的盲目搜索：
比如先完成前3轮的合理分配，再让求解器填充剩余轮次，能大幅缩短搜索时间。

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