Strong Equivalence in Answer Set Programming with Constraints
This work addresses a foundational problem in logic programming for researchers and practitioners in AI, focusing on theoretical extensions rather than incremental improvements.
The paper tackles the problem of characterizing strong equivalence in Answer Set Programming with constraints, demonstrating that under certain assumptions, it can be precisely characterized by equivalence in the logic of Here-and-There with constraints, and presents a translation to enable reasoning about strong equivalence in clingo-based solvers.
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.