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

Posted 2023-03-28

【中文标题】在 Z3py 的 forall 中定义量词变量问题

【英文标题】：Define quantifier variable issue in forall in Z3py

【发布时间】：2021-02-22 20:26:28

【问题描述】：

以下代码应返回 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)

【参考方案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。