y = 1/x, x = 0 실수로 만족? SMT-LIB에서

Question

:

(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}]{}

, /is defined this way in SMT-LIB 반환 해결책이 존재하지 않는 것을 나타내는 빈 목록을 반환한다. 따라서 Z3 또는 CVC4에 관한 한이 문제는 SAT입니다.