如何在OR-Tools CP-SAT求解器中优雅实现分段线性约束？

问题设定条件 #

• 需在2天内为一名工人分配2项任务
• 仅有一名工人，其每日最多工作8小时
• 目标为最小化总工作时长
• 任务可打包以提升效率，所需工时如下：
  • 0项任务 → 0小时
  • 1项任务 → 6小时
  • 2项任务 → 8小时

显然，最优方案是该工人在1天内完成两项任务，仅需8小时。

任务数量与工时关系 #

任务数量n和所需工时的对应关系如下：

• 蓝色虚线：理论线性工时 y = 6*n
• 黑色实线：实际工时 = min(6*n, 6 + 2*(n-1))
• 红色实线：每日工时上限（8小时）

对应的Python计算函数为：

def compute_hours(n):
    return min(6*n, 6 + 2 * (n - 1))

疑问 #

目前已知可通过添加布尔指示器变量，确保未分配任务时总工时为0，但在OR-Tools的CP-SAT求解器中，是否有更优雅的方式实现该分段线性约束？

内容的提问来源于stack exchange，提问作者John