Abstracting the Indistinguishable in ASP

1 Introduction

Answer set programming (ASP) is a widely used declarative programming framework where programs consist of rules and constraints describing solutions, so-called answer sets [Brewka et al., 2011]. Today, we see numerous applications of ASP in artificial intelligence, automated reasoning, and symbolic planning thanks to highly capable solvers [Gebser et al., 2014; Alviano et al., 2015; Alviano et al., 2017]. With increasingly large applications, generalizing from smaller details becomes crucial as it allows humans to identify the problem structure and the essential details. Constructing "good" abstractions over the problems from a few instances is key to finding generalized solutions that work for all potential instances with similar structure. The obtained generalized solutions can also be used as a guide in searching for a solution to the original problem.

Humans naturally and intuitively abstract, but defining notations and designing automated techniques turn out to be extremely challenging. While approaches that involve forgetting [Gonc¸alves et al., 2023; Doherty and Szałas, 2024], equivalence-based rewriting [Pearce, 2004; Eiter et al., 2004], partial evaluations [Brass and Dix, 1997; Janhunen et al., 2006] and dependency preserving abstractions [Saribatur and Woltran, 2023; Saribatur et al., 2024] show potential in obtaining simplifications of programs that might distinguish the essential details, the computational complexity of coming up with a simplified or abstracted program has received little attention so far.

Using the traditional notions of strong and uniform equivalence, which preserve answer sets between programs when they are extended with further programs and facts, respectively, easily result in quite technical constructions of the simplifications [Pearce, 2004; Eiter et al., 2004]. Furthermore an abstraction over the vocabulary cannot be treated. In forgetting [Gonc¸alves et al., 2023] the vocabulary is reduced by forgetting atoms, while the construction of the simplified programs satisfying the interesting properties of strong- and uniform persistence are also highly technical [Gonc¸alves et al., 2021; Berthold et al., 2019; Berthold, 2022] which was shown to be due to the aim to preserve dependencies w.r.t. the remaining atoms [Saribatur and Woltran, 2024].

Faithful abstractions [Saribatur et al., 2021] are first to define an abstraction via clustering atoms (in the non-ground setting) in the vocabulary, while preserving the answer sets, which was also defined for omitting atoms [Saribatur and Eiter, 2021]. Though the focus of [Saribatur and Eiter, 2021; Saribatur et al., 2021] was on over-approximating abstractions, and dealing with spurious abstract answer sets, thus constructing faithful abstractions was not investigated. Recently, abstraction by clustering notion was brought in to ground programs and restricted to achieve a uniform equivalence-like property [Saribatur et al., 2024], with the aim to capture irrelevancy of atoms, when the program is further extended with facts, which goes towards capturing generalized reasoning. A syntactic operator was proposed to obtain uniform abstractions, when possible, for certain fragments, and the complexity of checking whether a program is a uniform abstraction was shown to be in ΠP3 while hardness was left open.

A long open question is whether abstracting over atoms for getting rid of irrelevant details is similar to symmetry detection, especially whether it is possible to abstract over symmetry, c.f. [Fox et al., 2005; Yu et al., 2023]. So far in ASP, symmetry notion has focused on detecting symmetries for constructing symmetry breaking constraints to help with solving [Drescher et al., 2011; Tarzariol et al., 2023]. The potential of these symmetries to obtain an abstracted program was not investigated.

Here, we focus on faithful and uniform abstractions with clustering, take a look at symmetry with a fresh perspective, and show how to obtain intuitive abstractions over the indistinguishable. We systematically analyse the computational complexity of testing abstractions and checking for existence of abstractions. Our main contributions are as follows:

1. We examine the computational complexity of checking abstractions and existence of abstractions for established notions (faithful and uniform) using clustering (see Tables 1 and 2). Thereby, we provide novel insights into the crucial question of existence of abstractions.
2. We propose a novel syntactic operator that can construct uniform abstractions of programs, if exists. We show that the known necessary condition for uniform abstractions is in fact also sufficient, without directly diving into semantic technicalities (e.g., HT models).
3. We investigate the potential of syntactic and semantic symmetries in ASP in determining abstractions. We establish that symmetry and abstraction notions are orthogonal, due to the difference of interchangeability and indistinguishability.
4. We define a relaxation of the shown condition for uniform abstractions to capture atoms being semantically indistinguishable, which allows our syntactic operator to obtain intuitive faithful abstractions.
5. We show, with further syntactic restrictions, syntactically symmetric atoms become semantically indistinguishable and achieve uniform abstractions. We illustrate the usefulness of abstracting such symmetries when compared to breaking them.

Related Works and Boarder Relation to AI. Since the early days of AI research, several works have explored the definition of notions of abstraction for various domains, with some focusing on theoretical properties and others on domainspecific applications [Saitta and Zucker, 2013]. In planning, researchers investigated abstraction notions for generalized planning [Banihashemi et al., 2017; Srivastava et al., 2011; Illanes and McIlraith, 2019; Giacomo et al., 2025], where a plan that can solve multiple instances of a problem is obtained from a given a set of planning instances. Early approaches aimed to ignore irrelevant parts [Nebel et al., 1997] and synthesized invariants aiming to speed up the search [Rintanen, 2000]. Recent approaches aim at handling symmetries [Sievers et al., 2019] and compute abstractions for certain types of planning problems [Dong et al., 2025; Cui et al., 2021]. However, it remains entirely unclear how these approaches can be generalized to other AI formalisms. More importantly, the actual computational cost of finding good abstractions in a domain-independent setting, especially those that provide generalization abilities, remained largely open. Symmetry is widely used constraint solving and propositional satisfiability [Krishnamurthy, 1985; Devriendt et al., 2016] and recently also to lift tasks [Carbonnelle et al., 2024]. Breaking symmetries for faster solving has been addressed in a couple of publications [Benhamou, 2013; Devriendt and Bogaerts, 2016; Tarzariol et al., 2023].

2 Preliminaries

We assume familiarity with basics in Boolean satisfiability (SAT) and satisfiability of quantified Boolean formulas (QSAT) [Kleine B¨uning and Lettman, 1999], graphs and digraphs [Diestel, 2024; Bang-Jensen and Gutin, 2008], computational complexity theory [Papadimitriou, 1994; Arora and Barak, 2009], and answer set programming [Janhunen and Niemel¨a, 2016; Calimeri et al., 2020; Gebser et al., 2012]. Below, we briefly recap notions used in this paper.

Computational Complexity. Let Σ and Σ′ be finite alphabets. We call I ∈ Σ∗ an instance and n denotes the size of I. A decision problem is a subset L ⊆ Σ∗ . Recall that P and NP are the complexity classes of all deterministically and non-deterministically polynomial-time solvable decision problems [Cook, 1971], respectively. We also need the Polynomial Hierarchy (PH) [Stockmeyer, 1976; Wrathall, 1976]. In particular, ∆P0 := ΠP0 := ΣP0 := P and ∆Pi := P ΣPi-1 , ΣPi := NPΣPi , and ΠPi := coNPΣPi for i > 0 where C D is the class C of decision problems augmented by an oracle for some complete problem in class D.

Answer Set Programming (ASP). We consider propositional programs. Let l,m, n be non-negative integers such that l ≤ m ≤ n, and a1, . . . , an distinct propositional atoms. A disjunctive rule r is of the form

By Hr := {a1, . . . , al}, B+ r := {al+1, . . . , am}, and Br := {am+1, . . . , an}, we denote the head, positive or negative body atoms of r, respectively. We say that r is normal if |Hr| ≤ 1, positive if Br = ∅, and Horn if r is normal and positive. A disjunctive logic program (DLP) P , or program for short, is a set of rules, where at(P) := ⋃r∈P (Hr ∪B+ r ∪ Br ) denotes its atoms. For a set U of atoms and a logic program P , we say P is over U if at(P ) ⊆ U. A program P has a certain property if all its rules have the property. The (labeled) dependency digraph DP is the digraph defined on the set ⋃r∈P (Hr ∪ B+ r ∪ Br ) of atoms, where for every rule r ∈ P, two atoms b ∈ B+ r ∪ Br and a ∈ Hr are joined by an edge (b, a) labeled by "-" if b ∈ Br and "+" if b ∈ B+ r . An odd cycle of P is a cycle in DP that contains odd number of negative labeled edges. A normal program is stratified if there is a mapping str: at(P) → N such that for each rule r ∈ P, we have (i) if x ∈ B+ r and y ∈ Hr, then str(x) ≤ str(y) and (ii) if x ∈ Br and y ∈ Hr, then str(x) < str(y). By Disj, Strat, and Horn we denote the class of all disjunctive logic programs, stratified programs, and Horn programs respectively. An interpretation M ⊆ at(P) satisfies a rule r if (Hr∪Br )∩M ̸= ∅ or B+ r ⊈M, andM |= P ifM satisfies every rule r ∈ P . The (GL) reduct of P with respect to M is defined as P M := {Hr ← B+ r | Br ∩M = ∅}. Then, M is an answer set of P if M is a model of P, in symbols M |= P, such that no interpretation N ⊊ M is a model of P M [Gelfond and Lifschitz, 1988]. We let the set AS(P) consist of all answer sets of P. Deciding whether a program P has an answer set is ΣP2 -c and in P for DLPs and stratified programs, respectively [Eiter and Gottlob, 1995; Gelfond and Lifschitz, 1988].

Abstractions

We follow standard notations on abstractions in ASP [Saribatur and Eiter, 2021; Saribatur et al., 2024]. We admit to conveniently apply mappings also to sets of sets of atoms and rules. Below, we summarize existing notions of ASP abstractions. We denote the domain D of a function f : D → A by dom(f). For a function f, we denote the inverse function f -1 := { f(d) ↦→ d | d ∈ dom(f) }. Given sets U and V with |U| ≥ |V|, a mapping m is a surjective function m : U → V. For a set S, we let m(S) := {m(e) | e ∈ S }. Next, we formally define what we mean by clustering atoms.

Definition 1. We call a mapping m : U → V a clustering when V contains a set Vc = {a ∈ V | |m-1 (a)| > 1} of cluster atoms. Accordingly, we divide U into set of clustered atoms Clm = {a ∈ U | m(a) ∈ Vc}.

Next, we illustrate a clustering mapping.

Example 2. Consider the following program

Here, d and e both derive f whenever c holds true. So one can argue that specific details of whether d or e holds true are not of importance, and define a clustering as m : {d, e} → k. 1

1 This notation of a mapping represents only the clustered atoms. k is a fresh (clustered) atom to which m maps multiple atoms to. For those atoms that are not clustered, i.e., remain singletons, we assume they are mapped to themselves.

Note that omission mapping [Saribatur and Eiter, 2021] can be seen as a special case of clustering, where the set of atoms to omit are clustered into ⊤.

Faithful abstractions. Faithful abstractions preserve exactly the projected semantics of the original program, i.e., they do not invent new answer sets that appear in the abstract program but have no counterpart in the original answer sets [Saribatur and Eiter, 2021].

Definition 3. Formally, given a program P over U and a mapping m : U → V, and a program Q over V. Then, Q is a faithful m-abstraction of P if we have

We say that P is faithfully m-abstractable if there exists a Q that is a faithful m-abstraction of P .

An ELP 2 P can always have a faithful abstraction, for any given mapping [Saribatur and Woltran, 2024]. Though faithful abstractions are too relaxed to capture an abstraction notion that preserves dependencies within the program. This was investigated with clustering mapping for non-ground programs, and the complexity of checking whether some program is a faithful abstraction of a given program was shown to be coNEXP NP -complete [Saribatur et al., 2021]. For ground programs, for omission mapping, checking faithfulness was shown to be ΠP2 -complete for normal programs [Saribatur and Eiter, 2021].

Example 4 (cont.). Consider program P0 from Example 2. Naturally, since P0 only has the empty set as the answer set, we can have Q0 = ∅ as a faithful abstraction. If, however, we consider P ′0 := P0 ∪ {c} that results in answer sets {c, d, f}, {c, e, f}, then program

is a faithful abstraction of P ′0 , since m(AS(P ′0 )) = {{c, k, f }} = AS (Q′0 ).

Uniform Abstractions. Uniform abstractions simplify a program by replacing atoms with abstract representatives uniformly across the entire program such that answer sets do not change even if arbitrary facts are added [Saribatur et al., 2024].

Definition 5 (UniformAbstractions). Formally, let U and V be disjoint sets of atoms such that |V| < |U|. Given a program P over U and a mapping m : U → V, and a program Q over V. Then, Q is a uniformm-abstraction of P if, for any set F of facts over U, we have

We say that P is uniformly m-abstractable if there exists a Q that is a uniformm-abstraction of P.

Since not every program is uniform abstractable for a given mapping, Saribatur et al. (2024) studied necessary and sufficient conditions for abstractability in terms of SE- and UEmodels, and a model-based representation of such abstractions, showing that it is unique. 3

2 An extended logic program (ELP) P extends DLPs with double negation in the body.

Example 6 (cont.). Consider program P0 from Example 2. We have Q0 = {k ← c; f ← k} as a uniform m-abstraction of P0.

Saribatur et al. (2024) established the following complexity results. Given a program P over U and a mapping m : U → V. Deciding whether P is uniform m-abstractable is ΠP3 - complete. Given sets U and V of atoms, a program P over U, a mapping m : U → V, and a program Q over V, checking whether Q is a uniformm-abstraction of P is (i) in ΠP3 and ΠP2 -hard if P, Q ∈ Disj and (ii) the complexity drops to coNP when both programs are Horn.

3 Existence of Abstractions

Based on the definition of uniform abstractions, we first consider the computational problem for testing mappings, providing a more fine-grained analysis of previous considerations.

We start by assuming that the mapping m and program Q are given, and that we are unaware whether P is uniform m-abstractable.

Lemma 7. Given a program P over U, mapping m : U → V, and a program Q. Deciding whether Q is a faithful mabstraction of P is:

1. for stratified programs in P,
2. for normal programs ΠP2 -complete, and
3. for disjunctive programs ΠP3 -complete.

Proof. ("Membership").

(Claim 1): Stratified programs can only have at most one answer set, which can be computed in polynomial time [Gelfond and Lifschitz, 1988].

(Claims 2 and 3): We show membership of the inverse problem. For membership of the inverse question, it suffices to guess a candidate M that is an answer set of Q such that all answer set candidates N with N = m(M) that are not in m(AS(P)). Additionally, we might need to guess two answer set candidates M,N such that N = m(M) is in m(AS(P)) while M is not an answer set of Q. Both checks work in NP NP C , where C is the complexity for verifying a given answer set candidate. Consequently, the desired inverse problem is in the co-complexity class.

("Hardness").

(Claim 2): We reduce from ∀∃-SAT, and let Φ = ∀U∃V ϕ with ϕ = ∧ni=1 (li,1 ∨ li,2 ∨ li,3). We use copies of atoms, e.g., ˜ U={˜ u | u ∈ U} and construct PΦ as:

3 SE-models, also referred as HT-models [Lifschitz et al., 2001], represent the monotone core of the program and UE-models capture their maximal proper subsets [Eiter et al., 2007]. They are used to characterize strong and uniform equivalence of programs.

where ˜li,j is given by atom a if li,j is ∼a and by ˜a if li,j is a (positive) variable a. Q is constructed by:

We define mapping m by m(u) = u for every u ∈ U ∪ ˜ U and m(v) = sat for v ∈ {sat} ∪ V ∪ ˜ V ∪W ∪˜ W. It is easy to see that Φ is valid iff Q is a faithful m-abstraction of PΦ. (Claim 3): We reduce from ∀∃∀-SAT, and let Φ = ∀U∃V ∀Wϕ with ϕ = ∨ni=1 (li,1 ∧ li,2 ∧ li,3). We construct PΦ as follows.

where ˜li,j is given by atom ˜a if li,j is ∼a and by a if li,j is a (positive) variable a. Q is constructed by:

We define mapping m by m(u) = u for every u ∈ U ∪ ˜ U and m(v) = sat for v ∈ {sat} ∪ V ∪ ˜ V ∪W ∪˜ W. Then, Φ is valid iff Q is a faithful m-abstraction of PΦ.

Remark that there is a complexity jump from stratified programs to normal programs. This is because, for membership, it does not suffice to guess a set S ⊆ U that is not an answer set of P but m(S) is an answer set of Q, as there can be other S′ ⊆ U that is an answer set of P and m(S) = m(S′ ). In fact, for every S′ that can be mapped to m(S), one needs to check that S′ is not an answer set of P. This increases complexity. This leads to the following result.

Theorem 8. Given a program P over U, mapping m : U → V, and a program Q. Deciding whether Q is a uniform mabstraction of P is:

1. for stratified programs coNP-complete,
2. for normal programs in ΠP2 , and
3. for disjunctive programs ΠP3 -complete.

Proof. ("Membership"):

The upper bound was already established by Saribatur and Woltran (2024) for disjunctive programs. The construction works as follows: For given P, Q, and m, we check for Equation (2) defining Q to be a uniform m-abstraction. For the complementary problem, we guess a set F of facts and a set I checking whether I ∈ AS (P ∪F ) and checking whether m(I) ∈ AS(Q ∪m(F)), but that it does not hold for both. As answer set computation for disjunctive programs is in ΠP2 , the equality check is contained in ΣP3 . This then drops down one level for normal programs, and two levels for stratified programs.

("Hardness"):

(Claim 1): We reduce from ∀-SAT, and let Φ = ∀Uϕ with ϕ = ∨ni=1 (li,1 ∧ li,2 ∧ li,3).

where ˜li,j is given by atom a if li,j is ∼a and by ∼a if li,j is a (positive) variable a.

Q is independent from Φ and constructed by:

We define mapping m by m(u) = sat for every u ∈ U ∪ {usat, di | 1 ≤ i ≤ |Φ|}. It is easy to see that Φ is valid iff Q is a uniform m abstraction of PΦ.

(Claim 3): We establish the lower bound by knowing that uniform simplifiability [Saribatur and Woltran, 2023], which abstraction by omission of atoms, is a special case of clustering see [Saribatur et al., 2024, Prop.16]. In [Saribatur andWoltran, 2023] ΠP3 -hardness proof of checking whether P is simplifiable for a given set A of atoms, a program PΦ is constructed where A cannot be omitted if and only if the (3, ∃)-QSAT formula Φ is satisfied. In [Saribatur and Woltran, 2023] it was also shown that if P is uniform abstractable for omitting A, then P|A is an abstraction where A = U \ A and P|A refers to restricting the vocabulary to A. Thus, for hardness, we can use that PΦ and construct Q as P|A which is then not an uniform abstraction for omitting A of P if and only if Φ is true.

Ultimately, we are interested in whether a mapping m even exists so that P is uniformm-abstractable, as it is known that not every program might be abstractable with a non-trivial mapping, meaning that it maps at least two atoms to one.

Theorem 9. Given a program P over U. Deciding whether there exists a non-trivial mapping m : U → V such that P is uniform m-abstractable.

1. for stratified programs in ΣP2 ,
2. for normal programs in ΣP3 , and
3. for disjunctive programs in ΣP4 .

Proof. It is easy to see that we can guess mwith an additional level (on top of Theorem 8). Indeed, by [Saribatur et al., 2024] we know that the semantic characterization of uniform abstractions is unique, thus we can restrict ourselves to specific programs Q that are determined by P and m.

While Saribatur and Woltran (2024) observed that for any set A of atoms, an ELP P is faithful abstractable by omitting A, this does not hold for programs (instead of ELPs) and clustering. Below, Example 10 illustrates that if we consider programs, it is not always the case that a faithful abstraction by clustering exists.

Example 10. Consider the following program.

The answer sets of P1 are {a, b} and {c}. Now, consider the mapping m : {a, c} ↦→ k. Then, the desired answer set of a faithful abstraction would be {k, b} and {b}, which however conflicts with subset-minimality of answer sets. In turn, with the mapping m a faithful abstraction cannot be found.

In consequence of the previous example, we can now ask how hard it is to find a mapping such that P is faithful mabstractable.

It turns out that the decision problem just boils down to answer set consistency, however, we prove even a stronger result. Even if we fix V, a faithful abstraction trivially exists.

Theorem 11. Given a program P over U and a set V of atoms. There always exists a non-trivial mapping m : U → V s.t. P is faithful m-abstractable (decidable in constant time).

Proof. We show that a witnessing program Q and matching m always exists. If the empty answer set is an answer set of P , observe that this has to be the only answer set, as disjunctive rules do not allow both an empty answer set and a non-empty answer set simultaneously. Consequently, in this case we construct Q = {← x, ¬x. | x ∈ V} and take any mapping m. Otherwise, if P does not have an answer set, we let Q = {← ¬x. | x ∈ V} and take any arbitrary mapping m.

Otherwise, if P admits a (non-empty) answer set, we pick an arbitrary y ∈ V and construct Q = {y.}∪{← x, ¬x. | x ∈ V, x ̸= y} and set m(a) = y for every a ∈ U.

However, if we ask for a consistent Q, the situation changes.

Theorem 12. Given a program P over U and a set V of atoms. Asking whether there is exists a non-trivial mapping m : U → V s.t. P is faithful m-abstractable for some consistent Q is:

1. for stratified programs in P-complete,
2. for normal programs in NP-complete, and
3. for disjunctive programs in ΣP2 -complete.

Proof. ("Membership").

If the empty answer set is an answer set of P, which is in ΣPi for stratified (i = 0), normal (i = 0), and disjunctive (i = 1) programs, as above we construct witness Q = {← x. | x ∈ V} and take any mapping m.

Otherwise, we return yes iff P admits a (non-empty) answer set, as this allows us to pick an arbitrary y ∈ V and construct witness Q = {y.}∪{← x. | x ∈ V, x ̸= y} and set m(a) = y for every a ∈ U.

("Hardness").

We pick any a ∈ U and set V = {a}. Suppose that there is a Q and an m : U → V such that m(AS(P)) = AS(Q). Since Q admits an answer set by assumption, we know that our abstraction problem decides the consistency of P , as then P is consistent as well.

Constructing Abstractions

Now after we established knowledge about the computational complexity of checking for existence of abstractions, we ask how to come up with the concrete abstraction other than the very generic consideration as in the previous section. Interestingly, Saribatur et al. (2024) introduced a syntactic operator that simply applies the mapping m to the atoms in each rule in P , denoted as m(P), to construct uniform abstractions as in the following example.

Example 13 (cont.). Consider program P0 from Example 2. The program m(P0) is {k ← c; f ← k}, which is a uniform m-abstraction.

This syntactic operator is guaranteed to work for positive programs or for programs where negation can be eliminated, while the guarantee no longer holds for more general ones.

Next, we address this topic by introducing a new operator that allows us to construct uniform abstractions of disjunctive programs. We observe that the construction m(P) fails to achieve abstractions if the clustered atoms have negative dependencies, though without odd loops.

Example 14. Consider the programs

When clustering a and b by m:{a, b} ↦→ k, m(P2) = m(P ′2 ) = {k ← ∼k} is clearly not a uniform m-abstraction of the programs, since the negative dependency among the atoms is overwritten. However, it can be observed that Q = {k.} is a uniform m-abstraction of both programs. Although, for the program P ′′ 2 = P2 ∪ {b ← a}, the program {k ← ∼k} would be a uniform m-abstraction.

Next, we extend the previous operator to treat negative dependency. For a program P with exactly l odd loops, let Lc1 , . . . , Lcl denote all sets of literals of an odd loop, if exists.

Definition 15. Given a mapping m and a rule r : Hr ← Br,

where L ⊆ Br ∩Clm satisfying ∀ℓ ∈ L ∃α ∈ Hr : m(α) = m(ℓ) and {α, ℓ} ⊈ Lcj for all j.

The intention of the operator is to keep track of the odd loops, and remove those atoms from the negative body that agree on the mapping with the head of the rule but are not involved in an odd loop.

Example 16 (cont.). Consider program P2 from Example 14. Applying m∗ to rule r1 = {a ← ∼b} gives us m∗ (r1) = {m(a) ←} since {b} ⊆ Br1 ∩ Clm, a ∈ Hr1 , m(a) = m(b). Similarly for r2 = {b ← not a} from P ′2 . Thus we get m⋆ (P2) = m⋆ (P ′2 ) = {k}. Now for program P ′′ 2 = P2 ∪ {b ← a} we have Lc = {b, a} as the set of literals involved in an odd loop. Thus m⋆ (P ′′ 2 ) = {k ← ∼k; k ← k}.

Saribatur et al. (2024) established that not every program is uniform abstractable for a given mapping. To find the necessary and sufficient conditions for abstractability on the SEmodels of the program, they use the following observation.

Proposition 17 (Saribatur et al. 2024). If there is a uniform m-abstraction of P, then, for all Y and all sets of facts Z,Z ′ such that m(Z ′ ) = m(Z):

Instead of shifting the focus to SE-models, we remain with the answer set correspondence checking as it provides a much simpler picture. Thus, we first show that this condition is sufficient for the existence of a programQ, by showing that Q = m⋆ (P) is a uniform m-abstraction and thus satisfies Equation (2) of Definition 5. 4

4 We prove statements marked by "⋆" in the supplemental material at https://www.dbai.tuwien.ac.at/user/saribat/pub/ijcai26-supp.pdf.

Theorem 18 (⋆). Let U and V be sets of atoms, P be a program over U and m : U → V a mapping. If P satisfies Equation (3) for mapping m, then Q = m⋆ (P) is a uniform m-abstraction of program P .

Proof (Sketch). We assume this is not the case, and that there exists some F such that m(AS (P ∪ F )) ̸= AS (Q ∪ m(F )). We do case analysis and first look at the case when there exists I ′ ∈ AS(P ∪ F), while m(I ′ ) = I /∈ AS(Q∪m(F)). Since the aim is to reach a contradiction to existence of an I ′ ∈ AS(P ∪ F) with m(I ′ ) = I it is enough to look at F ′ = F ∪ m-1 (m(F )) which contains all atoms clustered in m(F). Then since P satisfies (3), we reach that this condition holds for all F. By looking at the possibilities of I not being an answer set of AS (Q∪m(F )) by tracing the trouble making rules, we always reach a contradiction. The same approach is applied for the other case when There exists I ∈ AS(Q ∪ m(F)) s.t. I /∈ m(AS(P ∪F)).

This operator thus extends our ability to construct uniform abstractions to programs, whenever possible.

Observe that, Theorem 18 shows that if Equation (3) is satisfied for a mapping, then a uniform abstraction can be constructed. Thus Equation (3) is in fact a necessary and a sufficient condition for the existence of a uniform abstraction.

Corollary 19. Given a program P and a mapping m, P satisfies Equation (3) for mapping m iff there is a uniform mabstraction of P .

4 Interchangeable vs. Indistinguishable

Is it possible to abstract over symmetries? That is a natural question that arises from abstractions and when constructing operators. In this section, we take a look at symmetries and investigate their potential to obtain an abstracted program in the context of uniform and faithful abstractions.

4.1 Symmetry

We begin by providing the usual definitions of symmetry from the context of propositional satisfiability [Krishnamurthy, 1985] to ASP. A permutation of a set S is a bijection σ : S → S, meaning that σ rearranges the elements of S in which each element i is replaced by the corresponding σ(i). For example, (3, 1, 2) corresponds to σ(1) = 3, σ(2) = 1, and σ(3) = 2.

Definition 20 (Symmetry). Given a program P over U and a permutation σ : U → U. The permutation σ is

• a syntactic symmetry of program P if P and σ(P) are identical;
• a semantic symmetry of P if AS(P) = AS(σ(P)).

It is known that every syntactic symmetry is a semantic symmetry, and not vice versa, which we also illustrate in the following example.

Example 21 (cont.). Consider program P1 from Example 10. Consider permutation σ = (b, a) meaning a ↦→ b, b ↦→ a. The program σ(P1) is not identical to P1 and thus σ is not a syntactical symmetry. But σ is a semantic symmetry, since a and b always appear together in an answer set.

As we are interested in investigating abstraction over symmetry, we define the notions of symmetry between atoms in a program. We use cycles where a permutation is a product of disjoint cycles. A cycle a1a2a3 . . . ak means that the permutation maps a1 ↦→ a2, a2 ↦→ a3, and so on, finally ak ↦→ a1.

Definition 22 (Symmetry of Atoms). Given a program P over U. Then, a set S ⊆ U of atoms is

• syntactically symmetric to one another in P, if there exists a permutation σ with cycle ℓ1 . . . ℓn for ℓi ∈ S that is a syntactic symmetry of P .
• semantically symmetric to one another in P, if there exists a permutation σ with cycle ℓ1 . . . ℓn for ℓi ∈ S that is a semantic symmetry of P .

The following example illustrates symmetry of atoms.

Example 23. Consider the following programs.

For the set S = {a, b}, we can see that the atoms in S are syntactically and thus semantically symmetric since the permutation σ = (a, b) is a syntactic symmetry of P3. However for program P4, the atoms in S are neither syntactically nor semantically symmetric.

The next example illustrates that actually not every semantically symmetric is a syntactically symmetric.

Example 24. In program P5 = {b ← a}, a and b are semantically symmetric, as P5 has only empty set as answer set, while not syntactically symmetric.

We have seen that uniform abstractions are able to abstract over atoms that are semantically indistinguishable according to their dependencies within the program. One natural question that arises is whether symmetric atoms have such an indistinguishable aspect, which seem to be not always the case as we illustrate in the example

Example 25 (cont.). Consider programs P3 and P4 from Example 23. For a mapping m : {a, b} → k, the program

is a uniform abstraction for both of them.

The above example shows that uniform abstractions are more general than capturing indistinguishability w.r.t syntactic symmetry, since in case of P4 the existence of {b ← a.} causes to lose the syntactic symmetry property, while still presents an indistinguishable behavior for abstracting.

Though also not every symmetry is uniform abstractable.

Example 26. Consider the program as follows.

a and b are syntactically symmetric, and thus semantically symmetric, however not uniform abstractable as we have AS (P6 ∪ {a, b}) = {{a, b}} while AS (P6 ∪ {a}) = {{a, c}}, not agreeing on the mapping {a, b} → k.

Consider the program as follows.

Similar to P6, here, a and b are syntactically symmetric, and thus semantically symmetric. However, they are not uniform abstractable, since we have AS (P7 ∪{a, b}) = {a, b, c} while AS (P7 ∪{a})={a}, not agreeing on the mapping {a, b} ↦→ k.

In the above example, although a and b are symmetric, they are not semantically indistinguishable, since c depends on their individual truth values, thus an abstraction satisfying the uniform condition cannot be achieved. However, for both programs P6 and P7 it is possible to come up with a faithful abstraction, as they are less restrictive than uniform abstractions.

Example 27 (cont.). Consider programs P6 and P7 from Example 26. The programs Q6 = {k. c ← k} and Q7 = {k} are faithful abstractions for programs P6 and P7, satisfying m(AS(Pi)) = AS(Qi), i ∈ {6, 7}.

However, in some cases, the obtained faithful abstraction might no longer resemble the original structure.

Example 28. Consider the program P8 as follows.

We have AS(P8) = {{x, a, b, c}, {y, a}, {y, b}}. a and b are syntactically symmetric, and the program

is a faithful abstraction of P8. Observe that the last rule in Q8 needs to be newly constructed to capture the semantic of the last rule of P8, thus no longer resembles it.

4.2 Indistinguishability

As shown, not every symmetry is uniform abstractable, meaning that uniform abstractions are too strong. Although faithful abstractions are weaker and could be obtained, it is not clear how to construct them when implicit relations that abstraction cannot distinguish need to be preserved in some way, as illustrated in Example 28. Meanwhile, our operator m⋆ in Definition 15 gives an intuitive way to construct abstractions with clustering. Thus, we can naturally ask whether it can be used to obtain intuitive faithful abstractions, which showed to be of importance when wanting to abstract over symmetry. Therefore, we first examine the following example.

Example 29 (cont.). Consider programs P6 and P7 from Example 26. The program m⋆ (P6) := {k. c ← ∼k.}, resp. m⋆ (P7) := {k. c ← k.}, is not a faithful abstraction of P6, resp. P7.

In program P7, a and b both need to hold true to obtain c, which actually never occurs, while in P6 at most one of a or b needs to hold true to get c. These relations cannot be handled with such a syntactic operator. However, such cases can be detected when looking at the addition of a and b as facts, as shown in Example 26. Thus, we define a property over P, which is a relaxation of Equation (3) to catch such cases.

Definition 30. Given program P and mapping m : U → V with k ∈ Vc. We say that the set S = m-1 (k) of atoms are semantically indistinguishable in P with m if for all Y and all sets of facts Z, Z ′ ⊆ S:

Example 31 (cont.). In Example 26, for the programs P6 and P7, the atoms a and b are not semantically indistinguishable, while in P3 from Example 23 they are.

It turns out we can use m⋆ to obtain faithful abstractions over the semantically indistinguishable.

Theorem 32 (⋆). Given a program P over U and a mapping m, if all clustered atoms are semantically indistinguishable, then, the programm⋆ (P) is a faithful abstraction.

4.3 From Symmetry to Abstraction

Let us now investigate how and which abstractions are possible over the symmetry. For this the notion of m-positive programs, that disallows occurrence of clustered atoms in negative body of the rules, comes handy.

Definition 33 (Saribatur et al. 2024). For a mapping m, program P is m-positive if for each rule r ∈P , Br ∩Clm =∅.

Our observations on programs P6 and P7 from Example 26 show, in addition to m-positiveness, also the need to disallow occurrence of clustered atoms in the same body. Thus we establish the following result. Here, for simplicity, we focus on clustering only two atoms.

Proposition 34 (⋆). Let P be a program with syntactically symmetric atoms a1, a2. For a mapping m:{a1, a2} ↦→ k, if P is m-positive and if there is no rule r ∈ P with {a, b} ⊆ Br then a1 and a2 are semantically indistinguishable in P .

In fact, the syntactic conditions over P allows us to reach uniform abstractability from syntactic symmetry.

Theorem 35 (⋆). Let P be a program with syntactically symmetric atoms a1, a2. For a mapping m:{a1, a2} ↦→ k, if P is m-positive and if there is no rule r ∈ P with {a, b} ⊆ Br then P is uniformm-abstractable.

Discussion

Intuitively, the notion of being semantically indistinguishable captures situations when we only need to match existence, thus we do not care about the actual object. Whereas interchangeable talks about whether there is a permutation that allows us to swap objects. The idea of symmetry is to detect interchangeable objects, thus avoiding an explosion in the search for a potential solution, such as pigeons and holes in the pigeonhole problem or colors in the graph coloring problem. However, in these problems, even though the objects are interchangeable, identifying them is necessary to ensure that the problem's constraints are still satisfied. This can also be observed in a very recent work [Carbonnelle et al., 2024] where the authors intuitively compress these objects while still preserving the information about the number of objects.

Abstraction, on the other hand, is about losing the identification of the objects as they do not matter in finding a solution. For example, consider having checkpoints to pass through in a package delivery problem or having multiple tables to use when moving the blocks in the blocksworld problem. In the former problem, the choice of which middle point the truck passes through is not important and the same holds for the choice of tables in the latter problem. illustrates how for these objects in the above problems, symmetry breaking cannot help, even if one considers the best possible constraint that steers the solving to only one solution by forbidding choosing an action that uses a non-maximal object among the ordered symmetrical objects. Meanwhile abstracting over these objects helps. The reason behind is that even though one breaks the symmetries, n objects remain in the search space blowing up the search, while with abstraction the number of objects are reduced to one.

5 Conclusion

In this paper, we investigate faithful and uniform abstractions, and their computational complexity. We provide concrete operators for constructing abstractions. Our investigations reveal that for cases of interchangeability, obtaining a uniform abstraction with generalization ability is not feasible; however, faithful abstractions can still be obtained, albeit they may not closely resemble the original program. The notion of semantic indistinguishability captures the cases where it is possible to use the intuitive operator to achieve (faithful) abstractions. Our results indicate that symmetry and abstraction are orthogonal. Symmetry aims to detect (and find ways to reconstruct) interchangeable objects. Abstraction aims at losing the identification of objects. However we show that it is possible to abstract over symmetrical atoms with additional syntactic properties which ensure indistinguishability, and show a case study on its usefulness compared to symmetry breaking which motivates further research into automating the search for indistinguishable symmetries.

Indeed, while we closed open questions in complexity, there are still open gaps; we expect that this work will foster followup studies on different versions of abstractions useful for generalization and their complexity.

Acknowledgments

This research was funded in whole or in part by the Austrian Science Fund (FWF) grant 10.55776/T1315, the Vienna Science and Technology Fund (WWTF) grant 10.47379/ICT25044 (Saribatur); the Austrian Science Fund (FWF) grant J4656, the French Agence nationale de la recherche (ANR) grant ANR-25-CE23-7647 (Hecher); and Excellence Center at Link¨oping - Lund in Information Technology (ELLIIT) funded by the Swedish government and the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation (Fichte).