CP-SAT模型报错MODEL_INVALID：除数跨零问题求助

你的问题核心是CP-SAT的AddDivisionEquality要求分母变量的整个取值范围不能包含0——哪怕你添加了denom > 0的约束，如果分母变量的初始定义域包含0，求解器在搜索过程中仍会尝试这个取值，导致MODEL_INVALID错误。以下是几种可行的解决方法：

方法1：直接限制分母变量的下界为1 #

既然denom是布尔变量x1+x2+x3的和，其可能取值为0、1、2、3，我们可以在创建denom变量时直接将下界设为1，彻底排除0的可能性：

# 直接定义denom的取值范围为1到3，而非默认的0到3
denom = model.NewIntVar(1, 3, "denom")
model.Add(denom == x1 + x2 + x3)
model.Add(num == a1*x1 + a2*x2 + a3*x3)
model.AddDivisionEquality(division, num, denom)
model.Minimize(division)

如果denom已经提前创建，也可以通过约束强制其下界为1：

model.Add(denom >= 1)  # 对整数变量，>=1等价于>0，但能明确排除0的取值

方法2：用乘法约束替代除法约束 #

绕开AddDivisionEquality，直接通过乘法建模除法关系，这样无需依赖求解器对分母定义域的严格检查：

• 如果是实数除法（division为实数变量）：

model.Add(division * denom == num)
model.Add(denom >= 1)
model.Minimize(division)

• 如果是整数除法（向下取整）：
  需要额外引入余数变量来满足整数除法的定义：

remainder = model.NewIntVar(0, 2, "remainder")  # 余数最大为denom-1，denom最小为1，最大为3
model.Add(num == division * denom + remainder)
model.Add(remainder < denom)
model.Add(denom >= 1)
model.Minimize(division)

方法3：使用逻辑蕴含约束（复杂场景适用） #

如果你的场景中denom存在为0的可能性但已通过其他约束排除，可以用逻辑蕴含确保仅当denom>=1时除法等式生效：

model.AddImplication(denom >= 1, division * denom == num)
model.Add(denom >= 1)
model.Minimize(division)

不过对于你的问题，方法1或2已经足够简洁有效。

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