OR-Tools二次整数规划模型不可行问题排查技巧咨询

问题背景 #

初次使用OR-Tools求解含大量IntVar变量的二次目标函数最小化问题，小规模案例运行正常，但大规模场景下模型返回INFEASIBLE状态，需排查根源。

模型运行日志（已翻译） #

Starting CP-SAT solver v9.6.2534
Parameters: log_search_progress: true enumerate_all_solutions: true
Setting number of workers to 1

初始优化模型 '': (model_fingerprint: 0x8f376cd881ed44f1)
#变量总数: 214 (#目标函数中整数变量数:1)

- 126个布尔变量 [0,1]
- 2个整数变量 [-100000,100000]
- 84个整数变量 [0,96]
- 2个整数变量 [0,2000000]
#kIntProd类型约束数量: 4004

0.00s 开始预求解
预处理约束#1142后发现不可行（警告：输出可能不一致）: int_prod { target { vars: 214 coeffs: 3249 offset: 3249 } exprs { vars: 212 coeffs: 570 offset: -102 } exprs { vars: 212 coeffs: 570 offset: -102 } }

预求解总结:
- 检测到2个仿射关系。
- 规则'affine: new relation'应用2次。
- 规则'int_prod: divide product by constant factor'应用2次。
- 规则'int_prod: linearize product by constant.'应用1140次。
- 规则'int_prod: removed constant expressions.'应用1140次。
- 规则'int_square: reduced target domain.'应用2次。
- 规则'linear: remapped using affine relations'应用1次。
- 规则'presolve: iteration'应用1次。
- 规则'variables: canonicalize affine domain'应用2次。
问题在预求解阶段判定为不可行。

CpSolverResponse 摘要:
status: INFEASIBLE
objective: NA
best_bound: NA
integers: 0
booleans: 0
conflicts: 0
branches: 0
propagations: 0
integer_propagations: 0
restarts: 0
lp_iterations: 0
walltime: 0.007945
usertime: 0.007945
deterministic_time: 0
gap_integral: 0

具体排查技巧 #

1. 优先定位预求解阶段的冲突约束 #

日志明确显示预求解处理约束#1142后直接判定不可行，该约束是一个二次乘积约束：两个相同的线性表达式（变量212的线性组合减102）的乘积，等于变量214的线性组合加3249。

• 核对该约束的业务逻辑：确认约束要表达的关系是否正确，是否存在需求理解偏差
• 验证取值范围兼容性：计算两个线性表达式的可能取值区间，乘积后的结果是否落在目标变量的定义域内
• 检查建模笔误：比如系数、偏移量是否写错，变量引用是否错误（例如此处两个表达式用了同一个变量集合，是否符合业务逻辑）

2. 逐步简化模型定位冲突源 #

• 移除所有非核心约束，只保留目标函数和最基础的变量定义域约束，验证模型是否可行
• 逐步添加约束，每次添加后运行模型，直到出现INFEASIBLE，此时新增的约束就是冲突的核心来源
• 将大规模模型拆分为多个小规模子问题，分别验证可行性，再逐步合并子问题，找到合并时触发冲突的部分

3. 检查变量定义域与二次项的匹配性 #

• 二次项的乘积结果可能超出目标变量的定义域范围，直接导致不可行：比如两个表达式的乘积最大值远大于目标变量的上限，或者最小值小于目标变量的下限
• 检查不同类型变量的组合是否隐含冲突：比如布尔变量与大范围整数变量的乘积，是否会产生无法满足其他约束的取值

4. 启用详细调试日志 #

• 在求解前添加参数：solver.parameters.log_level = cp_model.LOG_VERBOSE，获取预求解阶段的详细推导过程，明确约束#1142被判定不可行的具体原因
• 尝试禁用部分预求解规则（比如int_prod的线性化规则），虽然会降低求解效率，但能获得更直接的冲突提示

5. 验证二次目标函数的建模正确性 #

• OR-Tools CP-SAT原生仅支持线性目标函数，二次目标需要通过辅助变量+乘积约束实现，检查是否存在建模错误：
  • 辅助变量的定义域是否覆盖了二次项的所有可能取值
  • 二次项转化为约束的过程是否正确，是否遗漏了必要的关系

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