OrTools CP-SAT固定变量后模型不可行原因咨询

导致模型返回不可行的核心原因通常分为以下两类：

1. 变量y的类型或值域设置错误 #

• 若y被定义为布尔变量（BoolVar）：布尔变量仅能取0或1，但当x=1时，y=-5*x的计算结果为-5，完全超出布尔变量的合法取值范围，直接导致模型无解。
• 若y被定义为整数变量（IntVar）但值域未包含负数：比如你给y设置的范围是[0, N]，当x=1时y=-5超出值域限制，模型自然不可行。

2. 约束定义的潜在疏漏（若y的设置正确） #

如果y是值域包含-5的整数变量，理论上当z取0时，model.Add(y < 0).OnlyEnforceIf(z.Not())会生效（满足y=-5<0），而model.Add(y >= 0).OnlyEnforceIf(z)因z=0不触发，模型应该可行。若此时仍返回不可行，大概率是代码存在以下疏漏：

• 错误固定了z的取值（比如强制z=1）；
• 定义y=-5*x时误用语法，导致x和y的关联约束未正确生效（比如Python中误用赋值符号=而非约束符号==）。

from ortools.sat.python import cp_model

model = cp_model.CpModel()
x = model.NewBoolVar('x')
# 给y设置包含-5的合理值域
y = model.NewIntVar(-5, 0, 'y')
z = model.NewBoolVar('z')

# 正确定义x和y的线性约束
model.Add(y == -5 * x)
# 添加条件约束
model.Add(y >= 0).OnlyEnforceIf(z)
model.Add(y < 0).OnlyEnforceIf(z.Not())
# 固定x=1
model.Add(x == 1)

solver = cp_model.CpSolver()
status = solver.Solve(model)
print(f"求解状态: {solver.StatusName(status)}")
print(f"z的取值: {solver.Value(z)}")
print(f"y的取值: {solver.Value(y)}")

这段代码会返回可行解，z=0，y=-5，符合预期。

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