为何OR-Tools中CP-SAT求解N皇后更慢？求性能优化方案

我使用Python 3.12结合OR-Tools实现了N皇后问题，分别采用官方提供的CP-SAT求解器和原始约束规划求解器完成开发，为简化对比，已移除两个脚本中的结果打印模块。实验显示二者性能差异显著，以12皇后为例，运行时间统计如下：

原始求解器运行结果 #

time python queens-original.py

Statistics
  failures: 116806
  branches: 262010
  wall time: 688 ms
  Solutions found: 14200
python queens-original.py  0.72s user 0.01s system 99% cpu 0.736 total

CP-SAT求解器运行结果 #

time python queens-cp-sat.py  

Statistics
  conflicts      : 133465
  branches       : 708019
  wall time      : 10.891582737 s
  solutions found: 14200
python queens-cp-sat.py  11.59s user 0.62s system 106% cpu 11.424 total

问题 #

1. 为何该问题场景下原始求解器性能显著优于CP-SAT？
2. 是否存在可优化CP-SAT实现的调整方案，使其性能更接近原始求解器？

问题1解答 #

OR-Tools的原始约束规划求解器是专为传统组合优化问题设计的，在N皇后这类高度结构化的问题上，核心机制更贴合问题特性：

• 约束处理效率更高：原始求解器内置了针对排列类约束（N皇后本质是每行每列唯一的排列问题）的高效传播算法，无需额外编码转换；而CP-SAT基于SAT求解器，需要将整数约束转化为布尔子句，这一过程会引入额外计算开销。
• 搜索策略更适配：原始求解器的变量选择、值选择启发式是针对经典CP场景优化的，能快速剪枝无效搜索分支；CP-SAT默认启发式更偏向大规模布尔约束问题，在这类小规模但高度结构化的问题上，搜索效率反而更低。
• 额外开销更小：CP-SAT的SAT核心包含冲突子句学习、复杂回溯等机制，在N皇后这类不需要复杂布尔推理的问题上，这些机制带来的额外开销超过了其优势。

问题2解答 #

可以通过以下调整优化CP-SAT的性能，缩小与原始求解器的差距：

• 使用高效约束：针对N皇后的行列唯一性，直接使用model.AddAllDifferent约束，避免手动拆分多个布尔约束；对于对角线约束，用row_i - col_i和row_i + col_i的唯一性约束替代逐对约束，减少约束数量。
• 自定义搜索启发式：手动设置搜索策略，匹配原始求解器的逻辑：

  from ortools.sat.python import cp_model
  
  solver = cp_model.CpSolver()
  # 选择受影响最大的变量优先分支
  solver.parameters.variable_selection = cp_model.CHOOSE_MAX_AFFECTED
  # 选择影响最小的值优先尝试
  solver.parameters.value_selection = cp_model.SELECT_MIN_IMPACT
  # 或者使用固定分支策略，接近原始CP求解器逻辑
  solver.parameters.search_branching = cp_model.FIXED_SEARCH
  

• 添加对称性破缺约束：N皇后存在大量对称解，添加约束减少重复搜索，比如固定第一行皇后的位置在左半部分：

  n = 12
  queens = [model.NewIntVar(0, n-1, f'queen_{i}') for i in range(n)]
  model.Add(queens[0] <= (n // 2))
  

• 调整求解器参数：关闭不必要的多线程（单线程在这类问题上可能更高效），减少冲突子句学习的开销：

  solver.parameters.num_search_workers = 1
  solver.parameters.conflict_learning = cp_model.NO_LEARNING
  

• 禁用冗余特性：关闭CP-SAT的部分高级预处理特性，减少启动和运行时的额外开销。

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