CP-SAT create a bool variable which represents whether a sum of variables is greater than 0

Question

I have this piece of code in which im trying to make a variable teacher_doesnt_work that represents if Sum(classes_by_teacher[t] is 0 or not.

classes_by_teacher = {}
for t in all_teachers:
    cur_classes = []
    for d in all_days:
        for p in all_day_parts:
            for g in all_groups:
                for s in all_subjects:
                    cur_classes.append(classes[(t, d, p, g, s)])
    classes_by_teacher[t] = cur_classes

teacher_i_doesnt_work = []

for t in all_teachers:
    teacher_works_n_times = model.NewIntVar(0,10000, f"How many times does  {t} work").Sum(classes_by_teacher[t])
    teacher_doesnt_work = model.NewBoolVar(f"teacher {t} does not work")
    model.Add(teacher_doesnt_work == (teacher_works_n_times == 0))
    
    teacher_i_doesnt_work.append(teacher_doesnt_work)

model.Maximize(sum(teacher_i_doesnt_work))

it as expected gives me this error, is there some workaround this?

File ~/notebook/jupyterenv/lib/python3.8/site-packages/ortools/sat/python/cp_model.py:412, in LinearExpr.__eq__(self, arg)
    410     return BoundedLinearExpression(self, [arg, arg])
    411 else:
--> 412     return BoundedLinearExpression(self - arg, [0, 0])

File ~/notebook/jupyterenv/lib/python3.8/site-packages/ortools/sat/python/cp_model.py:334, in LinearExpr.__sub__(self, arg)
    332 if cmh.is_zero(arg):
    333     return self
--> 334 return _Sum(self, -arg)

TypeError: bad operand type for unary -: 'BoundedLinearExpression'

Answer 1

I suggest reading this section of the doc on channeling

The solution will use 2 linear equations with OnlyEnforceIf() extensions.