如何在OR-Tools CP-SAT中实现排除0的AllDifferent约束？

要实现「允许多个0，但所有非0决策变量值唯一」的约束，可通过以下两种方式实现：

方法一：布尔变量+两两约束 #

为每个变量创建布尔标记，标识其是否为非0值，再对任意一对变量添加约束：若两者均非0，则值必须不同。

from ortools.sat.python import cp_model as cp

model = cp.CpModel()
x = [model.NewIntVar(lb=0, ub=10, name=f"x_{i}") for i in range(5)]

# 固定x[0]、x[1]为0
model.Add(x[0] == 0)
model.Add(x[1] == 0)

# 为每个变量创建布尔变量，标记是否非0
is_non_zero = []
for i in range(len(x)):
    b = model.NewBoolVar(f"non_zero_{i}")
    model.Add(x[i] > 0).OnlyEnforceIf(b)
    model.Add(x[i] == 0).OnlyEnforceIf(b.Not())
    is_non_zero.append(b)

# 添加非0变量互异约束
for i in range(len(x)):
    for j in range(i + 1, len(x)):
        model.Add(x[i] != x[j]).OnlyEnforceIf([is_non_zero[i], is_non_zero[j]])

# 最大化x的和
model.Maximize(sum(x))

# 求解并输出结果
solver = cp.CpSolver()
status = solver.Solve(model)
if status == cp.OPTIMAL:
    solution = [solver.Value(var) for var in x]
    print(f"最优解：{solution}")
    print(f"总和：{solver.ObjectiveValue()}")
else:
    print("未找到最优解")

方法二：辅助变量+AllDifferent约束 #

通过辅助变量将0值映射为唯一的占位符，再对所有辅助变量施加AllDifferent约束，间接保证非0变量值唯一。此方法效率更高，适合变量数量较多的场景。

from ortools.sat.python import cp_model as cp

model = cp.CpModel()
x = [model.NewIntVar(lb=0, ub=10, name=f"x_{i}") for i in range(5)]
n = len(x)
ub_x = 10

# 固定x[0]、x[1]为0
model.Add(x[0] == 0)
model.Add(x[1] == 0)

# 创建辅助变量y：非0时与x值相同，0时取唯一占位符（避免冲突）
y = []
for i in range(n):
    y_i = model.NewIntVar(lb=0, ub=ub_x + n, name=f"y_{i}")
    # x非0时，y等于x
    model.Add(y_i == x[i]).OnlyEnforceIf(x[i] > 0)
    # x为0时，y取唯一占位符（ub_x+1到ub_x+n）
    model.Add(y_i == ub_x + 1 + i).OnlyEnforceIf(x[i] == 0)
    y.append(y_i)

# 约束所有辅助变量互异
model.AddAllDifferent(y)

# 最大化x的和
model.Maximize(sum(x))

# 求解并输出结果
solver = cp.CpSolver()
status = solver.Solve(model)
if status == cp.OPTIMAL:
    solution = [solver.Value(var) for var in x]
    print(f"最优解：{solution}")
    print(f"总和：{solver.ObjectiveValue()}")
else:
    print("未找到最优解")

两种方法运行后均可得到预期解[0, 0, 8, 9, 10]，总和为27。

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