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中，所有功能都是total的，所以这个例子是SMT-LIB中的SAT。对于问题中的示例，Z3 和 CVC4 确实 return SAT。

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

尽管如此，/ is defined this way in SMT-LIB。所以对于Z3或者CVC4来说，这个问题就是SAT

y=1/x, x=0 在实数中可满足吗？

y=1/x, x=0 satisfiable in the reals?

smt

z3

cvc4