or-tools中如何在子数组和约束场景下正确使用OnlyEnforceIf

OR-Tools的CP-SAT求解器中OnlyEnforceIf方法仅接受布尔变量作为参数，你直接传入的线性比较表达式属于BoundedLinearExpression类型，不具备布尔变量特有的Index属性，因此触发报错。

需要先为每个子数组的两种合法状态显式定义对应的布尔变量，再绑定约束关系：

• 为每行定义两个布尔变量，分别对应「行和为0」、「行和大于3」两种合法状态
• 用AddBoolOr约束两种状态必须触发其中一种，满足二选一的需求
• 分别为两种状态绑定对应的数值约束

from ortools.sat.python import cp_model

model = cp_model.CpModel()
# 示例中为4行4列的数组，每个元素取值范围0~2，可根据实际需求调整
n = 4
result = [[model.NewIntVar(0, 2, f'result_{i}_{j}') for j in range(n)] for i in range(n)]
validMinSum = 3

for i in range(n):
    row_sum = sum(result[i])
    # 定义状态变量
    is_zero_sum = model.NewBoolVar(f'is_zero_sum_{i}')
    is_gt3_sum = model.NewBoolVar(f'is_gt3_sum_{i}')
    
    # 约束：两种状态必须有一个成立
    model.AddBoolOr([is_zero_sum, is_gt3_sum])
    
    # 绑定状态和数值约束
    model.Add(row_sum == 0).OnlyEnforceIf(is_zero_sum)
    model.Add(row_sum > validMinSum).OnlyEnforceIf(is_gt3_sum)
    
    # 可选补充：加反向约束避免状态和数值不匹配，提升求解效率
    model.Add(row_sum != 0).OnlyEnforceIf(is_gt3_sum)
    model.Add(row_sum <= validMinSum).OnlyEnforceIf(is_zero_sum)

如果业务逻辑已经可以排除其他非法状态的出现，反向约束可以省略，添加后可减少求解器的搜索空间，加快求解速度。

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