Z3Py中如何为列表内声明的布尔变量赋值？

问题原因 #

你编写的循环代码未生效，是因为遍历列表时拿到的i只是临时变量引用，直接给i赋值False仅修改了临时变量的指向，并没有给Z3的符号布尔变量添加对应的取值约束。Z3的符号变量取值是通过求解器约束来定义的，不能像普通Python变量一样直接赋值修改。

正确实现方式 #

首先你需要先创建求解器实例，再给列表中的每个符号变量添加等于True/False的约束即可，示例代码如下：

from z3 import *

# 1. 定义布尔符号变量列表
lk = [Bool("a_0"), Bool("a_1"), Bool("a_2")]
# 2. 实例化求解器
s = Solver()
# 3. 批量添加约束，将所有变量设为False
s.add([var == False for var in lk])

# 验证结果
if s.check() == sat:
    print(s.model())

运行后输出的模型结果为：[a_0 = False, a_1 = False, a_2 = False]，符合预期。

如果需要给单个变量单独赋值，直接按索引取列表元素添加约束即可，比如将a_0设为True：

s.add(lk[0] == True)

注意事项 #

Z3的约束是叠加生效而非覆盖生效的，如果先后给同一个变量添加两个相反的取值约束，求解器会返回unsat（无满足解）。

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