Strong Equivalence in Answer Set Programming with Constraints
Pedro Cabalar, Jorge Fandinno, Torsten Schaub, Philipp Wanko
TL;DR
This work extends Answer Set Programming with constraints by introducing Here-and-There with constraints ($HT_{c}$) as a unifying framework to characterize strong equivalence in CASP. It provides a direct $HT_{c}$-theoretic encoding of constraint-programs, proves that strong equivalence of $ ext{T}$-programs corresponds to HT_c-equivalence of their translations, and analyzes the associated computational complexity, highlighting undecidability in general and $ ext{coNP}^{O}$-complete results under polynomial-time decidable theories. The translation framework also supports reasoning about external theories and their interactions with regular atoms, enabling modular optimization and potential new hybrid solvers. Overall, the paper delivers both theoretical foundations and practical tools for modular reasoning and optimization in ASP-enhanced constraint solving.
Abstract
We investigate the concept of strong equivalence within the extended framework of Answer Set Programming with constraints. Two groups of rules are considered strongly equivalent if, informally speaking, they have the same meaning in any context. We demonstrate that, under certain assumptions, strong equivalence between rule sets in this extended setting can be precisely characterized by their equivalence in the logic of Here-and-There with constraints. Furthermore, we present a translation from the language of several clingo-based answer set solvers that handle constraints into the language of Here-and-There with constraints. This translation enables us to leverage the logic of Here-and-There to reason about strong equivalence within the context of these solvers. We also explore the computational complexity of determining strong equivalence in this context.