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

Question

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

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

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

Answer 1

只需为每个(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)