Z3创建两个具有相同元素但顺序不同的intVectors

如何解决Z3创建两个具有相同元素但顺序不同的intVectors

我需要具有相同值的重复Vector，但是重复的顺序不同。 但是我不知道如何设置此约束。

此刻，我正在创建矢量，如下所示：

age = RealVector('age',NUM)
age_med_all = RealVector('age_m_a',NUM)

s.add([age[i] == age_med_all[i] for i in range(NUM)])
s.add([age_med_all[i] <= age_med_all[i + 1] for i in range(NUM - 1)])

因此，实际上我希望对第二个Vector进行排序以将其用于中位数约束，而原始Vector则不需要进行排序。

那么我该如何更改该行以获得age[i] == age_med_all[j]

s.add([age[i] == age_med_all[i] for i in range(NUM)])

我这样尝试过：

for j in range(NUM) :
    s.add(Sum([If(age[i] == age_med_all[j],1,0) for i in range(NUM)]) >= 1)

但是，当我这样做时，两个向量的取值并不相同。

解决方法

最简单的方法是将您的清单转换成包袋，并检查它们是否相等。 （袋子本质上是一个数组，用于存储您在其中存储的每个元素的多样性。）

基于这个想法，下面是一个示例实现：

from z3 import *

s = Solver()

# Working on 10 elements
SIZE = 10

# a is the original arary,sortedA will be the sorted version of it
a       = IntVector('A',SIZE)
sortedA = IntVector('S',SIZE)

# Assert that sortedA is indeed sorted
for i in range(SIZE-1):
    s.add(sortedA[i] <= sortedA[i+1])

# convert them to bags:
bagA = K(IntSort(),0)
bagS = K(IntSort(),0)
for i in range(SIZE):
    bagA = Store(bagA,a[i],1 + Select(bagA,a[i]))
    bagS = Store(bagS,sortedA[i],1 + Select(bagS,sortedA[i]))

# assert that the bags are the same
s.add(bagA == bagS)

# a few constraints to make output interesting. obviously you'll
# have actual constraints,so these won't be needed
s.add(a[3] == 5)    # a fixed element
s.add(a[3] > a[9])  # out-of order

# get and print the model
r = s.check()
if r == sat:
    m = s.model()
    finalA = []
    finalS = []
    for i in range(SIZE):
        finalA.append(m.evaluate(a[i],model_completion=True))
        finalS.append(m.evaluate(sortedA[i],model_completion=True))
    print("A = %s" % finalA)
    print("S = %s" % finalS)
else:
    print("Solver said: %s" % r)

我对代码进行了注释，因此应该易于理解，但是请随时询问是否有任何不清楚的地方。

运行该程序时，我得到：

A = [4,4,5,3,-2,-2]
S = [-2,5]

您可以验证S确实是A的排序版本。 （取决于您的z3版本，随机种子等，您当然可能会得到不同的答案。但是S应该仍然是A的排序版本。）