0

我正在使用 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)

4

1 回答 1

4

您的输入是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大于6？对于这个输入 z3 说：true x

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

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

希望有帮助！

于 2019-12-10T14:45:33.473 回答