如何在OR-Tools CP-SAT中用布尔变量标识整数变量的区间归属

核心逻辑 #

要创建布尔变量标识整数变量x是否处于[low, high]区间内，本质是让布尔变量x_in_range满足：

• 当low ≤ x ≤ high时，x_in_range = 1
• 否则，x_in_range = 0

在OR-Tools CP-SAT中，需通过双向约束关联两者状态——因为CP-SAT的约束是单向推导，所以要分别处理两种方向的逻辑。

正确实现代码 #

from ortools.sat.python import cp_model

def get_var_value(solver, var):
    return solver.Value(var)

model = cp_model.CpModel()
solver = cp_model.CpSolver()

# 定义整数变量x，范围0到100
x = model.NewIntVar(0, 100, 'x')
# 定义布尔变量，标识x是否在5到10之间
x_is_between_5_and_10 = model.NewBoolVar('x_is_between_5_and_10')

# 测试用例：强制x等于7
model.Add(x == 7)

# 方向1：如果布尔变量为1，则x必须在[5,10]区间内
model.Add(x >= 5).OnlyEnforceIf(x_is_between_5_and_10)
model.Add(x <= 10).OnlyEnforceIf(x_is_between_5_and_10)

# 方向2：如果x在[5,10]区间内，则布尔变量必须为1
# 先将整数约束转换为布尔变量状态
x_ge_5 = model.NewBoolVar('x_ge_5')
x_le_10 = model.NewBoolVar('x_le_10')
model.Add(x >= 5).OnlyEnforceIf(x_ge_5)
model.Add(x < 5).OnlyEnforceIf(x_ge_5.Not())
model.Add(x <= 10).OnlyEnforceIf(x_le_10)
model.Add(x > 10).OnlyEnforceIf(x_le_10.Not())

# 关联区间状态与目标布尔变量
model.Add(x_is_between_5_and_10 == 1).OnlyEnforceIf([x_ge_5, x_le_10])
model.Add(x_is_between_5_and_10 == 0).OnlyEnforceIf(x_ge_5.Not())
model.Add(x_is_between_5_and_10 == 0).OnlyEnforceIf(x_le_10.Not())

# 求解并输出结果
status = solver.Solve(model)
print('x的值:', get_var_value(solver, x))
print('x是否在5-10之间:', get_var_value(solver, x_is_between_5_and_10))

关键说明 #

• 单向约束的局限性：CP-SAT的OnlyEnforceIf仅支持单向推导，因此必须分别处理"布尔变量为1时x在区间内"和"x在区间内时布尔变量为1"两种逻辑。
• 辅助布尔变量：直接将5<=x这类整数约束作为OnlyEnforceIf的参数是错误的，必须先将整数约束转换为对应的布尔变量状态，再通过布尔逻辑关联。
• 简洁写法：OR-Tools提供AddBoolAnd、AddImplication等工具函数，可更简洁地表达复合布尔条件。

原代码问题说明 #

你提供的原代码中，model.Add(x_is_between_5_and_10 == 1).OnlyEnforceIf(5 <= x).OnlyEnforceIf(x <= 10)存在错误：OnlyEnforceIf的参数必须是布尔变量，而非直接的整数约束（如5<=x），因此无法正确触发约束。需先将整数约束转换为布尔变量后再关联。

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