python - CP-SAT 的天花板

Question

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

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))

有什么建议么？

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

Answer 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))