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

Question

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

标签： z3z3py

Answer 1

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

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结果。