如何使用Z3从向量列表中筛选满足约束的向量并求和得到指定结果

错误根因 #

你的报错来源于G_c定义行的for j in R逻辑：R是你定义的Z3符号整数变量数组，不是Python整数常量，无法直接作为元组下标去取Tr_tuple中的元素，Python在执行列表推导时会尝试把符号变量转为整数下标，自然就触发了「R不是合法索引」的报错。

修复思路 #

你需要用Z3的条件判断表达式If来实现「根据R中符号变量的值匹配对应向量的分量」的逻辑，不能直接用Python原生的下标取值。

修复后完整可运行代码 #

from z3 import *

Tr_tuple = ((-1,1,0,1,0,0,0,-1),
      (1,-1,1,0,0,0,-1,0),
      (0,-1,-1,1,0,1,0,0),
      (-1,0,1,-1,0,0,0,0),
      (0,0,0,-1,-1,1,0,1),
      (0,0,-1,0,1,-1,1,0),
      (0,1,0,0,0,-1,-1,1),
      (1,0,0,0,-1,0,1,-1),
      (1,1,-1,-1,1,1,-1,-1), 
      (-1,-1,1,1,-1,-1,1,1))
tr_count = len(Tr_tuple) # 统计可选向量总数

Start_tuple = (1,-1,0,-1,0,0,0,1)
depth = 2

G = [Int('g_%s' % i) for i in range(8)]
R = [Int('r_%s' % i) for i in range(depth)]

# R元素约束：取值范围是Tr_tuple的合法下标
R_c = [ And(R[i] >= 0, R[i] < tr_count) for i in range(depth) ]
# 可选补充约束：要求选中的向量不重复，不需要可以直接注释
# R_c += [ Distinct(R) ]

# 重写G的约束：用If表达式匹配每个r对应的向量分量
G_c = []
for i in range(8):
    total_offset = 0
    for r in R:
        # 每个r对应向量的第i位贡献：r等于k就加Tr_tuple[k][i]，否则加0
        total_offset += sum(If(r == k, Tr_tuple[k][i], 0) for k in range(tr_count))
    G_c.append(G[i] == Start_tuple[i] + total_offset)

# 目标约束：最终G全为0
G_g = [G[i] == 0 for i in range(8)]

# 执行求解
s = Solver()
s.add(R_c + G_c + G_g)
print(s.check())
if s.check() == sat:
    m = s.model()
    # 打印选中的向量下标
    selected = [m[r].as_long() for r in R]
    print("选中的Tr_tuple下标：", selected)
    # 结果验证
    res = list(Start_tuple)
    for idx in selected:
        res = [res[k] + Tr_tuple[idx][k] for k in range(8)]
    print("求和结果：", res)

内容的提问来源于stack exchange，提问作者Jetto