如何在 CP-SAT 中指定条件约束

Question

我想添加形式的约束

a - b > 0 如果 c + d == 4

documentation 谈论 OnlyEnforceIf 我希望允许

model.Add(a-b > 0).OnlyEnforceIf(c+d==4)

不幸的是，OnlyEnforceIf 似乎只能采用单个布尔值，而不能采用诸如 c+d==4 之类的条件。如果我正在正确阅读文档，它会继续建议

model.Add(c+d==4).OnlyEnforceIf(b)
model.Add(c+d!=4).OnlyEnforceIf(b.Not())
model.Add(a-b > 0).OnlyEnforceIf(b)

我有两个问题：

谁能解释一下这个公式的逻辑。如果第一个条件应该读作“if b then c+d == 4. if not b then c+d != 4. if b then a-b > 0”那么逻辑似乎不正确。我希望约束是 a-b>0 if c+d==4 所以它肯定是“if c+d==4 then b”不应该？
我有很多这些约束需要施加，所以我似乎需要创建很多新变量。我注意到，例如，在 CPLEX 中，您可以直接指定 if-then 而无需创建新变量。我错过了什么吗？

Answer 1

我们分解一下(c+d == 4) <=> b
1. b => (c+d == 4)加上model.Add(c+d==4).OnlyEnforceIf(b)
2. (c+d == 4) => b 的 contrapositive 是 not(b) => not(c+d == 4) 并且用 model.Add(c+d!=4).OnlyEnforceIf(b.Not())
ortools 的理念是他们不想像 CPLEX 那样在幕后创建变量。 Reference

How to specify conditional constraints in CP-SAT