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実数では満足できないと言う方が数学的に正当化されると思います。FindInstance[Element[x, Reals] && Element[y, Reals] && x == 0 && y == 1/x, {x, y}]Mathematica では、同等のコードは空のリストを返し、解が存在しないことを示します。つまり、{}

それにもかかわらず、/ は SMT-LIB でこのように定義されています。したがって、Z3 または CVC4 に関する限り、この問題は SAT です。