← Все статьи

2-ASP(Q) с weak constraints: сложность и реализация в Casper

Фрагмент логического программирования для оптимизации до Δ₃ᵖ — полная теория сложности и CEGAR в системе Casper.

Теги
researchsoftware engineering
Содержание

Коротко

ASP(Q) расширяет Answer Set Programming кванторами над answer sets. Класс 2-ASP(Q)^w (два квантора + weak constraints) достаточно выразителен для задач оптимизации уровня Δ₃ᵖ — и теперь имеет полную карту сложности плюс практический солвер.

Что изучили

Теория: полная характеризация основных задач для 2-ASP(Q)^w, включая ранее не разобранные случаи. Практика: CEGAR в системе Casper для вычисления оптимальных quantified answer sets.

Главные выводы

  • Фрагмент практически релевантен — не чистая теория.
  • CEGAR, адаптированный под ASP(Q), работает на жёстких бенчмарках из разных доменов.
  • Границы сложности жёсткие (tight completeness).

Что это значит для разработчиков

  1. Для комбинаторной оптимизации с вложенными кванторами смотрите ASP(Q) / Casper, не только SAT/SMT.
  2. Weak constraints — способ выражать soft goals в декларативной модели.
  3. CEGAR-паттерн переносим на другие abstraction-refinement пайплайны.

Ограничения

Ниша declarative logic; интеграция в обычный микросервисный стек редка.