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

Question

我需要一个具有相同值但副本具有不同顺序的重复向量。 但是我不知道如何设置这个约束。

目前我正在创建如下向量：

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)])

所以实际上我希望对第二个向量进行排序以将其用于中值约束，而无需对原始向量进行排序。

那么我怎样才能以某种方式更改该行以获得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)

但是，当我这样做时，两个向量不会包含相同的值。

Answer 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, 4, 5, 3, 5, 3, -2, 3, -2]
S = [-2, -2, 3, 3, 3, 4, 4, 4, 5, 5]

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