时间戳

首页 > 解决方案 > Or-tools cp_sat求解器结果不一致

or-tools - Or-tools cp_sat求解器结果不一致

问题描述

我有一个优化问题，我正在使用 or-tools cp_sat 求解器。变量的数量约为 3500（都是布尔值），但约束的数量很大（~750000）。在 3500 个变量中，约 3000 个直接依赖于其他 500 个变量。我测试了 2 个场景：

  1. 有一个简单的目标函数，取决于约 3000 个约束变量。
  2. 具有取决于 ~3000*3000 个新变量的复杂目标函数，其中每个新变量是 (1) 中变量的成对逻辑与。

对于每种情况，我们为求解器提供约 500 个变量的提示。

对于 1，它无法在合理的时间内找到最优解。运行大约 30-45 分钟后，目标函数的改进可以忽略不计，但解决方案令人满意。

对于 2，行为很奇怪。大约一半的时间，它声称问题是不可行的，一半的时间，声称它找到了最佳解决方案，但只返回提示暗示的解决方案。只有很少（少于百分之几的运行），它会进行一些优化并返回 FEASIBLE。

此外，案例 1 使用大约 4-6 GB 内存，但案例 2 使用 100-120 GB 内存。

案例 2 中的行为是预期的吗？我应该如何进行调试？

标签： or-tools

解决方案

对于案例2，问题变得非常大。您正在创建 9M 布尔变量。

你在使用多线程吗？

你可以尝试减小模型的大小，看看这是否仍然是片状的？

问题的产生是确定性的吗？

你用的是大系数吗？您是否可能遇到整数溢出错误？

谢谢

推荐阅读