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

Question

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

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

除了rise4fun教程页面上提供的内容外，是否有一些简单的FOL公式代码片段可供研究。

(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

由于以下assert，您的输入unsat：

(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))

也就是说，如果x大于6，f a xtrue？对于此输入 z3 说：

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

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

希望对您有所帮助！