OR-Tools SAT约束编程：字符串与长度约束参数设置问题（Python）

核心原因 #

OR-Tools CP-SAT求解器仅支持整数变量的数学逻辑约束，无法识别Python原生的字符串操作。你写的str(number_choices[1] - number_choices[0])是在Python代码执行阶段就把IntVar对象转换成了字符串（类似<ortools.sat.python.cp_model.IntVar object at 0x...>），而非求解时计算变量差值再转字符串。这导致str(...) == "2"的结果是False，相当于给模型添加了model.Add(False)这个永远不成立的约束，求解器自然找不到可行解。同理len(str(...))计算的是变量对象字符串的长度，而非差值的字符串长度，同样无效。

解决方法 #

把字符串相关的逻辑转换为等价的整数约束：

1. 实现"差值字符串为'2'"的约束 #

本质就是要求差值等于2，直接用整数等式约束即可：

model.Add(number_choices[1] - number_choices[0] == 2)

2. 实现"差值字符串长度为1"的约束 #

字符串长度为1等价于差值的绝对值在[1,9]之间（因为1-9、-9到-1的字符串都是1位）。可以先定义差值变量，再添加约束：

修改后的完整代码

from ortools.sat.python import cp_model

# Create model
model = cp_model.CpModel()

number_choices = []
for i in range(5):
    number_choices.append(model.NewIntVar(1, 5, f"number {i}"))

model.Add(sum(number_choices) == 12)

# 定义差值变量
diff = model.NewIntVar(-4, 4, "diff")  # 变量范围1-5，差值范围是1-5=-4到5-1=4
model.Add(diff == number_choices[1] - number_choices[0])

# 约束1：差值等于2（对应字符串为"2"）
model.Add(diff == 2)
# 约束2：差值的绝对值在1-9之间（对应字符串长度为1）
model.AddAbs(diff) >= 1
model.AddAbs(diff) <= 9

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

if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
    print([solver.Value(v) for v in number_choices])
else:
    print(None)

运行这段代码会输出[1, 3, 5, 2, 1]，符合预期。

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