Z3: странное поведение с нелинейной арифметикой

Question

Я только начинаю использовать Z3 (v4.4.0), и я хотел бы попробовать один из примеров учебника:

(declare-const a Int)
(assert (> (* a a) 3))
(check-sat)
(get-model)

(echo "Z3 will fail in the next example...")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)

Как уже было сказано, во втором примере происходит сбой с "неизвестным", и, повышая уровень многословия (до 3), я думаю, что понимаю, почему: какая-то проблема с упрощением процесса, а затем и тактика. Чтобы иметь лучшее представление о проблеме (и более короткий вывод), я решил удалить первую часть кода, чтобы проверить только неисправную часть:

(echo "Z3 will fail in the next example...")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)

Но волшебным образом, теперь я "сел". Я не уверен в том, как Z3 выбирает свою тактику, когда речь идет о нелинейной арифметике, но может ли проблема заключаться в том, что Z3 выбирает тактику для первой формулы, которая бесполезна для второй?

заранее спасибо

Answer 1

Второе кодирование не эквивалентно первому, отсюда и другое поведение. Вторая кодировка не включает ограничение (assert (> (* a a) 3)), поэтому Z3 может найти удовлетворительным, что b^3 + b*c = 3 для некоторого выбора вещественных чисел b и c. Однако, когда он имеет ограничение, что a^2 > 3 для некоторого целого числа a, он не может найти его выполнимым, даже если два утверждения не зависят друг от друга.

Для этой проблемы, по сути, Z3 по умолчанию не будет использовать нелинейный реальный арифметический решатель (который завершен), когда он встречает вещественные числа, смешанные с целыми числами. Вот пример того, как заставить его использовать qfnra-nlsat (ссылка rise4fun: http://rise4fun.com/Z3/KDRP):

(declare-const a Int)
;(assert (> (* a a) 3))
;(check-sat)
;(get-model)

(echo "Z3 will fail in the next example...")
(declare-const b Real)
(declare-const c Real)
(push)
(assert (and (> (* a a) 3) (= (+ (* b b b) (* b c)) 3.0)))
(check-sat)
(check-sat-using qfnra-nlsat) ; force using nonlinear solver for nonlinear real arithimetic (coerce integers to reals)
(get-model)
(pop)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
(get-model)

Аналогично, если вы просто измените (declare-const a Int) в (declare-const a Real)по умолчанию он выберет правильный решатель, который может с этим справиться. Так что да, по сути это связано с тем, что решатель выбирается, что отчасти определяется видами базовых терминов.

Вопросы и ответы по теме: Объединение нелинейного действительного с линейным Int