MaxSMT-решатель, поддерживающий режим портфолио

В. В. Фомина^a, В. Соболь^b, Д. В. Кознов<sup>a

a</sup> Санкт-Петербургский государственный университет
^b Университет ИТМО

Аннотация: Задача MaxSMT заключается в определении выполнимости формулы теории первого порядка с ограничениями. В статье представлен подход к решению этой задачи для случая бескванторных теорий, которые обычно разрешимы и востребованы на практике для генерации тестов к программному обеспечению. Подход включает в себя модифицированный MaxSAT-алгоритм PrimalDualMaxRes, в котором использование SAT-решателя заменено SMT-решателем, а также реализацию режима портфолио. Последний означает, что итоговый MaxSMT-алгоритм запускается параллельно с несколькими SMT-решателями, и в качестве конечного результата берется наилучший. В качестве SMT-решателей, на базе которых построен режим портфолио, были выбраны Z3, Yices и Bitwuzla. Подход реализован с использованием открытой Kotlin-библиотеки KSMT, реализующей инфраструктуру для работы с набором MaxSMT-решателей. В статье также представлен первый тестовый набор (benchmark) для MaxSMT-задачи. Проведенные эксперименты подтверждают эффективность предложенного решения. Разработанное портфолио MaxSMT-решателей справляется с примерами из тестового набора данных более, чем в четыре раза быстрее существующего MaxSMT-решателя vZ (проект Z3).

Ключевые слова: задача MaxSMT, MaxSMT-решатель, библиотека KSMT, SMT-решатель, режим портфолио

DOI: 10.15514/ISPRAS-2025-37(4)-10