z3 - 模型在通用量化公式中意味着什么？它是一个函数吗？

Question

考虑这两个公式:

• 存在 y。福尔X. (y>x)，这是unsat。
• 对于所有 x。存在 y。 (y>x)，即 sat。

请注意，我们无法找到 sat 公式的“模型”，例如，对于以下代码，使用 Z3 会输出 Z3Exception: model is not available:

phi = ForAll([x],Exists([y], lit))

s_def = Solver()
s_def.add(phi)
print(s_def.model())

此外，量词消除不会输出消除，而是输出可满足性结果 [[]](即True):

x, y = Reals('x, y')

t = Tactic("qe")

lit = (y>x)

ae = Goal()
ae.add(ForAll([x],Exists([y], lit)))
ae_qe = t(ae)

print(ae_qe)

我认为发生这种情况是因为 y 的值完全取决于 x (例如，如果 x 是 5 > 那么y 可以是6)。因此，我有几个问题:

• 我的这种解释正确吗？
• “通用量化公式的模型”是什么意思？
• 我们是否说公式接受量词消除，即使它从未消除量词，但“仅:评估为 True 或 False？
• 有没有办法合成或构造一个模型/函数来表示持有约束(y>x)的y；例如f(x)=x+1。换句话说，删除 Forall x. 的量词是否有意义？存在 y。 Phi(x,y) 就像示例中的那样 Forall x。 Phi(x,f(x))？

Answer 1

您得到模型不可用，因为您没有调用check。模型仅在调用 check 后才可用。试试这个:

from z3 import *

x, y = Ints('x y')

phi = ForAll([x], Exists([y], y > x))

s = Solver()
s.add(phi)
print(s.check())
print(s.model())

打印:

sat
[]

现在，您是正确的，当您拥有全称量词时，您将不会获得有意义/有帮助的模型；因为模型将取决于每种情况下 x 的选择。 (您只能获取顶级存在值的值。)这就是模型被打印为空列表的原因。

旁注在某些情况下，您可以使用 skolemization 技巧( https://en.wikipedia.org/wiki/Skolem_normal_form )来摆脱嵌套的存在并获得映射函数，但这并不能并不总是使用 SMT 求解器，因为它们只能构建“有限”skolem 函数。 (对于您的示例，不存在这样的有限函数；即可以编写为输入案例分析或 if-then-else 链的函数。) 对于您的具体问题:

• 是的； y 的值取决于 x，因此无法按原样显示。有时 skolemization 可以让您解决这个问题，但 SMT 求解器只能构建有限的 skolem 函数。

• 通用量化公式的模型或多或少是没有意义的。对于通用量化变量的所有值都是如此。只有顶层存在在模型中才有意义。

• 量词消除在这里确实有效；它摆脱了整个公式。请注意，量化宽松保持了可满足性；所以它已经完成了它的工作。

• 这是 skolem 函数。正如您所指出的，这个 skolem 函数不是有限的(不能写成具体值上的有限 if-then-else 链)，因此现有的 SMT 求解器无法为您找到/打印它们。如果您尝试，您会发现求解器只是循环:

from z3 import *

x = Int('x')

skolem = Function('skolem', IntSort(), IntSort())
phi = ForAll([x], skolem(x) > x)

s = Solver()
s.add(phi)
print(s)
print(s.check())
print(s.model())

不幸的是，上面的内容永远不会终止。对于 SMT 解决的按钮式方法来说，此类问题实在太复杂了。