使用 Google OR 工具设置二元约束

Question

我一直在使用 OR 工具，特别是在查看它在调度方面的用途。我觉得我现在已经掌握了这个库，尽管 Google 的主要示例 ( https://github.com/google/or-tools/blob/master/examples/python/shift_scheduling_sat.py ) 有一个方面我无法理解。我遇到问题的功能是：add_soft_sequence_constraint() 和相关的：negated_bounded_span（相关代码在下面）。

这些是为了限制一个人可以连续工作的轮班次数，但我不知道这是如何实现的。

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

如果能提供任何帮助，我将不胜感激，我希望能够使用和改编代码，但在正确理解代码之前这样做我感到不舒服。

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() 是布尔变量的否定。

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

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

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

即从位置1开始长度为2的序列，你加一个BoolOr指定v0为真，或v1为假，或v2为假，或v3为真。

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

这写成

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

.

Answer 2

详细说明Laurent的回答：

如果您想在长度为 4 的列表中避免长度为 2 的序列：

[1,1,0,0] -> BoolOr[v0.Not(),v1.Not(),v2]
[0,1,1,0] -> BoolOr[v0, v1.Not(), v2.Not(), v3]
[0,0,1,1] -> BoolOr[v1, v2.Not(), v3.Not()]

我也开了一期Githubhttps://github.com/google/or-tools/issues/1399，作为行

for start in range(len(works) - length - 1):

可能有误

长度为 4 且 hard min 为 3 的列表的小示例：

from ortools.sat.python import cp_model


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


if __name__ == '__main__':
    model = cp_model.CpModel()
    works = [model.NewBoolVar(f'{i}') for i in range(4)]
    for length in range(1, 3):
        print(f'Length {length}')
        for start in range(len(works) - length + 1):
            print(negated_bounded_span(works, start, length))

Returns 类似于：

Length 1
[0.Not(), 1(0..1)]
[0(0..1), 1.Not(), 2(0..1)]
[1(0..1), 2.Not(), 3(0..1)]
[2(0..1), 3.Not()]
Length 2
[0.Not(), 1.Not(), 2(0..1)]
[0(0..1), 1.Not(), 2.Not(), 3(0..1)]
[1(0..1), 2.Not(), 3.Not()]

使用 Google OR 工具设置二元约束

Setting Binary Constraints with Google OR-tools

python

or-tools