Всегда ли Z3 (и другие решатели) используют завершающие процедуры принятия решений, когда это возможно?

Я изучаю процедуры принятия решений и, с другой стороны, также изучаю 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

Структурированный массив Numpy
Структурированный массив Numpy
Однако в реальных проектах я чаще всего имею дело со списками, состоящими из нескольких типов данных. Как мы можем использовать массивы numpy, чтобы...
T - 1Bits: Генерация последовательного массива
T - 1Bits: Генерация последовательного массива
По мере того, как мы пишем все больше кода, мы привыкаем к определенным способам действий. То тут, то там мы находим код, который заставляет нас...
Что такое деструктуризация массива в JavaScript?
Что такое деструктуризация массива в JavaScript?
Деструктуризация позволяет распаковывать значения из массивов и добавлять их в отдельные переменные.
0
0
54
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Как и любое крупное программное обеспечение, z3 представляет собой набор алгоритмов, реализованных за многие годы. Таким образом, может быть трудно точно определить, какие алгоритмы реализованы и как они взаимодействуют; особенно учитывая, что он также активно развивается. Итак, чтобы ответить на ваш вопрос с какой-либо властью, вам нужно спросить реальных разработчиков. https://github.com/Z3Prover/z3/discussions лучший форум для этого; stack-overflow вряд ли даст вам удовлетворительный ответ.

Другая вещь, которую нужно сделать, это посмотреть на исходный код. Поскольку это открытый исходный код, вы можете сами увидеть, как он устроен. Хотя это не для случайных конечных пользователей, похоже, ваш интерес идет глубже; так что вы могли бы лучше ознакомиться с тем, как все это устроено.

Мое личное мнение таково, что это похоже на любой другой программный проект. Акцент делается на правильности с целью (но обязательно целью) полноты. Хорошая работа над практическими проблемами, с которыми сталкиваются люди в промышленности, важнее, чем реализация теоретической процедуры принятия решений, которая работает ужасно с точки зрения производительности. (Итак, здесь в игру вступают эвристики. Распознавание и переписывание паттернов в надежде, что может быть достигнут unsat результат. Теория битовых векторов — хороший пример этого: легко просто взорвать бит и бросить его в Решатель SAT, но z3 очень старается переписать и сделать другую «магию», чтобы можно было укротить вычислительную сложность; с разной степенью успеха.) Но все это «кухонная» сторона вещей. Чтобы получить точные ответы, попробуйте форум z3-discussions, и, надеюсь, один из реальных разработчиков даст вам более точный ответ.

Большое спасибо! Я задам тот же вопрос на форуме Z3; как вы сказали, я не буду задавать общий вопрос, а только то, какая именно процедура решения используется для этого фрагмента. Кроме того, я бы больше углубился в Z3, но моя проблема в том, что я точно не знаю его отличий от Yices, dReal и т. д., поэтому тратить слишком много времени может быть контрпродуктивно :)

Theo Deep 05.10.2022 17:11

Я не знаю ни одного документа, в котором эти системы сравниваются в деталях. Такое сравнение было бы крайне сложно составить по целому ряду причин. Но тоже было бы интересно почитать.

alias 05.10.2022 17:20

Другие вопросы по теме