Z3(Python)求解逻辑公式时报错Invalid bounded variables问题求助

错误根源 #

你触发报错的核心原因是量词绑定变量的参数格式不符合Z3要求：

• Z3的ForAll、Exists量词的第一个入参要求是单个Z3变量，或是平铺的变量序列，不能是嵌套列表
• 你的代码中e_vars = [a, b, c, d]本身已经是变量列表，又在传入ForAll时额外套了一层方括号，变成了[[a,b,c,d]]嵌套结构；同理s_vars = [v]传入Exists时也套了额外的方括号变成[[v]]，Z3无法识别嵌套列表内的变量，因此抛出绑定变量无效的错误。

你刻意设置的空列表neg_lts没有问题，Z3中And([])会默认返回True常量，不会触发该报错。

修复方案 #

去掉量词参数外层多余的方括号即可，修复后的可运行代码如下：

from z3 import *

v, a, b, c, d, e = Ints('v a b c d e') 

lt_1 = (v == 4)
lt_2 = (v == 2)
lt_3 = (v == 3)
lt_4 = (v == 5)
lt_5 = (v == 0)
lt_6 = (v >= 0)
lt_7 = (v <= 4)

s_vars = [v]
e_vars = [a, b, c, d]
pos_lts = [lt_1, lt_2, lt_3, lt_4, lt_5, lt_6, lt_7]
neg_lts = []
posNeg_Conjunction = And(And(pos_lts), And(neg_lts))
# 去掉ForAll参数外层的方括号
universal = ForAll(e_vars, (posNeg_Conjunction))

# 去掉Exists参数外层的方括号
pol_phi = Exists(s_vars, universal)
solve(pol_phi)

额外说明 #

修复后运行会返回unsat，这是你的逻辑本身的问题：pos_lts中同时包含v==4、v==2、v==3等互斥的约束，不存在能满足所有约束的v值，属于逻辑合理性问题，和代码语法无关。
你后续调整的无ForAll版本也按同样规则修改Exists的入参即可正常运行。

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