OR-Tools项目中CP-SAT求解器在C测试中的模型有效性验证问题

问题背景

在OR-Tools项目的最新版本中，C#语言绑定的CP-SAT求解器测试模块发现了一个关于模型有效性的验证问题。具体表现为SatSolverTest.cs测试文件中的两个测试用例未能通过验证，系统返回"ModelInvalid"状态而非预期的"Optimal"状态。

问题分析

测试用例的核心是构建一个简单的线性模型原型(CpModelProto)，包含以下关键组件：

1. 创建三个整数变量，范围分别为[-10,10]、[-10,10]和[-1000000,1000000]
2. 添加两个线性约束条件：
   • 第一个约束：变量0和变量1的线性组合，系数为1和1
   • 第二个约束：变量0、变量1和变量2的线性组合，系数为1、2和-1
3. 设置最大化变量2的目标函数

问题根源在于目标函数的构建方式。原始代码中使用了obj.Vars.Add(-v1 - 1)的方式添加变量索引，这会导致变量索引越界，因为变量索引应为非负整数。

技术细节

在CP-SAT求解器的实现中，变量索引必须严格对应模型中已定义的变量。当目标函数中引用了不存在的变量索引时，求解器会返回MODEL_INVALID状态，并附带错误信息"Out of bound integer variable"。

正确的做法应该是直接使用变量索引，而不进行负值转换。修复方案是将目标函数构建改为直接添加变量索引和系数：

obj.Vars.Add(v1);
obj.Coeffs.Add(c1);

解决方案验证

通过修改测试代码并构建一个简化的验证程序，可以确认修复后的行为：

1. 构建正确的CpModelProto模型
2. 直接使用变量索引而非转换后的值
3. 调用求解器后，现在能够返回预期的"Optimal"状态

经验总结

这个案例揭示了在使用OR-Tools的CP-SAT求解器时需要注意的几个关键点：

1. 变量索引必须严格对应模型定义中的变量顺序
2. 目标函数中的变量引用必须使用原始索引值
3. 当求解器返回MODEL_INVALID状态时，应仔细检查所有变量引用是否正确
4. 测试用例应当覆盖各种边界条件，包括变量索引的有效性验证

该问题的修复已经合并到项目的主分支和稳定版本分支中，确保了C#绑定的CP-SAT求解器在模型验证方面的正确性。