vZ - Optimization problems when type casting

[nalpure]

I tried to solve a Teacher Assignment Problem using the vZ extension. I have several constraints and a cost function that needs to be minimized. But the output is clearly not the minimal solution. I know this because of two things: a) When I add a certain constraint (marked in the code), I get a lower result value b) because logically seen either delta_plus or delta_minus should be 0 for each teacher, and the DELTA variable should always be smaller than 1 when optimized

The issue seems to be typecasting from 'Int' to 'Real'. I use this conversion to declare a '/' instead of a 'div' operation. When I change the variables delta_plus and delta_minus to 'Real' and remove the 'ToReal'-conversions, everything works.

Below is my code. I wanted to simplify it, but removing constraints, objective variables or events, teachers, etc. seems to make computation either too time consuming or does not produce the faulty error.

When running without the constrain you will get minimum value 3331.95? When you add the constraint: 3043.64?

More information on what I'm trying to do you can find here: https://stackoverflow.com/questions/71250463/z3-vz-adding-constraint-improves-optimum?noredirect=1#comment126025751_71250463

`

from z3 import *
import time


"""sample input"""

teachers = ['fr', 'hö', 'pf', 'bo', 'jö', 'sti', 'bi', 'la', 'he', 'kl', 'sc', 'str', 'ko', 'ba'] 
events = [i for i in range(5,13)] 
event_overlap_sets = [{5, 6}, {8, 9}, {10, 11}, {11, 12}, {12, 13}] 
desired_workdays = {'fr': 36, 'hö': 50, 'pf': 30, 'bo': 100, 'jö': 80, 'sti': 56, 'bi': 20, 'la': 140, 'he': 5.0, 'kl': 50, 'sc': 38, 'str': 42, 'ko': 20, 'ba': 20} 
event_size = {5: 2, 6: 2, 7: 2, 8: 3, 9: 2, 10: 2, 11: 3, 12: 2} 
event_durations = {5: 5.0, 6: 5.0, 7: 5.0, 8: 16, 9: 7.0, 10: 5.0, 11: 16, 12: 5.0} 

# assignment: (teacher, event, priority, distance)
possible_assignments = [('he', 5, 1, 11), ('sc', 5, 1, 48), ('str', 5, 1, 199), ('ko', 6, 1, 53), ('jö', 7, 1, 317), ('bo', 9, 1, 56), ('sc', 10, 1, 25), ('ba', 11, 1, 224), ('bo', 11, 1, 312), ('jö', 11, 1, 252), ('kl', 11, 1, 248), ('la', 11, 1, 303), ('pf', 11, 1, 273), ('str', 11, 1, 228), ('kl', 5, 2, 103), ('la', 5, 2, 16), ('pf', 5, 2, 48), ('bi', 6, 2, 179), ('la', 6, 2, 16), ('pf', 6, 2, 48), ('sc', 6, 2, 48), ('str', 6, 2, 199), ('sc', 7, 2, 354), ('sti', 7, 2, 314), ('bo', 8, 2, 298), ('fr', 8, 2, 375), ('hö', 9, 2, 95), ('jö', 9, 2, 119), ('sc', 9, 2, 37), ('sti', 9, 2, 95), ('bi', 10, 2, 211), ('hö', 11, 2, 273), ('bi', 12, 2, 408), ('bo', 12, 2, 318), ('ko', 12, 2, 295), ('la', 12, 2, 305), ('sc', 12, 2, 339), ('str', 12, 2, 218)] 


def compute_optimum():

    # key: assignment tuple     value: z3-Bool
    x = {assignment : Bool('e%i_%s' % (assignment[1], assignment[0])) for assignment in possible_assignments}

    delta_plus = {teacher : Int('d+_%s' % teacher) for teacher in teachers}
    delta_minus = {teacher : Int('d-_%s' % teacher) for teacher in teachers}
    DELTA = Real('DELTA')

    opt = Optimize()


    # constraint1: number of teachers needed per event
    num_available_per_event = {event : len(list(filter(lambda assignment: assignment[1] == event, possible_assignments))) for event in events}
    for event in events:
        num_teachers_to_assign = min(event_size[event], num_available_per_event[event])
        opt.add(Sum( [If(x[assignment], 1, 0) for assignment in x.keys() if assignment[1] == event] ) == num_teachers_to_assign)


    for teacher in teachers:
    
        # constraint2: teacher can't work in multiple overlapping events
        for overlapping_events in event_overlap_sets:
            opt.add(Sum( [If(x[assignment], 1, 0) for assignment in x.keys() if assignment[1] in overlapping_events and assignment[0] == teacher] ) <= 1)

        
        # constraint3: delta (absolute over and underload of teacher)
        num_teacher_workdays = Sum( [If(x[assignment], event_durations[assignment[1]], 0) for assignment in x.keys() if assignment[0] == teacher])
        opt.add(delta_plus[teacher] >= 0, delta_minus[teacher] >= 0)
        opt.add(delta_plus[teacher] - delta_minus[teacher] == num_teacher_workdays - desired_workdays[teacher])


        # constraint4: DELTA (maximum relative deviation of wished to assigned workdays)
        opt.add(DELTA >= ToReal(delta_plus[teacher] + delta_minus[teacher]) / desired_workdays[teacher])


    # --------------
    #opt.add(DELTA <= 1)    # ADDING THIS RESULTS IN BETTER OPTIMUM
    # --------------


    average_rel_workday_deviation = Sum( [ToReal(delta_plus[teacher] + delta_minus[teacher]) / desired_workdays[teacher] for teacher in teachers]) / len(teachers)
    overall_distance = Sum( [If(x[assignment], assignment[3], 0) for assignment in x.keys()])
    num_prio2 = Sum( [If(x[assignment], assignment[2]-1, 0) for assignment in x.keys()])
    
    obj_fun = opt.minimize(average_rel_workday_deviation+ DELTA + overall_distance + num_prio2)


    if opt.check() == sat:
        m = opt.model()
        for teacher in teachers:
            print(f"{teacher}: d+ {m.evaluate(delta_plus[teacher])}, d- {m.evaluate(delta_minus[teacher])}")
        print("DELTA:::", m.evaluate(DELTA))
        print("min value:", obj_fun.value().as_decimal(2))

    else:
        print("Not satisfiable")
        return []

start_time = time.time()
compute_optimum()
print("time: ", time.time()-start_time)

`