Google OR 工具：如何评估复杂或多级布尔约束

Question

设置

我使用 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：我无法立即在网上找到此信息，但根据我在此处的相关问题和此处另一个人的另一个相关问题上得到的答案找到了解决方案。我以问答的形式总结了我的发现，希望它们对某人有用。

Answer 1

这种约束不能立即添加到模型中。约束需要分解为其组件（和 & 或门）。每个基本组件需要设置为等于一个新的 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