在 Z3py 的 forall 中定义量词变量问题答案

【问题标题】：Define quantifier variable issue in forall in Z3py在 Z3py 的 forall 中定义量词变量问题
【发布时间】：2023-04-03 09:20:01
【问题描述】：

以下代码应返回 z>=15 的 sat。然而，它给了unsat。我认为，量词变量 'y' 必须在 forall 范围内定义。请建议如何做到这一点。

from z3 import *

s = Solver()
s.set(auto_config=False, mbqi=False)

x = Int('x')
y = Int('y')
z = Int('z')

s.add(ForAll([y], Implies(And(y>-5,y<5),And(x==y+z,x>10))))

print(s.check())
m = s.model()
print(m)

【问题讨论】：

标签： z3 z3py

【解决方案1】：

正如您所怀疑的，您所写的并不真正意味着您的意图。您编写的内容选择了 x 的单个值来满足它。相反，您想说的是，可以为y 的每个值选择一些x。所以，只要用那个量化来说明它：

from z3 import *

s = Solver()
s.set(auto_config=False, mbqi=False)

x = Int('x')
y = Int('y')
z = Int('z')

s.add(ForAll([y], Implies(And(y>-5,y<5), Exists([x], And(x==y+z,x>10)))))

print(s.check())
m = s.model()
print(m)

注意x 上的存在。这打印：

sat
[z = 15]

虽然 z3 可以解决此类涉及量化的简单情况，但您应该注意，SMT 求解器通常不擅长使用量词进行推理，尤其是在它们嵌套时。一旦问题变得足够复杂，您可能会开始收到unknown。

【讨论】：