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

Question

我需要一个具有相同值但顺序不同的副本 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)

然而，当我这样做时，这两个向量不包含相同的值。

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 的排序版本。）

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

Z3 create two intVectors with same elements but different order

z3

z3py