OR-Tools CP-SAT求解器中约束顺序影响求解结果的Bug分析

问题描述

在使用OR-Tools的CP-SAT求解器(v9.9)时，发现一个有趣的现象：模型中约束的添加顺序会影响最终的求解结果。具体表现为，在某些情况下，改变约束的添加顺序会导致原本可行的问题被错误地判定为不可行。

技术背景

CP-SAT求解器是OR-Tools中的一个约束规划求解器，它结合了约束编程(CP)和布尔可满足性(SAT)技术。在求解过程中，求解器会先进行预处理(presolve)阶段，这个阶段会对模型进行简化和优化，以提高后续求解效率。

问题复现

通过一个具体的整数规划模型可以复现这个问题。模型包含多个整数变量和两类约束：

1. 线性等式约束：连接多个变量之间的关系
2. 除法等式约束：使用add_division_equality方法定义

当按照特定顺序添加这些约束时，求解器会错误地报告问题不可行；而简单地调整约束添加顺序后，同一问题又能被正确识别为可行。

问题本质

这个问题源于预处理阶段的bug。预处理阶段在对模型进行简化时，由于约束处理顺序的影响，可能导致某些变量关系被错误地简化或消除，从而造成后续求解阶段无法找到实际存在的可行解。

临时解决方案

在官方修复此问题前，可以通过以下方式规避：

s = cp_model.CpSolver()
s.parameters.cp_model_presolve = False  # 禁用预处理
print(s.solve(model))

禁用预处理虽然可能略微降低求解效率，但能保证求解结果的正确性。

技术建议

1. 当遇到类似"模型应该可行但求解器报告不可行"的情况时，可以尝试调整约束添加顺序
2. 在调试阶段，可以暂时禁用预处理功能来验证是否为预处理导致的bug
3. 对于关键业务场景，建议在多个OR-Tools版本上交叉验证结果

总结

这个案例展示了约束求解器中一个有趣的现象：约束处理顺序可能影响求解结果。虽然这本质上是一个需要修复的bug，但它也提醒我们，在使用数值计算和优化工具时，应该对结果保持适当的怀疑态度，特别是当结果与直觉相悖时。