Компьютерная наука делает шаг вперед в области гибридного логического вывода. Исследовательница Юлиия Лерлер (Yuliya Lierler) представила EZSMTv3 — новую версию фреймворка для Constraint Answer Set Programming (CASP). Эта система объединяет декларативное программирование (ASP) с обработкой ограничений и проверкой выполнимости модификаций теорий (SMT), позволяя эффективно кодировать сложные комбинаторные задачи поиска.
Архитектура и ключевые улучшения
EZSMTv3 строится на фундаменте предыдущей версии EZSMT+, но предлагает существенные архитектурные сдвиги. Вместо реализации собственных процедур поиска, система использует мощь современных SMT-солверов: CVC5, YICES и Z3. Это позволяет переложить вычислительную нагрузку на оптимизированные инструменты, специализирующиеся на проверке выполнимости.
Среди ключевых нововведений:
- Расширенный язык ввода: Поддержка более выразительных конструкций для описания ограничений.
- Оптимизация: Внедрена поддержка слабых ограничений (weak constraints), что критично для задач оптимизации.
- Гибкость: Создана база для легкой интеграции новых типов ограничений.
Сравнение с конкурентами
В статье представлены результаты бенчмаркинга, сравнивающие EZSMTv3 с другими CASP-системами, такими как CLINGCON, CLINGO[DL] и CLINGO[LP]. Особый акцент сделан на способности EZSMTv3 обрабатывать смешанные домены, включающие как целочисленные, так и вещественные ограничения.
| Характеристика | EZSMTv3 | CLINGCON / CLINGO[DL] |
|---|---|---|
| Базовая технология | SMT-солверы (CVC5, YICES, Z3) | Специализированные CASP-решатели |
| Поддержка оптимизации | Да (weak constraints) | Зависит от версии/расширения |
| Типы ограничений | Целые и вещественные числа (mixed-domain) | Часто ограничено целыми числами |
| Подход к поиску | Трансляция в SMT | Гибридный поиск |
Значение для индустрии
Работа находится на рассмотрении в журнале Theory and Practice of Logic Programming (TPLP). Успешная реализация EZSMTv3 открывает путь для более сложных теоретических исследований и практических применений в областях, требующих точного логического вывода с непрерывными переменными, таких как планирование роботов, верификация систем и биоинформатика.
Источник: arXiv cs.AI ↗