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

Set up

我使用 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")

Question

我需要向模型添加复杂的布尔约束。就像是

(a || b) && (d || e) == g

如何向模型添加这样的复杂布尔约束？

PS:我无法立即在网上找到此信息，但根据我在相关问题上得到的答案找到了解决方案here https://stackoverflow.com/questions/70553100/constraint-optimization-in-python-with-or-tools-how-to-enforce-a-multi-level-co/70554356?noredirect=1#comment124730209_70554356以及另一个人的另一个相关问题here https://stackoverflow.com/questions/27814935/boolean-operations-on-constraints-in-google-or-tools-library。我以问答的形式总结了我的发现，希望它们对某人有用。

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

Output

获得以下输出：

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