В SMT-LIB:
(declare-fun y () Real)
(declare-fun x () Real)
(assert (= 0.0 x))
(assert (= y (/ 1.0 x)))
(check-sat)
Должна ли эта модель быть SAT или UNSAT?
y=1/x, x=0 выполнимо в реалах?
Ответы (1)
В SMT-LIB 2.0 и 2.5 все функции являются общими, поэтому этот пример — SAT в SMT-LIB. И 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.
person
Douglas B. Staple
schedule
29.06.2016
Да, именно так SMT определяет эти операторы/функции. Повторяющаяся тема, у которой всегда ровно 50% сторонников и 50% противников :)
- person Christoph Wintersteiger; 29.06.2016
Большое спасибо Кристоф. Я столкнулся с этим, пытаясь выяснить, должен ли
(and (= y (^ x 0.5)) (< x 0.0)) быть SAT или UNSAT. Для согласованности с остальной частью SMT я думаю, что этот пример sqrt также должен быть SAT. Теперь мне просто нужно выяснить, как заставить Z3 фактически выдать SAT для этого примера sqrt.
- person Douglas B. Staple; 29.06.2016
