Error: smt.diff_logic: non-diff logic expression

[dreinon]

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).

[tpaviot]

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.

[dreinon]

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!

[dreinon]

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)
)

[dreinon]

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.

[dreinon]

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

[tpaviot]

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

[dreinon]

Overlap_0_7_ae91ddf9 corresponds to the z3 Int created in the Workload constraint https://github.com/tpaviot/ProcessScheduler/blob/2d39619b89f82dc7753c85d788c66f3a38247e1f/processscheduler/resource_constraint.py#L75

Still working in the code

[dreinon]

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()

[tpaviot]

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