z3 - y=1/x, x=0 实数可满足？

Question

在 SMT-LIB 中：

(declare-fun y () Real)
(declare-fun x () Real)
(assert (= 0.0 x))
(assert (= y (/ 1.0 x)))
(check-sat)

这个模型应该是 SAT 还是 UNSAT？

Answer 1

在 SMT-LIB 2.0 和 2.5 中，所有功能都是总计的，所以这个例子是 SMT-LIB 中的 SAT。对于问题中的示例，Z3 和 CVC4 确实都返回了 SAT。

我发现这违反直觉。我认为从数学上说，这在实数中y=1/x, x=0是不可满足的。在 Mathematica 中，等价代码返回一个空列表，表示不存在解，即FindInstance[Element[x, Reals] && Element[y, Reals] && x == 0 && y == 1/x, {x, y}]返回{}

尽管如此，/ 在 SMT-LIB 中以这种方式定义。所以就Z3或CVC4而言，这个问题是SAT。