CP-SAT求解器中AddMaxEquality与OnlyEnforceIf是否不兼容？

是的，目前OR-Tools的CP-SAT求解器中，AddMaxEquality这类全局约束无法直接和OnlyEnforceIf结合使用，这会触发MODEL_INVALID错误。

解决办法 #

你可以手动拆解AddMaxEquality的逻辑，将其转化为一组普通约束，再为这些约束添加OnlyEnforceIf条件。

以你的代码为例，z = max(0, y)（y是布尔变量）等价于z = y，可以替换为如下代码：

from ortools.sat.python import cp_model

model = cp_model.CpModel()

x = model.NewBoolVar('x')
y = model.NewBoolVar('y')
z = model.NewBoolVar('z')

# 替换原有的AddMaxEquality + OnlyEnforceIf逻辑
model.Add(z == y).OnlyEnforceIf(x)
model.Minimize(1)

solver = cp_model.CpSolver()
status = solver.Solve(model=model)

if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
    print(f'x {solver.Value(x)}, y {solver.Value(y)}, z {solver.Value(z)}')
elif status == cp_model.INFEASIBLE:
    print("Infeasible")
elif status == cp_model.MODEL_INVALID:
    print("Model invalid")
else:
    print(status)

如果是更通用的场景（比如max的参数是多个整数变量），可以按以下逻辑拆解：
假设要实现z = max(a1, a2, ..., an)且仅当x为真时生效：

• 对每个变量ai，添加z >= ai，并加上.OnlyEnforceIf(x)
• 为每个ai创建一个布尔变量bi，添加约束z <= ai + M*(1 - bi)（M为足够大的常数，确保超过所有ai的可能取值范围），并加上.OnlyEnforceIf(x)
• 添加约束sum(bi) == 1，并加上.OnlyEnforceIf(x)

这样就能模拟出z等于所有ai中最大值的逻辑，且仅在x为真时生效。

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