Error: smt.diff_logic: non-diff logic expression

Hi!
Sometimes, when I add too many resources (workers), I get the following error:

(smt.diff_logic: non-diff logic expression (<= (+ |{example_worker_task_name}_start|  #  {example_worker_task_name} is a placeholder for the example
Reason: smt tactic failed to show goal to be sat/unsat (incomplete (theory difference-logic))

It gets solved when I run the problem with one less worker (it doesn't have to be the worker that the error specified in order for the error to get solved).

You mean there should be a kind of maximum in the number of workers? Never met this issue, feel free to post a code snippet.

Hi! We found the problem has more to be with the number of tasks added to the problem. Since removing a worker reduced the number of tasks, it gets solved that way, but it we have found it also gets solved reducing the number of tasks of a couple workers with the same number of workers. I'm working in a minimum example that reproduces the error.
Thanks!

I turned out that the log wasn't complete.
This is the actual log, which seems to say that an expression that's supossed to be >= 0 isn't:

(
  smt.diff_logic: non-diff logic expression 
  (<=
    (+ |{first_worker_added_to_the_problem_task_name}_start|
       (* (- 1) |{first_worker_added_to_the_problem_task_name}_end|)
       (ite Overlap_0_7_ae91ddf9!126 1 0)
    )
  0)
)

I have been researching about SMTLIB functions and terms syntax and I interpret that what that expression means (in Pythony lang) is the following:

# Note: QF_UFIDL stands for Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols

##### The meaning of the expression is:
# The following expression does not belong to QF_UFIDL logics and therefore we can't solve the problem:
(
  {first_worker_added_to_the_problem_task_name}_start
  - {first_worker_added_to_the_problem_task_name}_end
  + (1 if Overlap_0_7_ae91ddf9!126 else 0)
) <= 0

I have just tried without specifying the logics and the problem ends, but I don't know how increasing or decreasing the number of tasks has to do with this haha.

The problem might be the * (-1) (whatever) part, I've found '*' symbols are not allowed : https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_UFLIA

Interesting feedback, the python code itself is important to trace the issue, at the end we can post a ticket to the Z3 issue tracker

Overlap_0_7_ae91ddf9 corresponds to the z3 Int created in the Workload constraint

ProcessScheduler/processscheduler/resource_constraint.py

Line 75 in 2d39619

"Overlap_%i_%i_%s"

Still working in the code

Code snippet:

import processscheduler as ps

# NOTE:
# - If supervisor is removed (comment lines with (*) in the code), the problem has a solution.
# - Conflict between my custom constraint and the WorkLoad constraint, if any of them is removed, the problem has a solution.

# Combinations that don't give solution:
# - NUM_TASKS_PER_WORKER = 1 and NUM_REGULAR_WORKERS > 30
# - NUM_TASKS_PER_WORKER = 2 and NUM_REGULAR_WORKERS > 16
# - NUM_TASKS_PER_WORKER = 3 and NUM_REGULAR_WORKERS > 11
# - NUM_TASKS_PER_WORKER = 4 and NUM_REGULAR_WORKERS > 8
# - NUM_TASKS_PER_WORKER = 5 and NUM_REGULAR_WORKERS > 6
# - NUM_TASKS_PER_WORKER = 6 and NUM_REGULAR_WORKERS > 5
# - NUM_TASKS_PER_WORKER = 7,8 and NUM_REGULAR_WORKERS > 4
# - NUM_TASKS_PER_WORKER = 9-11 and NUM_REGULAR_WORKERS > 3
# - NUM_TASKS_PER_WORKER = 12-17 and NUM_REGULAR_WORKERS > 2
# - NUM_TASKS_PER_WORKER > 18 and NUM_REGULAR_WORKERS > 1
combinations = {
    '1': (1, 31),
    '2': (2, 17),
    '3': (3, 12),
    '4': (4, 9),
    '5': (5, 7),
    '6': (6, 6),
    '7-8': (7, 5),
    '9-11': (9, 4),
    '12-17': (12, 3),
    '18+': (18, 2),
}
NUM_TASKS_PER_WORKER, NUM_REGULAR_WORKERS = combinations['1']


def main():
    pb = ps.SchedulingProblem('ManyTasksErrorExample', horizon=40)

    workers = [ps.Worker(f'worker{i}') for i in range(NUM_REGULAR_WORKERS)]
    supervisor_worker = ps.Worker('supervisor')  # (*)

    def get_list_of_tasks(worker_name: str):
        return [ps.FixedDurationTask(f'task_{worker_name}_{i}', 1, optional=True) for i in range(NUM_TASKS_PER_WORKER)]

    period = (0, 10)

    def if_task_starts_in_period_ends_in_period_constraint(period, task):
        # If a task starts in the period, then it must end in the period
        cause = ps.and_([period[0] <= task.start, task.start < period[1]])
        consecuences = [task.end <= period[1]]
        return ps.implies(cause, consecuences)

    for worker in workers:
        for task in get_list_of_tasks(worker.name):
            # Add require resources
            task.add_required_resource(supervisor_worker)  # (*)
            task.add_required_resource(worker)

            # Add custom constraint for period
            pb.add_constraint(if_task_starts_in_period_ends_in_period_constraint(period, task))

        # Don't let anyone do more than 3 tasks in period
        ps.WorkLoad(worker, {period: 3}, kind='max')

    solver = ps.SchedulingSolver(pb, max_time=900, logics='QF_UFIDL')

    if not (solution := solver.solve()):
        print('No solution found')
        return

    solution.render_gantt_matplotlib()


if __name__ == '__main__':
    main()

The QF_UFIDL logics is not suitable for that problem, just remove it.