python - Setting Binary Constraints with Google OR-tools

Question

I have been using OR-tools, in particular looking at its uses for scheduling. I feel I have grasp on the library now, though there is one aspect of Google's main example ( https://github.com/google/or-tools/blob/master/examples/python/shift_scheduling_sat.py ) that I am having trouble understanding. The function I am having a problem with is: add_soft_sequence_constraint() and the related: negated_bounded_span (relevant code is below).

These are meant to constrain the number of shifts a person can work in a row though I cannot figure out how this is accomplished.

My issues are: What exactly is the result of using .Not()? I am having trouble locating any documentation on it or producing a clear test for it. Why is negated_bounded_space() (a function that depends on .Not()) necessary at all? Finally, in both cases in add_soft_sequence_constraint how does it know the difference between you working one long sequence (ie, 6 shifts in a row) which would not be allowed and 2 shorter sequences (4 shifts, a break, then 3 shifts) which may be allowed but adds up to the same (or more) as the long sequence?

Any help would be great and much appreciated, I would like to be able to use and adapt the code but I feel uncomfortable doing so before properly understanding it.

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() is the negation of a Boolean variable.

See https://en.wikipedia.org/wiki/Boolean_satisfiability_problem.

The main idea is that if you want to forbid a given pattern:

v0 = false, v1 = true, v2 = true, v3 = false

That is a sequence of length 2 starting at position 1, you add a BoolOr specifying that v0 is true, or v1 is false, or v2 is false, or v3 is true.

If any one of these condition is true, then this particular pattern is not present.

This is written as

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

.