CP 坐立并寻找解决方案的死胡同

Question

只是想知道当 CP SAT 选择一个不会导致全局最优的分支时会做什么？例如，最小化目标返回的代码：

Solution 0, time = 1.05 s, objective = 11700
Solution 1, time = 1.59 s, objective = 9200
Solution 2, time = 4.54 s, objective = 9100
Solution 3, time = 5.14 s, objective = 8600
Solution 4, time = 6.44 s, objective = 7600
Solution 5, time = 8.04 s, objective = 7100
Solution 6, time = 8.72 s, objective = 6000
Solution 7, time = 10.44 s, objective = 5900
Solution 8, time = 15.67 s, objective = 1600
Solution 9, time = 16.29 s, objective = 200

我理解它忽略了在最小化上下文方面具有更大客观价值的解决方案。

以下是设置。

solver = cp_model.CpSolver()
solver.parameters.max_time_in_seconds = 100
solver.parameters.num_search_workers = 16

由于代码在 40 秒内完成，我们可以假设它枚举了所有解决方案吗？我无法将 enumerate_all_solutions 参数与 num_search_workers 结合使用。

Answer 1

像所有求解器一样，它会尽快修剪分支。 请注意，SAT 求解器中的搜索不是树搜索。

40s后，证明该解是最优的。幸运的是，它不需要枚举所有解决方案来这样做。

注意：线性化级别 = 0 很奇怪。它会改变什么吗？