How to get median constraint with z3 solver in python

Viewed 301

I got different vectors where I want to set constraints for different medians. Where some medians are calculated for different subsets of the vector.

Eg, I want a constraint for

    age = IntVector('age', 10)
    male = BoolVector('male', 10)
    salary = IntVector('salary', NUM)

where I want a salary median of 50 for all female aged greater 50 and an age median of 40 for all male with salary > 70

So I know how to filter out the relevant data.

    If(And(male[i] == False, age[i] > 50)

I know how to get the mean eg:

    Sum([If(And(male[i] == False, salary[i] > 50), age[i], 0) for i in range(10)]) / (10 - NUM_MALE) == 50

however for the median I kneed a sorted list so I can say something like:

    (age[4] + age[5])/2 = MEAN

However, I cannot model a constraint to ensure the ordered age AND ordered salary, since person_1 will not be the youngest AND have the least salary.

So I would need to have a temporal ordering for all my vectors by either age or salary.

0 Answers
Related