Блог

Мне нужно иметь дубликат вектора с теми же значениями, но дубликат с другим порядком. Однако я не знаю, как установить это ограничение.

На данный момент я создаю векторы следующим образом:

 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)
  

однако, когда я делаю это так, два вектора не имеют одинаковых значений.

Самый простой способ сделать это — преобразовать ваши списки в пакеты и проверить, что они равны друг другу. (Пакет — это, по сути, массив, в котором хранится кратность каждого элемента, который вы храните в нем.)

Основываясь на этой идее, вот пример реализации:

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