Example for Ldrygala how to negate an AND using CP-SAT in python

ldrygala.py

from ortools.sat.python import cp_model


def x_is_outside_range(model, x, i, D):
    """Returns a boolean literal that is True if (x > i OR x <= i - D)."""
    # 1. Create the boolean that represents the final state
    is_outside = model.new_bool_var(f'outside_{i}_{D}')

    # 2. Define the two possible ways to be 'outside'
    too_high = model.new_bool_var('too_high')
    too_low = model.new_bool_var('too_low')

    # x > i
    model.add(x > i).only_enforce_if(too_high)
    model.add(x <= i).only_enforce_if(too_high.Not())

    # x <= i - D
    model.add(x <= i - D).only_enforce_if(too_low)
    model.add(x > i - D).only_enforce_if(too_low.Not())

    # 3. Logic: is_outside <=> (too_high OR too_low)
    # If is_outside is True, one of the conditions must be True
    model.add_bool_or([too_high, too_low]).only_enforce_if(is_outside)
    # If is_outside is False, both conditions must be False
    model.add_implication(~is_outside, ~too_high)
    model.add_implication(~is_outside, ~too_low)

    return is_outside


def main():
    model = cp_model.CpModel()

    N = 10
    D = 3

    x = model.new_constant(2)
    slots = []
    for i in range(N+1):
        neg = x_is_outside_range(model, x, i, D)

        slot_i = model.new_bool_var(f"busySlot{i}")
        model.add_implication(~neg, slot_i)
        model.add_implication(neg, ~slot_i)

        slots.append(slot_i)

    solver = cp_model.CpSolver()
    status = solver.solve(model)

    # Checks and prints the output.
    if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
        print(f"x = {solver.value(x)}")
        for slot in slots:
            print(f"{slot}: {solver.value(slot)}")
    elif status == cp_model.INFEASIBLE:
        print("The model is infeasible")
    else:
        print("Something went wrong. Please check the status and the log")


main()

zoutput.md

Potential output using last ortools python package

$ python3 -m venv plop
$ source plop/bin/activate
$ pip install ortools
$ ./ldrygala.py
x = 2
busySlot0: 0
busySlot1: 0
busySlot2: 1
busySlot3: 1
busySlot4: 1
busySlot5: 0
busySlot6: 0
busySlot7: 0
busySlot8: 0
busySlot9: 0
busySlot10: 0