# Strong Equivalence in Answer Set Programming with Constraints

arXiv: https://arxiv.org/abs/2502.04302 · HTML: https://mlsanity.com/paper/2502.04302/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 19 references that are in the map.
- First posted on arXiv 6 Feb 2025.

## Builds on (most cited first, 5 of 5)

- [Clingo goes Linear Constraints over Reals and Integers](https://mlsanity.com/paper/1707.04053/) (2017)
- [Clingcon: The Next Generation](https://mlsanity.com/paper/1705.04569/) (2017)
- [A Uniform Treatment of Aggregates and Constraints in Hybrid ASP](https://mlsanity.com/paper/2003.04176/) (2020)
- [Constraint Answer Set Programming: Integrational and Translational (or SMT-based) Approaches](https://mlsanity.com/paper/2107.08252/) (2021)
- [An ASP semantics for Constraints involving Conditional Aggregates](https://mlsanity.com/paper/2002.06911/) (2020)

## Built on by (most cited first, 2 of 2)

- [FLINGO -- Instilling ASP Expressiveness into Linear Integer Constraints](https://mlsanity.com/paper/2602.09620/) (2026)
- [Bound-Founded Semantics for Answer Set Programming with Difference Constraints: Preliminary Report](https://mlsanity.com/paper/2607.21201/) (2026)

## Abstract (arXiv)

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.