如何在Z3中操作变量列表，实现批量定义、求最大值、去重约束

1. 批量定义变量 #

直接生成变量名列表后传入z3.Ints即可，无需手动逐个声明变量：

# 示例：批量定义20个Int变量，命名为x0~x19
var_count = 20
var_names = ' '.join([f'x{i}' for i in range(var_count)])
vars = z3.Ints(var_names)
# 后续通过下标访问变量，vars[0]对应x0，vars[1]对应x1，以此类推

如果需要定义其他类型变量，将z3.Ints替换为z3.Reals/z3.Bools即可。

2. 变量列表求解最大值 #

用functools.reduce将二元最大值判断逻辑迭代作用到整个变量列表即可：

from functools import reduce

def z3_max(x, y):
    return z3.If(x >= y, x, y)

# 求vars列表所有变量的最大值
max_val = reduce(z3_max, vars)
# 可直接基于最大值加约束，比如要求最大值小于10
s.add(max_val < 10)

3. 批量生成去重约束 #

遍历变量列表生成每个变量不等于当前模型取值的条件，全部传入z3.Or即可：

while s.check() == z3.sat:
    model = s.model()
    print(model)
    # 批量生成排除当前模型的约束
    block = z3.Or([var != model[var] for var in vars])
    s.add(block)

完整可运行示例 #

import z3
from functools import reduce

def z3_max(x, y):
    return z3.If(x >= y, x, y)

# 可自定义变量数量
VAR_COUNT = 20

# 批量定义变量
var_names = ' '.join([f'x{i}' for i in range(VAR_COUNT)])
vars = z3.Ints(var_names)
s = z3.Solver()

# 示例约束：所有变量大于0，变量和为100
s.add(z3.Sum(vars) == 100)
s.add([v > 0 for v in vars])

# 最大值约束：所有变量最大值小于20
max_val = reduce(z3_max, vars)
s.add(max_val < 20)

# 迭代求解+自动去重
while s.check() == z3.sat:
    model = s.model()
    print(model)
    block = z3.Or([v != model[v] for v in vars])
    s.add(block)

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