OR-Tools CP-SAT求解8餐社交高尔夫问题超时无结果

1. 先验证问题可行性 #

从组合数学角度初步判断是否存在解，避免无效搜索：

• 总两两组合数：C(190,2)=17955，即最多允许17955次同桌对
• 8餐可产生的同桌对总数：8×19×C(10,2)=8×19×45=6840，远小于总允许数
• 1-19号的约束仅要求每餐分坐不同桌，他们之间不会产生同桌对，不影响整体可行性
  结论：问题理论上存在可行解，需优化求解效率而非放弃。

2. 模型优化 #

减少冗余约束 #

• 同桌次数约束仅需处理p < q的人员对，避免重复约束（p和q的同桌关系是对称的），将约束数量从190×189=35010减少到17955，大幅降低求解器负担
• 跳过1-19号之间的同桌约束（他们每餐必不同桌，同桌次数恒为0），再减少C(19,2)=171个约束

优化变量表示 #

• 对1-19号（核心人员）使用排列变量：为每餐创建一个19元素的全排列变量（表示核心人员的桌号分配），替代为每个核心人员单独创建桌号变量并添加两两不同约束，排列变量的内部优化能提升求解效率
• 对普通人员保留table[p][m]（人p在第m餐的桌号）的整数变量表示，保持紧凑性

高效实现人数约束 #

• 使用OR-Tools的AddCount约束替代循环判断：对每餐每桌，通过model.AddCount([table[p][m] for p in all_people], table_id, 10)直接约束该桌人数为10，比逐个添加人员归属约束更高效

3. 求解器参数调优 #

• 启用多线程搜索：设置parameters.num_search_workers = <CPU核心数>（如8或16），利用多核并行搜索提升速度
• 调整线性化等级：设置parameters.linearization_level = 2，让求解器更高效地处理布尔型约束（如同桌判断）
• 启用搜索进度日志：设置parameters.log_search_progress = True，观察搜索过程中的节点数、约束传播情况，判断是否卡在特定分支
• 优先寻找可行解：设置parameters.search_branching = cp_model.PORTFOLIO_SEARCH，让求解器尝试多种分支策略，优先探索更可能找到可行解的路径

4. 定制搜索策略 #

• 优先处理核心人员：通过model.AddDecisionStrategy(leader_table_vars, cp_model.CHOOSE_FIRST, cp_model.SELECT_MIN_VALUE)指定先分配1-19号的桌号，利用其强约束快速剪枝无效分支
• 提供初始解提示：基于已求出的7餐可行解，用model.AddHint(table[p][m], 7_meal_solution[p][m])为前7餐的变量赋值，让求解器从已有解出发扩展第8餐，大幅缩小搜索空间

5. 分步分解问题 #

• 拆分核心人员与普通人员的求解：
  1. 先单独求解1-19号的8餐桌号分配（仅需满足每餐全排列约束），这个子问题规模小，可快速得到解
  2. 将核心人员的桌号分配固定到主模型中，再求解普通人员的座位安排，此时问题复杂度大幅降低
• 增量扩展求解：先求解7餐的解，再在该解基础上添加第8餐的约束进行搜索，避免从零开始遍历整个解空间

6. 其他辅助手段 #

• 检查代码中是否存在低效的约束写法（如重复计算、不必要的变量），比如避免在循环中重复创建相同逻辑的约束
• 尝试更新OR-Tools到最新版本，新版本通常会优化求解器的搜索算法和性能

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