模型在普遍量化公式中意味着什么?它是一个函数吗?

Question

考虑以下两个公式:

• Exists y. Forall x. (y>x)，即unsat。
• Forall x. Exists 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持有约束(y>x);例:f(x)=x+1;换句话说，像示例那样的Forall x. Exists 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函数。

• 模型的普遍量化公式或多或少是没有意义的。对于全称量化变量的所有值都成立。只有顶层存在在模型中是有意义的。

• 量词消除在这里起作用;它去掉了整个公式。请注意，QE保留了满意度;所以它完成了它的任务。

• 这是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的按钮解决方法来说太复杂了。