设置
我正在使用 google OR 工具作为约束编程求解器：
from ortools.sat.python import cp_model
我已经定义了以下 BoolVars
model = cp_model.CpModel()
a = model.NewBoolVar("a")
b = model.NewBoolVar("b")
c = model.NewBoolVar("c")
d = model.NewBoolVar("d")
e = model.NewBoolVar("e")
f = model.NewBoolVar("f")
g = model.NewBoolVar("g")
问题
我需要为模型添加一个复杂的布尔约束。就像是
(a || b) && (d || e) == g
如何将这样的复杂布尔约束添加到模型中？
PS：我无法立即在网上找到此信息，但根据我在这里的一个相关问题和另一个人的另一个相关问题的答案找到了解决方案。我在这里以问答方式总结了我的发现，希望它们对某人有用。
这种约束不能立即添加到模型中。约束需要在其组件（和 & 或门）中拆分。每个基本组件都需要设置为等于一个新的 BoolVar。然后将它们组合起来以添加最终约束。
分解为基本组件
我们将按如下方式进行：
(a || b) == c
(d || e) == f
(c && f) == g
最后一个方程等价于原始方程：
(a || b) && (d || e) == g
在新的 BoolVars 中存储基本约束
可以使用以下函数评估“OR”类型的方程：
def evaluate_or(a, b, c):
# Either a or b or both must be 1 if c is 1.
model.AddBoolOr([a, b]).OnlyEnforceIf(c)
# The above line is not sufficient, as no constraints are defined if c==0 (see reference documentation of
# "OnlyEnforceIf". We therefore add another line to cover the case when c==0:
# a and b must both be 0 if c is 0
model.AddBoolAnd([a.Not(), b.Not()]).OnlyEnforceIf([c.Not()])
类似地，可以使用以下函数评估“AND”类型的方程：
def evaluate_and(a, b, c):
# Both a and b must be 1 if c is 1
model.AddBoolAnd([a, b]).OnlyEnforceIf(c)
#What happens if c is 0? This is still undefined thus let us add another line:
# Either a or b or both must be 0 if c is 0.
model.AddBoolOr([a.Not(), b.Not()]).OnlyEnforceIf(c.Not())
在这种特定情况下，基本约束是两次或门。我们将它们存储在 c 和 f 中：
evaluate_or(a, b, c)
evaluate_or(d, e, f)
添加复杂约束
这现在非常简单，可以使用上一步中的 BoolVars 和 AND 门来完成：
evaluate_and(c, f, g)
讨论
可以使用中间 BoolVars 以及上面定义的 OR 和 AND 门函数添加任何复杂的约束。只需将约束分解为其基本组成部分。
完整程序
这是完整的程序：
from ortools.sat.python import cp_model
model = cp_model.CpModel()
a = model.NewBoolVar("a")
b = model.NewBoolVar("b")
c = model.NewBoolVar("c")
d = model.NewBoolVar("d")
e = model.NewBoolVar("e")
f = model.NewBoolVar("f")
g = model.NewBoolVar("g")
def evaluate_or(a, b, c):
# Either a or b or both must be 1 if c is 1.
model.AddBoolOr([a, b]).OnlyEnforceIf(c)
# The above line is not sufficient, as no constraints are defined if c==0 (see reference documentation of
# "OnlyEnforceIf". We therefore add another line to cover the case when c==0:
# a and b must both be 0 if c is 0
model.AddBoolAnd([a.Not(), b.Not()]).OnlyEnforceIf([c.Not()])
def evaluate_and(a, b, c):
# Both a and b must be 1 if c is 1
model.AddBoolAnd([a, b]).OnlyEnforceIf(c)
#What happens if c is 0? This is still undefined thus let us add another line:
# Either a or b or both must be 0 if c is 0.
model.AddBoolOr([a.Not(), b.Not()]).OnlyEnforceIf(c.Not())
#Add the constraints
evaluate_or(a, b, c)
evaluate_or(d, e, f)
evaluate_and(c, f, g)
# Solve the model.
solver = cp_model.CpSolver()
solver.parameters.enumerate_all_solutions = True
status = solver.Solve(model, cp_model.VarArraySolutionPrinter([a, b, c, d, e, f, g]))
输出
获得以下输出：
Solution 0, time = 0.00 s
a = 0 b = 0 c = 0 d = 1 e = 0 f = 1 g = 0
Solution 1, time = 0.00 s
a = 0 b = 0 c = 0 d = 1 e = 1 f = 1 g = 0
Solution 2, time = 0.00 s
a = 0 b = 0 c = 0 d = 0 e = 1 f = 1 g = 0
Solution 3, time = 0.00 s
a = 0 b = 0 c = 0 d = 0 e = 0 f = 0 g = 0
Solution 4, time = 0.00 s
a = 0 b = 1 c = 1 d = 0 e = 0 f = 0 g = 0
Solution 5, time = 0.00 s
a = 0 b = 1 c = 1 d = 1 e = 0 f = 1 g = 1
Solution 6, time = 0.00 s
a = 0 b = 1 c = 1 d = 1 e = 1 f = 1 g = 1
Solution 7, time = 0.00 s
a = 0 b = 1 c = 1 d = 0 e = 1 f = 1 g = 1
Solution 8, time = 0.00 s
a = 1 b = 1 c = 1 d = 0 e = 1 f = 1 g = 1
Solution 9, time = 0.00 s
a = 1 b = 1 c = 1 d = 1 e = 1 f = 1 g = 1
Solution 10, time = 0.00 s
a = 1 b = 1 c = 1 d = 1 e = 0 f = 1 g = 1
Solution 11, time = 0.00 s
a = 1 b = 1 c = 1 d = 0 e = 0 f = 0 g = 0
Solution 12, time = 0.00 s
a = 1 b = 0 c = 1 d = 0 e = 0 f = 0 g = 0
Solution 13, time = 0.00 s
a = 1 b = 0 c = 1 d = 0 e = 1 f = 1 g = 1
Solution 14, time = 0.00 s
a = 1 b = 0 c = 1 d = 1 e = 1 f = 1 g = 1
Solution 15, time = 0.00 s
a = 1 b = 0 c = 1 d = 1 e = 0 f = 1 g = 1