如何用Google OR-Tools实现工作流可满足性问题的至多约束？代码排查

问题背景 #

需求是给步骤集合分配用户时，每个集合至多分配k个用户（比如步骤1、2、3最多分配2个用户）。每个任务仅分配给一位用户，用户可承担多个任务。用assignments[user_x, step_y]布尔变量表示user_x是否被分配到step_y。输入是列表列表格式，例如[[2,1,2,3], [3,1,2,3,4,5]]代表两条约束：步骤1-3最多2个用户，步骤1-5最多3个用户。

用户编写的代码如下：

for list in range(len(at_most_k)):
    # get max number of users
    k = at_most_k[list][0]
    # get the group of steps
    group_of_steps = at_most_k[list][1:]
    user_group = []
    for steps in group_of_steps:
        for users in range(num_users):
            user_group.append(assignments[users, steps-1])
    model.Add(sum(user_group) <= k)

错误原因 #

这段代码的核心逻辑错误：它把所有用户-步骤对的布尔值求和，统计的是「用户被分配到步骤组的总次数」，而非「被分配到步骤组的不同用户数量」。比如一个用户被分配到步骤组里的3个步骤，会被计数3次，但实际该用户只应算1个，导致约束完全不符合需求。

修正方案 #

需要先判断每个用户是否被分配到步骤组的任意一个步骤，再统计这样的用户总数，确保不超过k。代码如下：

for constraint in at_most_k:
    max_users = constraint[0]
    step_group = constraint[1:]
    user_participation = []
    
    for user_idx in range(num_users):
        # 创建辅助变量：标记该用户是否参与当前步骤组
        is_in_group = model.NewBoolVar(f"user_{user_idx}_in_step_group")
        
        # 关联辅助变量与用户的分配状态：只要用户在步骤组任意步骤有分配，is_in_group为True
        model.AddBoolOr([assignments[user_idx, step-1] for step in step_group]).OnlyEnforceIf(is_in_group)
        # 反之，若用户在步骤组所有步骤都没分配，is_in_group为False
        model.AddBoolAnd([assignments[user_idx, step-1].Not() for step in step_group]).OnlyEnforceIf(is_in_group.Not())
        
        user_participation.append(is_in_group)
    
    # 添加核心约束：参与步骤组的用户总数不超过max_users
    model.Add(sum(user_participation) <= max_users)

逻辑说明 #

• 对每个用户创建辅助布尔变量is_in_group，仅当该用户被分配到步骤组中至少一个步骤时为True。
• 通过AddBoolOr和AddBoolAnd将辅助变量与用户的实际分配状态绑定，确保变量值准确反映用户是否参与步骤组。
• 最后对所有用户的is_in_group求和，约束总和≤k，这才是真正统计步骤组的用户数量。

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