使用unsat消除forall

Question

我们知道，我们可以通过这样的话来证明定理的有效性：

let Demorgan(x, y) = formula1(x,y) iff formula2(x,y)
assert ( forall (x,y) . Demorgan(x,y) )

或者，我们可以通过这样说来消除forall量词：

let Demorgan(x, y) = formula1(x,y) iff formula2(x,y)
( assert (not  Demorgan(x,y) ) )

因此，如果它返回unsat值，那么我们可以说上面的公式是有效的。

现在我想用这个想法从下面的断言中去掉forall量词：

assert ( exists x1,x2,x3 st .( forall y . formula1(x1,y) iff
                                          formula2(x2,y) iff
                                          formula3(x3,y) ) )

那么，在Z3中(使用SMT或C++ -LIB2.0)有没有办法断言如下所示：

assert (exists x1,x2,x3 st. ( and ((not ( formula1(x1,y) iff formula2(x2,y) )) == unsat)
                                  ((not ( formula2(x2,y) iff formula3(x3,y) )) == unsat))) 

Answer 1

是的，当我们可以通过证明一个公式的否定是不可满足的来证明它的有效性时。例如，为了证明Forall X. F(X)是有效的，我们只需要证明not (Forall X. F(X))是不可满足的。公式not (Forall X. F(X))等同于(Exists X. not F(X))。公式(Exists X. not F(X))可等同于公式not F(X)，其中绑定变量X被新的常量X替换。所谓可均衡化，我的意思是第一个是可满足的当且仅当第二个是可满足的。这个删除存在量词的步骤通常被称为。请注意，后两个公式是而不是等效项。例如，考虑将X分配给2的解释{ X -> 2 }。在这种解释中，公式Exists X. not (X = 2)的计算结果仍然是true，因为我们可以选择X作为3。另一方面，在这种解释中，公式not (X = 2)的计算结果为false。我们通常使用术语量词消除过程来表示给定公式F生成等价的无量词公式F'的过程。因此，skolemization不被认为是量词消除过程，因为结果不是等价的公式。

也就是说，我们不需要一步一步地应用skolemization。Z3可以为我们做到这一点。这里有一个例子(也可以在here上找到)。

(declare-sort S)
(declare-fun F (S) Bool)
(declare-fun G (S) Bool)
(define-fun Conjecture () Bool 
    (forall ((x S)) (= (and (F x) (G x)) (not (or (not (F x)) (not (G x)))))))
(assert (not Conjecture))
(check-sat)

现在，让我们考虑一个形式为Exists X. Forall Y. F(X, Y)的公式。为了证明这个公式的有效性，我们可以证明否定not Exists X. Forall Y. F(X, Y)是不可满足的。这个否定等价于Forall X. Exists Y. not F(X, Y)。现在，如果对这个公式应用skolemization，我们就得到了Forall X. not F(X, Y(X))。在本例中，绑定变量Y被替换为Y(X)，其中Y是结果公式中的新函数符号。直觉上，函数Y就是“选择函数”。对于每个X，我们可以选择一个不同的值来满足公式F。Z3会自动为我们执行所有这些步骤。我们不需要手动应用skolemization。然而，在这种情况下，结果公式通常更难求解，因为它在skolemization步骤之后包含通用量词。