如何解决如何在python中使用z3求解器获取中值约束
我有不同的向量,要为不同的中位数设置约束。 计算矢量的不同子集的一些中位数。
例如,我想要一个约束
age = IntVector('age',10)
male = BoolVector('male',10)
salary = IntVector('salary',NUM)
我希望所有50岁以上的女性的薪水中位数为50,而所有salary > 70
的男性的薪水中位数为40
所以我知道如何过滤掉相关数据。
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不会是年龄最小且薪水最低的人,因此我无法对确保年龄和薪水的约束进行建模。
所以我需要按年龄或薪水对所有向量进行时间排序。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。