z3 - 如何在python中使用z3求解器获得中值约束

Question

我有不同的向量，我想为不同的中位数设置约束。其中一些中位数是针对向量的不同子集计算的。

例如，我想要一个约束

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

我希望所有 50 岁以上的女性的工资中位数为 50，所有男性的年龄中位数为 40salary > 70

所以我知道如何过滤掉相关数据。

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

我知道如何获得平均值，例如：

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

但是对于中位数，我使用了一个排序列表，所以我可以这样说：

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

但是，我无法对约束进行建模以确保有序的年龄和有序的薪水，因为 person_1 不会是最年轻的并且薪水最低。

因此，我需要按年龄或薪水对所有向量进行时间排序。

标签： z3z3py