z3 - 使用 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 中有什么方法(使用 C++ API 或 SMT-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)其中绑定(bind)变量X被一个新的常数 X 替换. Equisatisfiable，我的意思是第一个是可满足的，如果第二个是可满足的。这个删除存在量词的步骤通常称为 skolemization .
请注意，最后两个公式是 不是 相等的。
例如，考虑解释 { X -> 2 }分配 X至2 .公式Exists X. not (X = 2)在这个解释中仍然评估为真，因为我们可以选择 X成为 3 .另一方面，公式 not (X = 2)在这种解释中计算为假。
我们通常使用术语量词消除过程来表示给定公式 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)) .在这种情况下，绑定(bind)变量 Y已替换为 Y(X) , 其中 Y是结果公式中的新函数符号。直觉是函数 Y是“选择函数”。对于每个 X ，我们可以选择不同的值来满足公式 F . Z3 会自动为我们执行所有这些步骤。我们不需要手动应用 skolemization。但是，在这种情况下，生成的公式通常更难求解，因为它在 skolemization 步骤之后包含一个全称量词。