Я изучаю процедуры принятия решений и, с другой стороны, также изучаю Z3. В частности, я исследую различные разрешимые фрагменты теории массивов первого порядка.
Например, в статье [1] представлен ∃∗∀∗
фрагмент массивов, для которых мы можем доказать свойства: например, ∀i . 0 ≤ i < n → a[i+1] = a[i]−1
. Однако они устанавливают разрешимость этой логики, следуя теоретико-автоматному подходу, через определение нового класса автоматов Бюхи со счетчиками. Мне это кажется далеким от классических исключений кванторов, которые, как я понимаю, реализованы в SMT-решателях как процедуры принятия решений для разрешимых теорий с кванторами.
Таким образом, мой вопрос заключается в следующем: если доказана разрешимость теории, как в статье [1], реализует ли Z3 (и другие решатели) эти процедуры принятия решений? Другими словами, решается ли запрос ∀i . 0 ≤ i < n → a[i+1] = a[i]−1
с помощью завершающей процедуры принятия решения в Z3 или использует более эффективную, но полуразрешимую эвристику? В случае использования завершающих процедур, как Z3 (и остальные) идентифицируют разрешимый фрагмент? Может быть, с языковой идентификацией с использованием формальных грамматик?
[1] Что еще можно решить о целочисленных массивах? https://hal.archives-ouvertes.fr/hal-01418914/document
Как и любое крупное программное обеспечение, z3 представляет собой набор алгоритмов, реализованных за многие годы. Таким образом, может быть трудно точно определить, какие алгоритмы реализованы и как они взаимодействуют; особенно учитывая, что он также активно развивается. Итак, чтобы ответить на ваш вопрос с какой-либо властью, вам нужно спросить реальных разработчиков. https://github.com/Z3Prover/z3/discussions лучший форум для этого; stack-overflow вряд ли даст вам удовлетворительный ответ.
Другая вещь, которую нужно сделать, это посмотреть на исходный код. Поскольку это открытый исходный код, вы можете сами увидеть, как он устроен. Хотя это не для случайных конечных пользователей, похоже, ваш интерес идет глубже; так что вы могли бы лучше ознакомиться с тем, как все это устроено.
Мое личное мнение таково, что это похоже на любой другой программный проект. Акцент делается на правильности с целью (но обязательно целью) полноты. Хорошая работа над практическими проблемами, с которыми сталкиваются люди в промышленности, важнее, чем реализация теоретической процедуры принятия решений, которая работает ужасно с точки зрения производительности. (Итак, здесь в игру вступают эвристики. Распознавание и переписывание паттернов в надежде, что может быть достигнут unsat
результат. Теория битовых векторов — хороший пример этого: легко просто взорвать бит и бросить его в Решатель SAT, но z3 очень старается переписать и сделать другую «магию», чтобы можно было укротить вычислительную сложность; с разной степенью успеха.) Но все это «кухонная» сторона вещей. Чтобы получить точные ответы, попробуйте форум z3-discussions, и, надеюсь, один из реальных разработчиков даст вам более точный ответ.
Я не знаю ни одного документа, в котором эти системы сравниваются в деталях. Такое сравнение было бы крайне сложно составить по целому ряду причин. Но тоже было бы интересно почитать.
Большое спасибо! Я задам тот же вопрос на форуме Z3; как вы сказали, я не буду задавать общий вопрос, а только то, какая именно процедура решения используется для этого фрагмента. Кроме того, я бы больше углубился в Z3, но моя проблема в том, что я точно не знаю его отличий от Yices, dReal и т. д., поэтому тратить слишком много времени может быть контрпродуктивно :)