y=1/x, x=0 在实数中可满足? [英] y=1/x, x=0 satisfiable in the reals?

问题描述

在 SMT-LIB 中:

In SMT-LIB:

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

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

Should this model be SAT or UNSAT?

推荐答案

在 SMT-LIB 2.0 和 2.5 中，所有功能都是全部，所以这个例子是 SMT-LIB 中的 SAT.Z3 和 CVC4 确实为问题中的示例返回 SAT.

In SMT-LIB 2.0 and 2.5, all functions are total, so this example is SAT in SMT-LIB. Both Z3 and CVC4 do indeed return SAT for the example in the question.

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

I found this counter-intuitive. I think it would be mathematically more well justified to say that y=1/x, x=0 is unsatisfiable in the reals. In Mathematica, the equivalent code returns an empty list, indicating that no solution exists, i.e., FindInstance[Element[x, Reals] && Element[y, Reals] && x == 0 && y == 1/x, {x, y}] returns {}

尽管如此，/ 在 SMT-LIB 中是这样定义的.所以就Z3或CVC4而言，这个问题就是SAT.

Nonetheless, / is defined this way in SMT-LIB. So as far as Z3 or CVC4 are concerned, this problem is SAT.

这篇关于y=1/x, x=0 在实数中可满足?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！