OR-Tools CP-SAT求解器中预设解与假设条件冲突的Bug分析

问题概述

在使用OR-Tools的CP-SAT求解器时，当同时使用预设解(solution hint)和假设条件(assumptions)功能时，在某些情况下会出现求解器返回错误状态的问题。具体表现为：当模型实际上无解(UNSAT)时，求解器却错误地报告找到了可行解(OPTIMAL)。

问题重现

考虑以下简单的布尔约束模型：

1. 定义两个布尔变量x和y
2. 添加约束条件：x必须为真(x ∨ 0)
3. 添加约束条件：x和y不能同时为真(¬x ∨ ¬y)
4. 设置假设条件：y必须为真(y=1)
5. 提供预设解：y=1

在这种情况下，模型明显无解，因为：

• 假设条件要求y=1
• 第一个约束要求x=1
• 但第二个约束禁止x和y同时为1

预期与实际行为对比

预期行为：求解器应返回INFEASIBLE状态，表示模型在给定假设下无解。

实际行为：

• 当启用预设解和预求解(presolve)时，求解器错误地返回OPTIMAL状态，并给出无效解[x=1,y=0]
• 当禁用预设解或禁用预求解时，求解器正确返回INFEASIBLE状态

技术分析

这个问题源于预求解阶段与预设解、假设条件的交互处理不当。预求解是CP-SAT求解器在正式求解前进行的简化步骤，旨在减少问题规模。在这个案例中：

1. 预求解阶段可能过于激进地处理了假设条件
2. 预设解的优先级可能被错误地评估
3. 求解器在预求解后未能正确验证解是否满足所有假设条件

影响范围

这个bug会影响以下使用场景：

• 同时使用预设解和假设条件的模型
• 启用了预求解功能的模型(默认启用)
• 模型在假设条件下实际无解的情况

临时解决方案

在官方修复发布前，用户可以采取以下临时解决方案：

1. 禁用预求解功能：solver.parameters.cp_model_presolve = False
2. 避免在可能冲突的情况下同时使用预设解和假设条件
3. 手动验证返回的解是否满足所有假设条件

总结

OR-Tools CP-SAT求解器在处理预设解与假设条件的交互时存在一个边界情况下的bug，导致在某些配置下返回错误的状态信息。虽然官方已确认此问题并将进行修复，但用户在使用这些高级功能时应当注意验证求解结果的正确性，特别是在模型可能无解的情况下。