在Python的Google OR-Tools CP-SAT中创建自定义差值约束的问询

核心原则 #

CP-SAT求解器中，所有参与约束计算的中间值必须是CP变量（即IntVar/BoolVar等），不能用普通Python变量存储——普通变量是静态值，而CP变量是求解过程中动态确定的对象，两者无法直接混用构建数组或计算。

具体解决方案 #

1. 创建差值对应的CP变量

对每对需要计算绝对值差的变量，先创建一个新的IntVar来存储差值结果，再用求解器提供的AddAbsEquality约束关联原变量和差值变量：

from ortools.sat.python import cp_model

model = cp_model.CpModel()
# 假设X1、X2是已定义的CP变量，取值范围0-100
X1 = model.NewIntVar(0, 100, "X1")
X2 = model.NewIntVar(0, 100, "X2")

# 创建存储abs(X1-X2)的CP变量
max_possible_diff = 100  # 根据变量取值范围设定
delta = model.NewIntVar(0, max_possible_diff, "delta_X1_X2")
model.AddAbsEquality(delta, X1 - X2)

# 将所有差值变量存入数组（数组元素全是CP变量）
deltas = [delta]
# 重复上述步骤添加其他差值，比如abs(X3-X4)
X3 = model.NewIntVar(0, 100, "X3")
X4 = model.NewIntVar(0, 100, "X4")
delta2 = model.NewIntVar(0, max_possible_diff, "delta_X3_X4")
model.AddAbsEquality(delta2, X3 - X4)
deltas.append(delta2)

2. 基于差值数组添加计数类约束

以“统计差值大于5的数量等于3”为例，有两种实现方式：

• 方式一：布尔变量标记+求和约束
  先为每个差值变量创建布尔变量，标记是否满足条件，再约束布尔变量的和等于目标计数：

  bool_vars = []
  target_count = 3
  threshold = 5
  
  for d in deltas:
      # 创建布尔变量，d>5时为True，否则为False
      b = model.NewBoolVar(f"is_gt_{threshold}_{d.Name()}")
      model.Add(d > threshold).OnlyEnforceIf(b)
      model.Add(d <= threshold).OnlyEnforceIf(b.Not())
      bool_vars.append(b)
  
  # 约束满足条件的差值数量等于target_count
  model.Add(sum(bool_vars) == target_count)
  

• 方式二：直接使用AddCount全局约束
  如果OR-Tools版本支持，可直接用AddCount约束统计符合取值范围的变量数量：

  # 统计deltas中取值在[6, 100]（即>5）的数量等于3
  model.AddCount(deltas, [6, 100], [target_count])
  

关于“是否必须转化为数学表达式” #

是的。CP-SAT求解器仅能识别基于其自身变量的约束逻辑（等式、不等式、全局约束等），所有业务逻辑都需要转化为求解器可处理的约束表达式，不能用普通Python的条件判断、循环计算等逻辑直接操作CP变量——因为这些变量在求解完成前没有确定的数值。

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