CP-SAT 的天花板答案

【问题标题】：Ceiling in CP-SATCP-SAT 的天花板
【发布时间】：2019-08-27 09:10:55
【问题描述】：

在调度问题中。我想根据工作天数按比例分配假期。现在我有一个使用多个布尔标志的工作解决方案，但它不能很好地扩展。

from ortools.sat.python import cp_model
from math import ceil

model = cp_model.CpModel()
solver = cp_model.CpSolver()

days = model.NewIntVar(0, 365, 'days')
vacations = model.NewIntVar(0, 30, 'vacations')

for i in range(365 + 1):
    flag_bool = model.NewBoolVar(f'days == {i}')
    model.Add(days == i).OnlyEnforceIf(flag_bool)
    model.Add(days != i).OnlyEnforceIf(flag_bool.Not())
    model.Add(vacations == ceil(i * 30 / 365)).OnlyEnforceIf(flag_bool)

# test
model.Add(days == 300)

status = solver.Solve(model)

print(solver.Value(days), solver.Value(vacations))

有什么建议吗？

编辑：一个更普遍的问题是，是否有更好的方法来实现一个变量到另一个变量的预先计算的任意映射。

【问题讨论】：

我不了解 or-tools 但您似乎想要一个简单的线性约束？ vacations == days * 30/365?唯一的问题是有上限，但我很确定您不需要为每个可能的天数添加一个约束……您可能需要一个新变量来计算提醒。
是的，主要问题是天花板，应该有更好的方法来做到这一点，但还没有找到
第一个问题，你需要一个int_var吗？为什么不是 365 bool_vars 的数组？
没问题，使用布尔值更好吗？
布尔变量的总和很快。这些总和的限制是什么？顺便说一句，使用您的代码，它可以在 presolve 期间解决，无需任何搜索。在您的问题上，您要么使用布尔模型，要么使用整数模型。整数模型将是 y = days * 30 + 364。然后是 AddDivisionEquality(vacation, y, 365)，或纯布尔模型。您的选择。

标签： python constraint-programming or-tools cp-sat-solver

【解决方案1】：

按照 Laurent 的建议解决：

ceil(days * 30 / 365) == (days * 30 + 364) // 365

因此

from ortools.sat.python import cp_model

model = cp_model.CpModel()
solver = cp_model.CpSolver()

days = model.NewIntVar(0, 365, 'days')
vacations = model.NewIntVar(0, 30, 'vacations')
tmp = model.NewIntVar(364, 365 * 30 + 364, 'days*30+364')

model.Add(tmp == days * 30 + 364)
model.AddDivisionEquality(vacations, tmp, 365)

# test
model.Add(days == 300)

status = solver.Solve(model)

print(solver.Value(days), solver.Value(vacations))

【讨论】：