使用 Z3 检查一阶公式的可满足性

Question

我正在使用 Z3 尝试一些基本的 FOL 公式可满足性问题。我无法理解为什么下面的代码 sn-p 返回 Unsat。请帮忙。

如果可能的话，如果有人尝试使用带有量词的 FOL 给出“Sat”并且通过一些小的细微更改给出“Unsat”作为输出的示例，将会非常有帮助

除了rise4fun教程页面提供的以外，是否有一些简单的FOL公式代码sn-ps可以学习。

(set-option :smt.mbqi true)
(declare-fun f (Real Real) Bool)
(declare-const a Real)
(declare-const b Real)

(assert (forall ((x Real)) (and (f a x) (> x 6))))
(assert (and (f a b) (> b 6) ))
(check-sat)

Answer 1

您的输入是unsat，因为这个assert：

(assert (forall ((x Real)) (and (f a x) (> x 6))))

右边是连词。所以这就是说所有真正的x 值都大于 6，这显然不是真的。事实上，您可以将整个输入简化为：

(assert (forall ((x Real)) (> x 6)))
(check-sat)

出于完全相同的原因，它仍然是unsat。

也许你的意思是这样的：

(set-option :smt.mbqi true)
(declare-fun f (Real Real) Bool)
(declare-const a Real)
(declare-const b Real)

(assert (forall ((x Real)) (=> (> x 6) (f a x))))
(assert (and (f a b) (> b 6) ))
(check-sat)
(get-value (f a b))

即f a x是true 如果 x大于6？对于这个输入 z3 说：

sat
((f (lambda ((x!1 Real) (x!2 Real)) (= x!2 0.0)))
 (a 0.0)
 (b 7.0))

你可以看到这确实是一个令人满意的模型，虽然不是一个特别有趣的模型。

希望有帮助！