CP-SAT | OR-Tools：如何声明两数组至多一组含真值的约束？

需求回顾 #

需要约束布尔变量数组arr1和arr2，禁止arr1至少有一个True且arr2至少有一个True的情况，允许以下场景：

• 单个数组存在多个True（另一数组全为False）
• 两组数组均无True

你提供的布尔实现方案是可行的 #

你的第二段代码完全符合需求，理由如下：

1. 对于arr1_at_least_one：
   • for i in arr1: model.add_implication(i, arr1_at_least_one)：只要arr1中有任意一个元素为True，arr1_at_least_one必须为True
   • model.add_at_least_one(arr1).only_enforce_if(arr1_at_least_one)：如果arr1_at_least_one为True，arr1中至少有一个元素为True
   • 两者结合，实现了arr1_at_least_one与OR(arr1)的等价关系
2. 同理，arr2_at_least_one等价于OR(arr2)
3. model.add_at_most_one(arr1_at_least_one, arr2_at_least_one)：直接禁止两个变量同时为True，完美对应NAND(OR(arr1), OR(arr2))的逻辑

更简洁的实现方案 #

可以利用CP-SAT的原生等价约束进一步简化代码，减少冗余：

方案1：直接关联等价关系 #

# 创建布尔变量表示数组是否存在至少一个True
or_arr1 = model.new_bool_var("or_arr1")
or_arr2 = model.new_bool_var("or_arr2")

# 建立等价关系：or_arr1 等价于 arr1中至少一个True
model.add_equivalence(or_arr1, model.new_bool_var_from_bool_or(arr1))
# 建立等价关系：or_arr2 等价于 arr2中至少一个True
model.add_equivalence(or_arr2, model.new_bool_var_from_bool_or(arr2))

# 添加核心约束：如果or_arr1为True，则or_arr2必须为False（反之同理）
model.add_implication(or_arr1, ~or_arr2)

方案2：无中间变量的直接约束 #

甚至可以省略中间变量，直接表达NOT (OR(arr1) AND OR(arr2))的逻辑：

# 逻辑等价于：OR( arr1全为False, arr2全为False )
model.add_bool_or([
    model.new_bool_var_from_bool_and([~a for a in arr1]),
    model.new_bool_var_from_bool_and([~b for b in arr2])
])

方案3：更高效的成对约束（适合小规模数组） #

如果数组规模不大，也可以直接对所有元素对添加约束：

# 只要arr1中有一个元素为True，arr2中所有元素必须为False
for a in arr1:
    for b in arr2:
        model.add_implication(a, ~b)

这种方式无需额外布尔变量，但数组规模较大时会生成大量约束，性能不如前两种方案。

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