Любое сравнение между различными решателями SMT?

У меня есть реализация на Python, в которой используется доказательство теорем. Я хотел бы знать, есть ли возможность ускорить часть решения SMT, которая в настоящее время использует Z3.

Я пытаюсь найти разные решатели и нашел cvc4/cvc5 и Yices как решатели множественной теории (арифметика, равенство, битвекторы...). Я также нашел dReal и MetiTarski (этот, кажется, устарел) для конкретного случая вещественной арифметики.

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

Тем не менее, я хотел бы знать заранее, есть ли какое-то сравнение между этими решателями, чтобы иметь более полезную основу для моих выводов. Меня интересуют как стандартные тесты, так и пользовательские тесты на GitHub или Stack.

Я нашел только эту статью cvc5 (https://www-cs.stanford.edu/~preiner/publications/2022/BarbosaBBKLMMMN-TACAS22.pdf ), которая, очевидно, предлагает ее как лучший вариант. Я также нашел это минимальное сравнение ( https://lemire.me/blog/2020/11/08/benchmarking-theorem-provers-for-programming-tasks-yices-vs-z3/), которое говорит нам, что Yices В 15 раз быстрее, чем Z3 для конкретного примера.

Любой совет?

Запросы на внешние ресурсы не по теме на Stack Overflow. Я понимаю, что вы не просите нас порекомендовать решатель, но вы просите нас найти какое-то существующее исследование или анализ, который сравнивает решатели.

kaya3 15.09.2022 16:36

Я думаю, что это совершенно правильный вопрос, поскольку он ищет информацию о том, как использовать преимущества нескольких существующих решателей по своей сути. Именно для этого и существует соревнование SMT, хотя нужно быть осторожным, делая слишком общие предположения. Каждая проблема уникальна, когда дело доходит до производительности.

alias 15.09.2022 16:45
Почему в Python есть оператор "pass"?
Почему в Python есть оператор "pass"?
Оператор pass в Python - это простая концепция, которую могут быстро освоить даже новички без опыта программирования.
Некоторые методы, о которых вы не знали, что они существуют в Python
Некоторые методы, о которых вы не знали, что они существуют в Python
Python - самый известный и самый простой в изучении язык в наши дни. Имея широкий спектр применения в области машинного обучения, Data Science,...
Основы Python Часть I
Основы Python Часть I
Вы когда-нибудь задумывались, почему в программах на Python вы видите приведенный ниже код?
LeetCode - 1579. Удаление максимального числа ребер для сохранения полной проходимости графа
LeetCode - 1579. Удаление максимального числа ребер для сохранения полной проходимости графа
Алиса и Боб имеют неориентированный граф из n узлов и трех типов ребер:
Оптимизация кода с помощью тернарного оператора Python
Оптимизация кода с помощью тернарного оператора Python
И последнее, что мы хотели бы показать вам, прежде чем двигаться дальше, это
Советы по эффективной веб-разработке с помощью Python
Советы по эффективной веб-разработке с помощью Python
Как веб-разработчик, Python может стать мощным инструментом для создания эффективных и масштабируемых веб-приложений.
1
2
89
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

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

Вы всегда можете посмотреть результаты конкурса SMT: https://smt-comp.github.io

Сказав это, я думаю, что глупо искать «лучшее». Не существует хорошего критерия для осмысленного сравнения всех решателей: все зависит от вашего конкретного приложения.

Если ваша система позволяет использовать несколько серверных решателей, почему бы не воспользоваться преимуществом множества ядер на современных машинах: создать их все и использовать результат первого для завершения. Любой априорный выбор решателя будет страдать от случая, когда другой будет работать лучше. На данный момент запуск всех доступных и получение самого быстрого результата — лучший вариант использования вашего оборудования.

«почему бы не воспользоваться множеством ядер на современных машинах» — я предлагаю воспользоваться этим, используя неоднопоточный решатель; нет приличного решателя. «На данный момент запуск всех доступных и получение самого быстрого результата — лучший вариант использования вашего оборудования». Весьма сомнительно - существует множество доступных решателей, и во многих задачах они будут иметь одинаковую производительность друг с другом, поэтому, запуская их все, вы просто увеличиваете свои вычислительные затраты на какой-то постоянный коэффициент. В других случаях, безусловно, можно оценить, какой решатель будет работать лучше всего.

kaya3 15.09.2022 16:33

Это не мой опыт. Даже разные версии одного и того же решателя сильно различаются по производительности для одного и того же решателя. Оценка производительности для нескольких решателей, которые, как вы утверждаете, «наверняка возможны», не была моим опытом, даже для, казалось бы, простых задач с разными версиями решателей.

alias 15.09.2022 16:44

Большое спасибо! Я поиграюсь с многоядерниками и спрошу здесь, если обнаружу проблемы.

Theo Deep 15.09.2022 16:48

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