python - 使用 Google OR-tools 设置二元约束

Question

我一直在使用 OR 工具，特别是研究它在调度方面的用途。我觉得我现在已经掌握了这个库，尽管谷歌的主要示例( https://github.com/google/or-tools/blob/master/examples/python/shift_scheduling_sat.py )的一个方面我无法理解。我遇到问题的函数是:add_soft_sequence_constraint() 和相关的:neated_bounded_span(相关代码如下)。

这些旨在限制一个人可以连续工作的轮类次数，尽管我不知道这是如何实现的。

我的问题是:使用 .Not() 的结果到底是什么？我无法找到有关它的任何文档或为其生成清晰的测试。为什么 neated_bounded_space() (依赖于 .Not() 的函数)是必要的？最后，在 add_soft_sequence_constraint 的两种情况下，它如何知道您工作一个不允许的长序列(即连续 6 个类次)和 2 个较短的序列(4 个类次、一个休息时间)之间的区别，然后 3 个轮类)，这可能是允许的，但加起来与长序列相同(或更多)？

任何帮助都会非常好，非常感谢，我希望能够使用和调整代码，但在正确理解它之前这样做我感到不舒服。

def negated_bounded_span(works, start, length):
    sequence = []
    # Left border (start of works, or works[start - 1])
    if start > 0:
        sequence.append(works[start - 1])
    for i in range(length):
        sequence.append(works[start + i].Not())
    # Right border (end of works or works[start + length])
    if start + length < len(works):
        sequence.append(works[start + length])
    return sequence

def add_soft_sequence_constraint(model, works, hard_min, soft_min, min_cost,
                                 soft_max, hard_max, max_cost, prefix):

    # Forbid sequences that are too short.
    for length in range(1, hard_min):
        for start in range(len(works) - length - 1):
            model.AddBoolOr(negated_bounded_span(works, start, length))


    # Just forbid any sequence of true variables with length hard_max + 1
    for start in range(len(works) - hard_max - 1):
        model.AddBoolOr(
            [works[i].Not() for i in range(start, start + hard_max + 1)])

Answer 1

Not() 是 bool 变量的求反。

参见https://en.wikipedia.org/wiki/Boolean_satisfiability_problem.

主要思想是，如果你想禁止给定的模式:

v0 = 假，v1 = 真，v2 = 真，v3 = 假

这是一个从位置 1 开始的长度为 2 的序列，您添加一个 BoolOr 指定 v0 为 true，或 v1 为 false，或 v2 为 false，或 v3 为 true。

如果这些条件中的任何一个为真，则该特定模式不存在。

这写成

BoolOr([v0, v1.Not(), v2.Not(), v3])

.