您如何在 OrTools 中定义 At-Most-K SAT 约束

问题描述

最多k个约束，给定多个任务和用户，其中给定数量的任务必须由最多k个用户完成，每个任务只分配给一个用户，一个用户可以有多个任务。目标是找出哪些任务分配给了哪些用户。

一个示例实例是，给定 4 个用户和 4 个任务，对最多 2 个用户、task1、task2、task3 的约束进行编码。

我正在使用 OrTools python 库对此进行编码，但任何解释都会有所帮助

解决方法

只需为每个 (user,taskgroup_id) 对创建一个 boolvar 并将其限制为：

for t in taskgroup:
    # t1 v t2 v t3 => user_in_group
    model.AddImplication(assigment[u,t],user_in_taskgroup[u,taskgroup_id])

# user_in_group => t1 v t2 v t3
model.AddBoolOr([user_in_taskgroup[u,taskgroup_id].Not()] + [assigment[u,t] for t in tasks])

model.Add(sum(user_in_taskgroup[u,taskgroup_id] for u in users) <= k)