Strong Equivalence in Answer Set Programming with Constraints

TL;DR

This paper extends the concept of strong equivalence in Answer Set Programming to include constraints, providing a logical characterization and translation method to reason about equivalence in solvers, along with complexity analysis.

Contribution

It introduces a precise characterization of strong equivalence with constraints using the logic of Here-and-There and offers a translation for practical solver analysis.

Findings

Strong equivalence can be characterized by Here-and-There logic with constraints.

A translation from clingo-based solvers to Here-and-There logic is provided.

The computational complexity of determining strong equivalence is analyzed.

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.