Я попытался решить 2 ^ x = 4 с помощью Z3, разместив на веб-сайте Z3 следующее: https://rise4fun.com/z3/tutorial.
(declare-const x Real)
(declare-const y Real)
(declare-const z Real)
(assert (=(^ 2 x) 4))
(check-sat)
(get-model)
Z3 произведено
unknown
(model
)
Я неправильно использую Z3?
Задачи, связанные с экспонентами, обычно недоступны для z3 или решателей SMT общего назначения. Это не значит, что они не могут их решить: теория вещественных чисел разрешима. Но у них может не быть правильной эвристики, чтобы ответить на каждый запрос, включающий экспоненты, такие как sat/unsat. Вы можете выполнить поиск в stack-overflow по таким ключевым словам, как nnf, non-linear и т. д., чтобы увидеть множество вопросов, касающихся запросов, содержащих такие сложные термины.
Сказав это, есть отдельное направление исследований, называемое дельта-выполнимостью, которое может в значительной степени помочь с такого рода проблемами. Обратите внимание, что дельта-выполнимость отличается от обычной выполнимости. Это означает, что либо формула выполнима, либо ее дельта-возмущение. Самый известный такой решатель — dReal, и вы можете прочитать о нем здесь: http://dreal.github.io/
На ваш вопрос dReal говорит:
[urfa]~/qq>dreal a.smt2
delta-sat with delta = 0.001
(model
(define-fun x () Real [2, 2])
(define-fun y () Real [-0.0005, 0.0005])
(define-fun z () Real [-0.0005, 0.0005])
)
(На самом деле вы не использовали y и z в своем запросе, поэтому вы можете игнорировать эти выходные данные.)
Как видите, dReal определяет, что x должно быть в диапазоне [2, 2], то есть должно быть 2. Но он также говорит delta-sat with delta = 0.001: Это означает, что он обеспечил правильность этого фактора. (Вы можете настроить коэффициент самостоятельно, сделав его сколь угодно малым, но не равным нулю.) Когда у вас возникают проблемы, связанные с физическими системами, дельта-спутник — правильный выбор для их моделирования в мире SMT.
