如何使用 Z3 符号变量索引 Python 列表？

Question

我正在尝试了解 Python 使用 SymbolicWalk 对符号变量进行索引。这是一个我无法继续的小片段：

from z3 import *

s = Solver()

Buckets = [3, 2, 5, 1, 4]

B_Weights = [7.3, 5.7, 4.25, 3.77, 6.02] # Weight of each bucket

B = len(Buckets)

pick = 3

X =[Int('B%d' % b) for b in range (pick)]

def pickBuckets(p):
    return Or([p == r for r in Buckets])

for p in range(pick):
    s.add(pickBuckets(X[p]))
    
# ------Calculate the weights of the picked buckets----
def SymbolicWalk(i, lst_B, lst_W, k):
#     Walk through B_Weights[i](lst_W[i]) and return the weight of the ith bucket

def SymbolicChoice(lst_B, lst_W):
#     select the index of X[p] in Buckets(lst_B) as i

def index(i, lst_B, lst_W):
    return SymbolicWalk(i, lst_B, lst_W, SymbolicChoice)

total_weight = 0
for p in range(pick):
    total_weight = total_weight + index(X[p], Buckets, B_Weights)
    
s.add(total_weight>15)
    

while s.check() == sat:
    m = s.model()
    picked = []
    for i in X:
        picked += [m[i]]

    print(picked)
    s.add(Or([p != v for p, v in zip(X, picked)]))

我应该选择 X[p] 中选择的每个桶的索引，然后从列表 B_Weights 中提取其权重。例如，如果X[p]==5，那么它应该提取4.25。上述示例的一种解决方案是：

[3, 1, 4]

这个问题可能是一种非常简单的符号行走形式，但我仍在努力弄清楚它能解决更复杂的问题。

Answer 1

这是一个简单得多的问题，您可以简单地通过迭代值对并适当地添加权重来解决：

from z3 import *

s = Solver()

Buckets   = [  3,   2,    5,    1,    4]
B_Weights = [7.3, 5.7, 4.25, 3.77, 6.02]

pick = 3
X = [Int('B%d' % b) for b in range (pick)]

s.add(Distinct(X))

total_weight = 0
for p in range(pick):
    s.add(Or([X[p] == b for b in Buckets]))
    total_weight = total_weight + sum([If(b == X[p], w, 0) for (b, w) in zip (Buckets, B_Weights)])

s.add(total_weight>15)

for s in all_smt(s, X):
   print(s)

其中 all_smt 来自

当运行时，会产生：

[B0 = 2, B2 = 4, B1 = 1]
[B0 = 3, B2 = 1, B1 = 4]
[B0 = 1, B2 = 2, B1 = 4]
[B0 = 5, B2 = 2, B1 = 4]
[B0 = 4, B2 = 2, B1 = 1]
[B0 = 4, B2 = 5, B1 = 2]
[B0 = 4, B2 = 2, B1 = 5]
[B0 = 4, B2 = 2, B1 = 3]
...

加上一堆满足约束的其他解决方案。

请注意，我添加了 s.add(Distinct(X)) 以确保您不会两次选择同一个桶。通常，您可能希望确保 X 中的所有元素也已排序。（即，选择 4-2-3 与 2-3-4 相同。）如果是这种情况，您可以在单独的循环中对 X 添加有序约束以减少解决方案。

如何使用 Z3 符号变量索引 Python 列表？

How to index a Python list with a Z3 Symbolic variable?

python

z3

z3py