arXiv CSopen access

2-ASP(Q) programs with weak constraints: Complexity and efficient implementation

Under consideration for publication in Theory and Practice of Logic Programming

1

2-ASP(Q) programs with weak constraints: Complexity and efficient implementation∗

arXiv:2605.27338v1 [cs.AI] 26 May 2026

ANDREA CUTERI

GIUSEPPE MAZZOTTA

FRANCESCO RICCA

University of Calabria, Rende, Italy (e-mail: {andrea.cuteri,giuseppe.mazzotta,francesco.ricca}@unical.it) submitted 1 January 2003; revised 1 January 2003; accepted 1 January 2003

Abstract ASP(Q) extends Answer Set Programming (ASP) with Quantifiers over answer sets. In this paper we focus on the class of ASP(Q) programs with two quantifiers and weak constraints, denoted as 2-ASPw (Q). 2-ASPw (Q) is a practically relevant fragment of ASP(Q) that is expressive enough to capture optimization problems up to the class ∆P 3 . On the theoretical side, we provide a complete complexity characterization of the main computational tasks for 2ASPw (Q) programs, including tight completeness results and the analysis of nontrivial cases that have not been addressed in previous works. On the practical side, we introduce novel strategies for computing (optimal) quantified answer sets in the casper system, that rely on a Counterexample-Guided Abstraction Refinement (CEGAR) technique tailored to ASP(Q). An experimental evaluation on hard benchmarks from different application domains shows that the proposed techniques are effective in practice. KEYWORDS: ASP, Quantified ASP, Combinatorial Optimization Problems

1 Introduction Answer Set Programming (Brewka et al. 2011) (ASP) is a well-established declarative formalism that has been widely adopted for modeling and solving hard combinatorial problems. Over the years, ASP has been successfully applied in a variety of real-world domains, including planning (Son et al. 2023), scheduling (Dodaro et al. 2018; Cardellini et al. 2021), business process management (Chiariello et al. 2024; Fionda et al. 2024), among many others (Eiter et al. 2008). A substantial body of research has focused on extending ASP modeling and solving capabilities, leading to the proposal of several language extensions (Amendola et al. 2019; Bogaerts et al. 2016; Fandinno et al. 2021). Among these, Answer Set Programming with Quantifiers (Amendola et al. 2019) (ASP(Q)) introduces the possibility to quantify over answer sets (Gelfond and Lifschitz 1991). This extension enhances the expressive power of ASP, allowing for the natural modeling of problems spanning the entire Polynomial Hierarchy (PH). ASP(Q) has ∗ This work has been partially funded by the Italian Ministry of Industrial Development (MISE) under project EI-TWIN n. F/310168/05/X56 CUP B29J24000680005 and also partially by projects SIGENERA (CUP J29I24001770005) and MOZART (J49I24001740005) selected within the framework of the PR FESR – FSE Calabria 2021/2027 and implemented with the support of the Italian State and the Calabria Region.

2

A. Cuteri, G. Mazzotta, F. Ricca

found interesting applications in several contexts, including outlier detection (Bellusci et al. 2022), planning (Faber et al. 2022) and related domains (Faber 2024), establishing it as a promising framework for solving problems beyond NP. More recently, ASP(Q) has been extended with weak constraints, denoted by ASPw (Q) (Mazzotta et al. 2024), further enhancing its ability to naturally represent hard optimization problems. Weak constraints in ASPw (Q) can be applied both locally to enable quantification over optimal answer sets, and globally to express preferences among solutions, thus capturing optimization problems throughout the PH. While weak constraints improve the modeling capabilities of ASP(Q), they introduce additional sources of computational complexity, making the design of effective solving techniques challenging (Azzolini et al. 2025). Within this context, we focus on ASP(Q) programs with two quantifiers and weak constraints, denoted as 2-ASPw (Q), which are expressive enough to model complex optiw mization problems up to ∆P 3 . Indeed, the expressive power of 2-ASP (Q) is not yet fully characterized, as existing completeness results are available only for specific language fragments (Mazzotta et al. 2024). As a consequence, the development of efficient and complexity-aware implementations for the entire 2-ASPw (Q) has so far been left unexplored. To fill this gap, this paper undertakes a complexity analysis of the main reasoning tasks for 2-ASPw (Q) programs, namely coherence and brave reasoning, and derives tight completeness results for the general case. Moreover, the paper introduces efficient solving techniques for 2-ASPw (Q). In particular, we propose an efficient evaluation technique based in Counterexample-Guided Abstraction Refinement (CEGAR) (Clarke et al. 2003; Janota et al. 2016), which serves as the foundation for two algorithms computing optimal quantified answer sets. Although inspired by the lower and upper-bound improving strategies used in ASP solvers (Alviano et al. 2020), our lower-bound improving approach departs from existing methods by realizing lower-bound improvement via abstraction refinement instead of unsatisfiable-core extraction, thereby yielding a distinctive and novel technique. Finally, the proposed techniques have been implemented on top of the casper system (Cuteri et al. 2026). Experimental results demonstrate the effectiveness of our approach across several benchmarks drawn from diverse application domains, confirming both its practical viability and its alignment with the theoretical complexity results. 2 Background In this section, we provide some preliminaries and notation on ASP and ASP(Q). 2.1 Answer Set Programming Syntax A term is a constant (i.e., an integer or a string starting with lowercase letter) or a variable (i.e., a string starting with uppercase letter). An atom is an expression of the form p(⃗t) with ⃗t = t1 , . . . , tn being a list of terms and p being a predicate of arity n ≥ 0. An atom p(⃗t) is ground if all terms in ⃗t are constants. A literal is either an atom a or its negation ∼a. The complement of a literal l = a (resp. l = ∼a) is l = ∼a (resp. l = a). Given a set of literals L, L+ (resp. L− ) denotes the set of positive (resp. negative) literals appearing in L. A rule is an expression of the form h ← l1 , . . . , ln where h is an atom referred to as head, and l1 , . . . , ln with n ≥ 0 is a conjunction of literals referred

2-ASP(Q) with weak constraints

3

to as body. A rule with empty body is called fact, while a rule with empty head is called hard constraint. A weak constraint is an expression of the form ←ω l1 , . . . , ln [w@l, ⃗t] where l1 , . . . , ln is a conjunction of literals referred to as body, w and l are terms, and ⃗t = t1 , . . . , tm is a possibly empty list of terms. Given a rule (resp. a weak constraint) r, Hr denotes the set of atoms appearing in the head of r while Br denotes the set of literals appearing in the body of r. A rule r (resp. a weak constraint) is safe if each variable appears in at least one literal in Br+ . A program P is a set of safe rules and weak constraints. Given a program P , R(P ) and W(P ) denote, respectively, the sets of rules and weak constraints appearing in P ; while H(P ) denotes the set of atoms appearing in the head of some rules in P . Given an expression ϵ (atom, program, etc.), at(ϵ) denotes the set of atoms appearing in ϵ. Semantics Given an ASP program P , the Herbrand Universe, HUP , of P is the set of all constants appearing in P ; the Herbrand Base, BP , is the set of all possible ground atoms that can be obtained from predicates and constants in P ; ground(P ) denotes the set of all ground rules that can be obtained from P by proper substitutions of variables in P with constants in HUP . An interpretation I ⊆ BP is a set of atoms. A ground literal l = a (resp. l = ∼a) is true w.r.t. I if a ∈ I (resp. a ∈ / I), false otherwise. A conjunction of literals conj is true w.r.t. I if all the literals in conj are true w.r.t. I, false otherwise. An interpretation I is an answer set of P iff (i) I is a model of P , namely for each rule r ∈ ground(P ) either Hr is true w.r.t. I or Br is false w.r.t. I; and (ii) I is a minimal model of its GL-reduct (Gelfond and Lifschitz 1991). Let AS(P ) be the set of answer set of a program P , then P is coherent iff AS(P ) ̸= ∅. For a program P and an interpretation I, let the set of weak constraint violations be ws(P, I) = {(w, l, ⃗t) | ←ω b1 , . . . , bm [w@l, ⃗t] ∈ ground(P ) and b1 , . . . , bm are true w.r.t. P I}, then the cost function of P is defined as C(P, I, k) = (w,k,⃗ t)∈ws(P,I) w for every integer k. Let M1 , M2 ∈ AS(P ) then M1 is dominated by M2 if there exists an integer l such that C(P, M1 , l) > C(P, M2 , l) and for each l′ > l, C(P, M1 , l′ ) = C(P, M2 , l′ ). Let M ∈ AS(P ) then M is an optimal answer set iff M is not dominated by any M ′ ∈ AS(P ). We denote by OptAS(P ) the set of optimal answer set of P . 2.2 ASP with Two Quantifiers w

A 2-ASP (Q) program (Mazzotta et al. 2024) is an expression of the form □1 P1 □2 P2 : C : C ω , where □1 , □2 are quantifiers in {∃st , ∀st }, P1 , P2 are ASP programs possibly with weak constraints, C is a stratified program (Ceri et al. 1990) with hard constraints, and C ω is a set of weak constraints such that BC ω ⊆ BP1 . Weak constraints appearing P1 and P2 are said local ; whereas those in C ω are said global. A 2-ASPw (Q) program Π is said to be existential if □1 = ∃st , otherwise it is universal. Moreover, Π is said to be alternating if □1 ̸= □2 , and plain if it contains no weak constraints. We now define the semantics of 2-ASPw (Q) programs. Let P be an ASP program and M ⊆ BP , then fixP (M ) denotes the set of facts and hard constraints of the form {a ←| a ∈ M } ∪ {← a | a ∈ BP \ M }. Then, M ∈ AS(P ) satisfies a program P ′ if P ′ ∪ fixP (M ) is coherent. At this point the coherence of 2-ASPw (Q) can be defined as follows: • ∃st P : C : C ω is coherent iff there exists M ∈ OptAS(P ) such that M satisfies C. • ∀st P : C : C ω is coherent iff for each M ∈ OptAS(P ), M satisfies C.

4

A. Cuteri, G. Mazzotta, F. Ricca • ∃st P1 □2 P2 : C : C ω is coherent iff there exists M1 ∈ OptAS(P1 ) such that □2 P2 ∪ fixP1 (M1 ) : C : C ω is coherent. • ∀st P1 □2 P2 : C : C ω is coherent iff for each M1 ∈ OptAS(P1 ), □2 P2 ∪ fixP1 (M1 ) : C : C ω is coherent.

For an existential 2-ASPw (Q) program Π, an optimal answer set M1 ∈ OptAS(P1 ) is a quantified answer set of Π if □2 P2 ∪fixP1 (M1 ) : C : C ω is coherent. We denote by QAS(Π) the set of quantified answer sets of Π. Let Π be an existential 2-ASPw (Q) program, l be an integer, and M ∈ QAS(Π), then the cost of M at level l is defined as C(M, Π, l) = C(M, P1 ∪ C ω , l). Let M1 , M2 ∈ QAS(Π), then M1 is dominated by M2 if there exists l such that C(M1 , Π, l) > C(M2 , Π, l) and for each l′ > l, C(M1 , Π, l′ ) = C(M2 , Π, l′ ). Thus, M is an optimal quantified answer set if M is not dominated by any M ′ ∈ QAS(Π). We denote by OptQAS(Π) the set of optimal quantified answer sets. Example 1 Let Π be a 2-ASPw (Q) program of the form ∃st P1 ∀st P2 : C, where C = {← nb, nc} and     a ← ∼na b ← ∼nb c ← ∼nc ←ω a, ∼c [1@1] P1 = P2 = na ← ∼a nb ← ∼b nc ← ∼c ←ω b, ∼nc [1@1] Let us consider M1 = {na, nb} ∈ AS(P1 ). In this case, {na, nb, nc} ∈ OptAS(P2 ∪ fixP1 (M1 )) violates the constraint ← nb, nc ∈ C. Thus, M1 ∈ / QAS(Π). Conversely, M1′ = {a, nb} ∈ AS(P1 ) is such that P2 ∪ fixP1 (M1′ ) admits only one optimal answer set M2 = {a, nb, c} which satisfies the constraint in C and so M1 ∈ QAS(Π). If we remove weak constraints from P2 , then AS(P2 ∪ fixP1 (M1 )) = {M2 , M2′ } where M2′ = {a, nb, nc}. Here, M2′ violates the constraint in C and so M1 is not a quantified answer set anymore.

3 Complexity Results for 2-ASPw (Q) In this section, we study the main computational tasks for 2-ASPw (Q): Coherence and Brave reasoning. For 2-ASPw (Q) programs, the coherence problem checks whether a program is coherent, while brave reasoning verifies whether an atom occurs in an optimal quantified answer set. Unlike standard ASP, local weak constraints in ASPw (Q) programs introduce an additional source of computational complexity, as observed by Mazzotta et al. (2024). Even though complexity results for these tasks have been established for specific subclasses of ASPw (Q), a complete characterization is still missing. In particular, it was shown that verifying the coherence for 2-ASPw (Q) programs (i) is P P in ΣP 3 for existential programs and in Π3 for universal programs, and (ii) is hard for Σ2 P and Π2 , respectively. Starting from these results, we prove that the coherence problem for 2-ASPw (Q) is complete for the second level of the PH, namely ΣP 2 for existential programs and ΠP for universal programs (full proofs in Appendix B). 2 Theorem 1 (Membership) The coherence problem for 2-ASPw (Q) programs of the form □1 P1 □2 P2 : C is in: ΣP 2 if st st □1 = ∃st ; ΠP otherwise, no matter whether □ = ∃ or □ = ∀ . 2 2 2

2-ASP(Q) with weak constraints

5

Proof (Sketch) To prove our thesis we need to distinguish three different scenarios. Uniform quantifiers □1 = □2 . By applying the transformation (Algorithm 1) by Mazzotta et al. (2024), it is possible to obtain a plain 2-ASP(Q) program Π′ such that Π′ is coherent if and only if Π is coherent. From the result of Amendola et al. (2019), verifying st P the coherence of Π′ is ΣP 2 -complete if □1 = ∃ ; otherwise is in Π2 -complete. Thus the thesis holds for uniform quantifiers. Case □1 = ∃st and □2 = ∀st . In this case, it is possible to translate Π into an existential 2-ASPw (Q) program Π′ where weak constraints appear only in the first subprogram. Since verifying the coherence of Π′ is ΣP 2 -complete (Corollary 3.1 by Mazzotta et al. (2024)), then the thesis holds also in this case. More precisely, the 2-ASPw (Q) program Π′ can be obtained by copying the rules of the program P2 in P1 and then adding rules in the program C for verifying the optimality of an answer sets of P2 . As a result, we obtain Π′ of the form ∃P1′ ∀P2′ : C ′ where: • optimal answer sets M of P1′ are of the form M1 ∪ M2c where M1 is an optimal answer set of P1 and M corresponds to an answer set of P2 ∪ fixP1 (M1 ); • answer sets N of P2′ ∪ fixP1′ (M ) are of the form M1 ∪ M2c ∪ M2 where M1 ∪ M2 is an answer set of P2 ∪ fixP1 (M1 ); • an answer set N of P2′ ∪ fixP1′ (M ) satisfies C ′ if and only if M1 ∪ M2c is not dominated by M1 ∪ M2 and one of the following holds: 1. there exists l such that the cost of M1 ∪ M2 is different from the cost of M1 ∪ M2c ; 2. the cost of M1 ∪ M2 is equal to the cost of M1 ∪ M2c for each level and M1 ∪ M2 satisfies C. Let M = M1 ∪ M2c be an optimal answer set of P1′ . If M is not an optimal answer set of P2 ∪ fixP1 (M1 ), then M cannot be a quantified answer set as there exists N = M1 ∪ M2c ∪ M2 in the answer sets of P2′ ∪ fixP (M ), where M1 ∪ M2 is an optimal answer set of P2 ∪ fixP1 (M1 ) and N violates C ′ since M1 ∪ M2c is dominated by M1 ∪ M2 . On the other hand, since M is an optimal answer set of P2 ∪ fixP1 (M1 ), then for each N = M1 ∪ M2c ∪ M2 in the answer sets of P2′ ∪ fixP1′ (M ), M1 ∪ M2c is not dominated by M1 ∪ M2 (i.e., Condition 1 is always satisfied). Thus, let N = M1 ∪ M2c ∪ M2 be an answer set of P2 ∪ fixP1′ (M ), then N satisfies C ′ if and only if one between conditions 1 and 2 holds. Here we can observe that Condition 1 holds if and only if M1 ∪ M2 is not an optimal answer set of P2 ∪ fixP1 (M1 ); whereas Condition 2 holds if and only if M1 ∪ M2 is an optimal answer set of P2 ∪ fixP1 (M1 ) and M1 ∪ M2 satisfies C. Thus, M is a quantified answer set of Π′ if and only if each optimal answer set M1 ∪ M2 of P2 ∪ fixP1 (M1 ) satisfies C. Hence, M is a quantified answer set of Π′ if and only if M1 is a quantified answer set of Π. Finally, we can conclude that Π is coherent iff Π′ is coherent. Case □1 = ∀st and □2 = ∃st . By following the same working principle as before, it is possible to encode Π into a 2-ASPw (Q) program Π′ which preserves the coherence of Π and in which weak constraints appear only in the first subprogram. In this case, verifying the coherence of Π′ is ΠP 2 -complete (Corollary 3.1 by Mazzotta et al. (2024)), then the thesis holds also in this last case. In this case, the 2-ASPw (Q) program Π′ is of the form ∀P1′ ∃P2′ : C ′ where: • optimal answer sets M of P1′ are of the form M1 ∪ M2c where M1 is an answer set of P1 and M is an answer set of P2 ∪ fixP1 (M1 );

6

A. Cuteri, G. Mazzotta, F. Ricca

• answer sets N of P2′ ∪ fixP1′ (M ) are of the form M1 ∪ M2c ∪ M2 where M1 ∪ M2 is an answer set of P2 ∪ fixP1 (M1 ); • an answer set N of P2′ ∪ fixP1′ (M ) satisfies C ′ if and only if one of the following holds: 1. M1 ∪ M2c is dominated by M1 ∪ M2 ; 2. the cost of M1 ∪ M2 is equal to the cost of M1 ∪ M2c for each level and M1 ∪ M2 satisfies C. According to the ASPw (Q) semantics, Π′ is incoherent if and only if there exists an optimal answer set M1 of P1′ such that for every answer set N of P2′ ∪ fixP1′ (M )), N does not satisfy C ′ . Let M = M1 ∪ M2c be an optimal answer set of P1′ , with M1 ∈ OptAS(P1 ) and M ∈ AS(P2 ∪ fixP1 (M1 )). If M1 ∪ M2c is not an optimal answer set of P2 ∪ fixP1 (M1 ), then there exists M1 ∪ M2 ∈ OptAS(P2 ∪ fixP1 (M1 )) such that M1 ∪ M2c is dominated by M1 ∪ M2 . Consequently, N = M1 ∪ M2c ∪ M2 ∈ AS(P2′ ∪ fixP (M )) is such that Condition 1 is satisfied, and thus M cannot witness the incoherence of Π′ . Otherwise, M1 ∪M2c is optimal for P2 ∪fixP1 (M1 ). In this case, for every N = M1 ∪M2c ∪ M2 ∈ AS(P2′ ∪ fixP1′ (M )), N satisfies C ′ if and only if Condition 2 holds, that is, if and only if M1 ∪ M2 has the same cost of M1 ∪ M2c (i.e., M1 ∪ M2 ∈ OptAS(P2 ∪ fixP1 (M1 ))) and M1 ∪ M2 satisfies C. Therefore, Π′ is incoherent if and only if there exists M1 ∈ AS(P1 ) such that no M1 ∪ M2 ∈ OptAS(P2 ∪ fixP1 (M1 )) satisfies C, which is exactly the condition for Π to be incoherent. Hence, Π′ preserves the coherence of Π. Note that, the presence of weak constraints in both quantified programs do not allow for a simple quantifier elimination, and the existing translation proposed by Mazzotta et al. (2024) requires the introduction of an additional quantifier, resulting in a non necessary jump in complexity to the third level of the PH in case □1 ̸= □2 . Theorem 2 (Hardness) The coherence problem for 2-ASPw (Q) programs of the form □1 P1 □2 P2 : C is hard for: st P st ΣP or □2 = ∀st . 2 if □1 = ∃ ; Π2 otherwise, no matter whether □2 = ∃ Proof (Sketch) Let us consider the different combination of quantifiers separately. (Case □1 = □2 = ∃st ). From Thm 4 by Mazzotta et al. (2024), deciding the coherence of Π is ΣP 2 -complete if W(P1 ) = ∅. Thus, the thesis holds since this is a particular case. (Case □1 = □2 = ∀st ). Let Φ = ∀X∃Y ϕ be a 2-QBF, where X and Y are disjoint set of variables and ϕ is a boolean formula in 3-CNF. Verifying that Φ is true is a ΠP 2complete problem (Schaefer and Umans 2002). We encode in polynomial time any Φ in a 2-ASPw (Q) program of the form ∀st P1 ∀st P2 : C, as detailed in Appendix B. (Case □1 ̸= □2 ). Deciding the coherence of plain alternating 2-ASP(Q) programs ΣP 2complete if □1 = ∃st ; otherwise it is ΠP -complete (Amendola et al. 2019). Since this is 2 w a particular case of 2-ASP (Q) (i.e. W(P1 ) = W(P2 ) = ∅), then the thesis follows. Theorem 3 (Completeness) The coherence problem for 2-ASPw (Q) programs of the form □1 P1 □2 P2 : C is: ΣP 2st st complete if □1 = ∃st ; ΠP -complete otherwise, no matter whether □ = ∃ or □ = ∀ . 2 2 2

2-ASP(Q) with weak constraints

7

Proof The thesis follows from Theorem 1 and 2. From Theorem 3, we derive complete results for the brave reasoning task in 2-ASPw (Q), which asks whether an atom a is true in some optimal quantified answer set. Theorem 4 Let Π be an existential 2-ASPw (Q) program of the form □1 P1 □2 P2 : C : C ω and a be a ground atom, then verifying whether a ∈ M , with M ∈ OptQAS(Π), is ∆P 3 -complete no matter whether □2 = ∃st or □2 = ∀st . These results strengthen those of Mazzotta et al. (2024), as they establish completeness for all combinations of quantifiers, rather than for alternating programs only. 4 Solving 2-ASPw (Q) via CEGAR Counterexample-Guided Abstraction Refinement (CEGAR) (Clarke et al. 2003) is an iterative technique that starts from a simplified system representation (abstraction) and progressively refines it using counterexamples, until a solution is found or non-existence is proven. CEGAR-based techniques were successfully applied to QBF-satisfiability (Janota et al. 2016) and 2-ASP(Q) solving (Cuteri et al. 2026). Building on these ideas, we propose a CEGAR-based approach for the evaluation of 2-ASPw (Q) programs. In the following we give a game-theoretic characterization of the semantics of 2-ASPw (Q) and then we focus on the two stages of CEGAR: abstraction refinement and counterexample search. 4.1 The 2-ASPw (Q) Game Let □ ∈ {∃st , ∀st } be a quantifier, then the opponent of □ is □ = ∀st if □ = ∃st ; otherwise □ = ∃st . Thus, for any alternating 2-ASPw (Q) program □2 is the opponent of □1 , that is, □2 = □1 . In what follows, w.l.o.g., we consider 2-ASPw (Q) programs of the form: □P1 □P2 : C : C ω

(1)

Let Π be a 2-ASPw (Q) program of the form (1), then a move for □ is an answer set M1 ∈ OptAS(P1 ). Given a move M1 for □, for each M2 ∈ OptAS(P2 ∪ fixP1 (M1 )), M2 |H(P2 ) is a candidate countermove to M1 for □. Let M2 ∈ OptAS(P2 ∪ fixP1 (M1 )) be a candidate countermove then M2 |H(P2 ) is effectively a countermove to M1 for □ if: (i) □ = ∃st and M2 does not satisfies C; or (ii) □ = ∀st and M2 satisfies C. A winning move for □ is a move M1 such that no countermove to M1 for □ exists. Thus, □ = ∃st wins if there exists M1 ∈ OptAS(P1 ) such that no countermove to M1 for □ exists. Proposition 1 Let Π be a 2-ASPw (Q) of the form (1), there exists a winning move for □ if and only if (i) □ = ∃st and Π is coherent, or (ii) □ = ∀st and Π is incoherent. Intuitively, the notion of winning moves closely corresponds to the definition of coherence of 2-ASPw (Q) programs. Let Π be a 2-ASPw (Q) program of the form (1), and let M1 be a winning move for □. If □ = ∃st , then there is no M2 ∈ OptAS(P2 ∪ fixP1 (M1 )) such that M2 violates C. This implies that ∀st P2 ∪ fixP1 (M1 ) : C is coherent, and hence Π is coherent. Conversely, if □ = ∀st , then there is no M2 ∈ OptAS(P2 ∪ fixP1 (M1 )) such that M2 satisfies C. Therefore, ∃st P2 ∪ fixP1 (M1 ) : C is incoherent, and thus Π is incoherent.

8

A. Cuteri, G. Mazzotta, F. Ricca 4.2 Counterexample search in 2-ASPw (Q)

Given a 2-ASPw (Q) program Π of the form (1), from Proposition 1, the coherence of Π can be decided by searching for a winning move for □. Thus, the program P1 , whose optimal answer sets coincide with the possible moves of □, is a natural abstraction for Π. Hence, given M1 ∈ OptAS(P1 ), the counterexample search aims at contradicting M1 , which means finding a countermove to M1 for □. To this end, we define the countermove program whose optimal answer sets correspond to countermoves to M1 for □. We recall that countermoves correspond to optimal answer sets of P2 ∪ fixP1 (M1 ) that either satisfy or not the program C according to □. Since C is stratified with hard constraints, it admits one answer set (Dantsin et al. 2001) iff hard constraints are satisfied. Thus, the following transformation can be used to capture the incoherence of C. Definition 1 (Complement of stratified program) Let P be a stratified ASP program with hard constraints, then the complement of P , denoted by ¬P , is obtained from P by (i) transforming hard constraints ← l1 , . . . , ln into rules of the form v ← l1 , . . . , ln ; and (ii) adding an hard constraint of the form ← ∼v.

Proposition 2 Given a stratified ASP program P , its complement ¬P is coherent iff P is incoherent. At this point, if □ = ∃st (resp. □ = ∀st ) one might be tempted to define the counterexample program as P2 ∪ ¬C ∪ fixP1 (M1 ) (resp. P2 ∪ C ∪ fixP1 (M1 )). However, an optimal answer set of such a counterexample program may correspond to a non-optimal answer set of P2 ∪ fixP1 (M1 ) that violates (resp. satisfies) C, which does not correspond to a countermove for □ to M1 . To address this issue, we need to relax hard constraints from C into weak constraints with a lower priority level w.r.t. weak constraints in P2 . Definition 2 (Relaxed program) Let P be a stratified program with hard constraints, l be an integer, and unsat be a fresh atom not appearing anywhere else. Then relaxed(P, l) is defined as:   ← Br . ∀r ∈ P s.t.Hr ̸= ∅   Hr relaxed(P, l) = unsat ← Br . ∀r ∈ P s.t.Hr = ∅   w ← unsat.[1@l] Intuitively, relaxed(·, ·) is similar to ¬C but the fresh atom introduced as head of the hard constraints of P is used to assign a penalty if P is incoherent. As a result, relaxed(·, ·) has the following property, which is fundamental in the computation of countermoves. Proposition 3 Given a stratified ASP program P with hard constraints, and an integer l, relaxed(P, l) is always coherent. Thanks to the above property, the program relaxed(¬C, l) (resp. relaxed(C, l)) can be combined with P2 in such a way that rules in ¬C (resp. C) do not filter out any optimal answer set of P2 ∪fixP1 (M1 ). Thus, we are now ready to define the countermove program.

2-ASP(Q) with weak constraints

9

Definition 3 (Countermove program) Let Π be a 2-ASPw (Q) of the form (1) and lmin be the smallest priority level among weak constraints in P2 , then the countermove program for Π is ctr(Π) = P2 ∪relaxed(¬C, lmin − 1) if □ = ∃st ; otherwise ctr(Π) = P2 ∪ relaxed(C, lmin − 1). Note that, the above definition aligns with the countermove definition from Section 4.1. Specifically, when □ = ∃st , a countermove must violate C, so the countermove program incorporates rules from relaxed(¬C, lmin − 1). Conversely, when □ = ∀st , a countermove must satisfy C, so the countermove program incorporates rules from relaxed(C, lmin −1). Consequently, countermoves to a move for □ are given by the optimal answer sets of the counterexample program. Proposition 4 Let Π be a 2-ASPw (Q) program of the form (1) and M1 ∈ OptAS(P1 ) be a move for □. There exists M2 ∈ OptAS(ctr(Π) ∪ fixP1 (M1 )) such that unsat ∈ / M2 if and only if M2 |H(P2 ) is a countermove to M1 for □. 4.3 Refining abstractions in 2-ASPw (Q) The next step in designing our CEGAR-based approach for 2-ASPw (Q) is to define a transformation for refining the abstraction according to known countermoves. Specifically, let M1 be a move for □ and M2 be a countermove for □, then the goal of the refinement, namely Ref (Π, M2 ), is to obtain a set of rules such that optimal answer sets of P1 ∪ Ref (Π, M2 ) correspond to moves M1′ for □ such that M2 is not a countermove to M1′ for □. Note that, M2 is not a countermove to M1′ for □ if one of the these condition holds: 1. there is no M2′ ∈ AS(P2 ∪ fixP1 (M1′ )) such that M2′ |H(P2 ) = M2 ; 2. there exists M2′ ∈ AS(P2 ∪ fixP1 (M1′ )) such that M2′ |H(P2 ) = M2 but M2′ ∈ / OptAS(P2 ∪fixP1 (M1′ )) (i.e. M2′ is dominated by some answer set of P2 ∪fixP1 (M1′ )); 3. there exists M2′ ∈ OptAS(P2 ∪fixP1 (M1′ )) such that M2′ |H(P2 ) = M2 but M2′ satisfies C and □ = ∃st (resp. violates C and □ = ∀st ). Thus, we define some transformations encoding these conditions to refine our abstraction. First of all, we need a predicate substitution function that maps each predicate p to a fresh one of the form pα β , where α and β are strings, to obtain rules over a fresh signature for each discovered countermove. More in detail, let L be a set of literals and ϵ be an ASP expression (i.e. rule, program, etc.), then σβα (L, ϵ) denotes the expression obtained from ϵ by mapping each positive (resp. negative) literal p(⃗t) ∈ L (resp. ∼p(⃗t) ∈ L) with ⃗ ∼ α ⃗ pα β (t) (resp. pβ (t)). Now, we are ready to define the rules which verify Condition 1. Definition 4 (Check Answer Set) Let P be an ASP program and M be an interpretation, then checkAS(P, M ) is:  − σM (H(P ), {a ← |a ∈ M })    + −   ∀r ∈ P, H(r) ̸= ∅  σM (H(P ), σM (H(P ), r))   + − f ailM ← σM (H(P ), σM (H(P ), B(r))) ∀r ∈ P, H(r) = ∅ checkAS(P, M ) = − ∼ ⃗  f ailM ← p(⃗t)+ ∀ p(⃗t) ∈ H(P )  M , p(t)M   − + ⃗ ⃗  f ailM ← p(t)M , ∼p(t)M ∀ p(⃗t) ∈ H(P )    asM ← ∼f ailM

10

A. Cuteri, G. Mazzotta, F. Ricca

Basically, checkAS(P, M ) encodes the GL-reduct of a program P w.r.t. an interpretation M and checks whether M is a ⊂-minimal model of the reduct. Specifically, M is encoded as facts over a fresh negative signature (i.e., each atom p(⃗t) ∈ M is represented by a fact ⃗ p− M (t) ←). Atoms over the negative signature are used to rewrite negative body literals, yielding the GL-reduct of P w.r.t. M ; whereas head atoms and positive body literals ⃗ are mapped to a fresh positive signature (i.e., p(⃗t) mapped to p+ M (t)). Finally, if the true atoms over positive and negative signatures coincide then M is an answer set of P . We can now focus on Condition 2 which requires checking answer set optimality. To this end, we define a transformation to compute the cost of answer sets of an ASP program. Definition 5 (Cost Program) Let P be an ASP program, L be the set of priority levels in W(P ), and vP and clP are fresh predicates not appearing in P . Then, cost(P ) is defined as:  vP (w, l, ⃗t) ← l1 , . . . , ln ∀ ←ω l1 , . . . , ln [w@l, ⃗t] ∈ P cost(P ) = clP (T , l) ← #sum{C, ⃗t : vP (C, l, ⃗t)} = T ∀l ∈ L Intuitively, weak constraints of the form ←ω l1 , . . . , ln [w@l, ⃗t] can be rewritten into rules whose head is a fresh atom encoding violation tuples (i.e. (w, l, ⃗t)); and introduces a rule for each level l that sums up the the weights of the violation tuples at level l. To verify the optimality of an answer set M ∈ AS(P ), it is necessary to compare its cost with that of every M ′ ∈ AS(P ). To this end, we use clone(P ) = σclone (H(P ) ∪ H(P ), P ), which clones the program P , enabling the comparison between the cost of M and the cost of all answer sets of the cloned program. Definition 6 (Dominated program) Let P1 and P2 be two ASP programs, then checkDom(P1 , P2 ) is the following program: dif fP1 ,P2 (L) ← clP1 (C1, L), clP2 (C2, L), C1 ̸= C2. hasHigherP1 ,P2 (L) ← dif fP1 ,P2 (L), dif fP1 ,P2 (L1), L < L1. highestP1 ,P2 (L) ← dif fP1 ,P2 (L), ∼hasHigherP1 ,P2 (L). domP1 ,P2 ← highestP1 ,P2 (L), clP1 (C1, L), clP2 (C2, L), C2 < C1 where clP1 and clP2 are, respectively, the predicates introduced by cost(P1 ) and cost(P2 ); whereas dif fP1 ,P2 , hasHigherP1 ,P2 , highestP1 ,P2 , and domP1 ,P2 are fresh predicates. Intuitively, let M ∈ AS(P ) and Mc ∈ AS(clone(P )), then checkDom(P, clone(P )) can be used to compare the cost of M and Mc . More precisely, cost(P ) and cost(clone(P )) compute, respectively, the cost of M and Mc , for each level l, as atoms of the form clP (C, l) and clclone(P ) (C, l). Thus, rules from dom(P, clone(P )) derive domP,clone(P ) if and only if M is dominated by Mc , which means M is not an optimal answer set of P . Finally, we can focus on Condition 3. Recall that Condition 3 requires to verify the coherence (resp. incoherence) of the program C. To this end, it is possible to leverage relaxed(C, l) (resp. relaxed(¬C, l)), as we have seen for counterexample program. Now that, we have transformations for each condition (i.e., Condition 1, 2, and 3), we need to control the activation of the different transformations in the refinement process. Definition 7 (Controlled program) Let P be a program and l a literal s.t. at(l) ∈ / BP , then or(P, l) = {Hr ← Br , l | r ∈ P }.

2-ASP(Q) with weak constraints

11

Intuitively, or(P, l) controls the activation of P according to the literal l. If l is true, it can be removed from rules in or(P, l), obtaining back the program P ; otherwise rules in or(P, l) are satisfied as l falsifies rules’ body. We can now define the refinement program. Definition 8 (Refinement Program) Let Π be a 2-ASPw (Q) program of the form (1), M be a move for □ and let CE be a countermove to M for □. The refinement program is defined as follows:   checkAS(P2 , CE)         ←w asCE [1@lmin − 1]         CE   or(cost(P2 ), asCE )      or(clone(R(P )), as )  2 CE ref (Π, CE) = or(cost(clone(P2 )), asCE )         CE   or(checkDom(P2 , clone(P2 )), asCE )       w   ∼domP CE ,clone(P ) [1@lmin − 2] ← as ,   CE 2   2   − ′ ′ or(σCE (lits(P2 ) ∪ lits(C ), C ), asCE ) − where P2CE = σCE (lits(P2 ), P2 ), lits(P2 ) = H(P2 ) ∪ H(P2 ), asCE is the predicate introduced by checkAS(P2 , CE), C ′ = relaxed(C, lmin − 3) if □ = ∃st ; otherwise C ′ = relaxed(¬C, lmin − 3), lits(C ′ ) = H(C ′ ) ∪ H(C ′ ), and lmin is the smallest priority level among weak constraints of P1 .

Let Π be a 2-ASPw (Q) of the form (1), M be a move for □ and CE be a countermove to M for □, then we aim at computing a new move M ′ for □ such that CE is not a countermove to M ′ for □. To this end, we use ref (Π, CE) to check Conditions 1-3. More precisely, rules in checkAS(P2 , CE) encode the reduct of P2 w.r.t. CE, and derive the atom asCE iff there exists M2 ∈ AS(P2 ∪ fixP1 (M ′ )) such that M2 |H(P2 ) = CE (i.e., Condition 1 is not satisfied). Thus, the weak constraint ←ω asCE [1@lmin − 1] expresses the preference to satisfy Condition 1. If Condition 1 is not satisfied, then there exists M2 ∈ AS(P2 ∪ fixP1 (M ′ )) such that M2 |H(P2 ) = CE and so asCE is derived as true. At this point, asCE activates the following blocks which check Conditions 2 and 3. To check Condition 2, or(cost(P2CE ), asCE ) computes the cost of M2 w.r.t. weak constraints in P2 ; or(clone(R(P2 )), asCE ) clones the program P2 to compare pair of answer set of P2 ∪fixP1 (M ′ ); or(cost(clone(P2 )), asCE ) computes the cost of an answer set of the cloned program; and finally or(checkDom(P2CE , clone(P2 )), asCE ) derive the atom domP2 ,clone(P2 ) iff M2 is not optimal as M2 is dominated by some answer set of the cloned program. As a result, the weak constraint ←w asCE , ∼domP2CE ,clone(P2 ) [1@lmin − 2] prefers answer sets of the cloned program that dominate M2 (i.e., M2 is not optimal). If M2 cannot be dominated by any answer set of the cloned program then M2 is optimal − and so or(σCE (lits(P2 )∪lits(C ′ ), C ′ ), asCE ) checks Condition 3. In particular, if □ = ∃st st (resp. □ = ∀ ), then the atom unsat is derived iff M2 does not satisfy C (resp. ¬C), which means Condition 3 is not satisfied. Thus, the weak constraint ←ω unsat, asCE [1@lmin −3] in C ′ models the preference of satisfying C (resp. ¬C) (i.e. Condition 3 is satisfied). Thus, if there exists an optimal answer set of P1 ∪ ref (Π, CE) that satisfies at least one weak constraint in ref (Π, CE) then this corresponds to a move M ′ that does not admit CE as countermove. A detailed example is provided in Appendix C.2.

12

A. Cuteri, G. Mazzotta, F. Ricca 5 Computing Optimal Quantified Answer Sets

Computing optimal (quantified) answer sets requires algorithms that make multiple oracle calls to search for such answer sets (Alviano et al. 2020; Azzolini et al. 2025). Quantified Answer Set Computation The computation of quantified answer sets in presence of weak constraints can be obtained by plugging the transformations defined in previous section in the CEGAR for 2-ASP(Q) algorithm by Cuteri et al. (2026). In particular, we update both counterexample search and refinement procedure with those introduced in Section 4.2 (i.e., Definitions 3 and 8), and update the conditions of existence of a winning move accordingly. Indeed, in the original algorithm it was sufficient to check for existence of an answer set of the refined or counterexample programs, whereas here we have to look at the cost of their optimal answer sets. More in detail, at the least three levels the cost 1 if no winning exists; whereas for the counterexample program at the last level the cost is 1 if the current move is winning (full algorithm in Appendix D). Upper-bound improving Optimal quantified answer sets can be computed starting from a quantified answer set and iteratively searching for better ones until the incoherence is met (Alviano et al. 2020). A quantified answer set M of the input program Π is computed applying CEGAR for 2-ASPw (Q), and the cost of M is our initial upper bound. Note that if M does not exist, no optimal quantified answer set exists and the search stops immediately. Next, to improve on this bound a constraint is added to Π to enforce a preference for answer sets of P1 (i.e. candidate quantified answer sets) with a lower cost, and the solver is called again. The process repeats until the upper bound cannot be improved anymore, and the last quantified answer set is optimal. Lower-bound improving The core idea of these strategies is to fix an initial lower-bound cost and, if no answer set within this bound exists, iteratively relax the program to raise the bound until an optimal solution is obtained. Traditional ASP solvers start by treating all weak constraints as hard, aiming for a zero-cost lower bound. If no answer set exists, unsatisfiable cores guide the progressive relaxation of the program, incrementally raising the lower bound (roughly admitting some weak constraint must be violated) until an optimal solution is found (Alviano et al. 2020). Unluckily, this strategy cannot be ported as it is in our setting, since a notion of unsatisfiable core has never been defined for ASPw (Q). Thus, we propose alternative ways for targeting a lower bound, and also for relaxing the program so that the lower bound improves iteratively until the optimum is found. Intuitively, we aim to compute an answer set of P1 that is optimal with respect to the global weak constraints. This is achieved by adding the global weak constraints C ω to P1 with the lowest priority and searching for the optimum answer sets of the resulting program P1lower . Note that, an optimum answer set of P1lower is a reasonable lower bound candidate, since it is either an optimum for Π or it does not satisfy the subsequent quantifiers. In the latter case, following the CEGAR approach, an oracle call is used to compute a countermove, and the corresponding refinement is added to P1lower . This enables the next iteration to search for a new candidate optimal answer set. The procedure repeats until a winning move is found, incrementally improving the lower bound by discarding candidates that are not quantified answer sets of Π. To ensure

2-ASP(Q) with weak constraints

13

the correctness of the approach the global weak constraints W are moved at the lowest priority levels w.r.t. both local weak constraints in P1 and weak constraints that would be added to P1lower by the refinement procedure. More precisely, the initial abstraction is defined as P1 ∪ W , where W = {←ω l1 , . . . , lk [w@λ + l, ⃗t] |←ω l1 , . . . , lk [w@l, ⃗t] ∈ C ω }, with λ being an integer such that levels from C ω are remapped to strictly lower priority levels w.r.t. lmin −3 (i.e., the smallest priority level added by the refinement), and lmin being the lowest priority level in P1 . In this way, the first winning move will be a quantified answer set which is also optimal. Note that the proposed ordering of priority levels in the (refined) abstraction is essential: it first favors moves that admit no known countermove and only then prefers moves that are optimal with respect to C ω . Under this ordering, the first winning move obtained is an optimal quantified answer set. 6 Implementation and Experiments We run an experimental campaign on an Intel(R) Xeon(R) CPU E7-8880 v4 @ 2.20GHz, running Debian GNU/Linux 12, with memory and CPU (i.e., user+system) limited to 8GB and 800s. Benchmarks and executables are available at https://osf.io/gmnjx Implementation The proposed approach was implemented on top of the casper (Cuteri et al. 2026). More in detail, casper is written in Python and uses clingo (Gebser et al. 2016) as an oracle for computing moves and countermoves. For non-alternating 2-ASPw (Q) programs, our implementation applies the transformations proposed by Mazzotta et al. (2024) for removing weak constraints, as the 2-ASPw (Q) game is defined for alternating programs. Specifically, non-alternating 2-ASPw (Q) programs are translated into 2-ASP(Q) program with two alternating quantifiers and no local weak constraints. Benchmarks We considered several benchmarks from diverse ASP(Q) applications (Faber et al. 2023; Azzolini et al. 2025; Azzolini et al. 2025): Propositional Abduction Problem (PAP) (Eiter and Gottlob 1995), Minmax Clique (MMC) (Cao et al. 1995), Max Term Deletion (MTD) (Schaefer and Umans 2002), Most Probable Explanation in Probabilistic ASP (MPE) (Azzolini et al. 2025), and Clique Coloring (CC) (Schaefer and Umans 2002). For PAP, we consider three reasoning tasks: pap-opt, pap-rel, and pap-nec, corresponding to computing cardinality-minimal solutions, and relevant and necessary hypotheses, respectively. For MMC we considered both the decision and optimization variant of the problem, namely mmc-bound and mmc-opt. For MTD, we considered the optimization version. Finally, for MPE we considered both coloring and smokers domains (Azzolini et al. 2025). For the CC benchmark, we considered graphs of varying size (from 10 to 120 nodes) and edge density (25%, 50%, and 75%), generated according to the Erdős–Rényi model provided by NetworkX library (https: //pypi.org/project/networkx). For each combination of size and density, we generated 10 instances. For the other benchmarks, instances were drawn from previous experiments (Cuteri et al. 2026; Azzolini et al. 2025; Azzolini et al. 2025). Compared methods In our evaluation we compared the approach by Azzolini et al. (2025) implemented in pyqasp. Note that, pyqasp implements the upper-bound improving algorithm on top of a rewriting in QBF and it uses quabs (https://github.com/

14

A. Cuteri, G. Mazzotta, F. Ricca Bench

#inst

TT

pap-opt mtd coloring smokers mmc-opt pap-nec pap-rel mmc-bound cc

294 80 94 99 45 294 294 225 420

opt opt opt opt opt coh coh coh coh

Sol. 123 50 11 99 44 282 294 225 370

casper-l Sum t.(s) 6450.78 1698.24 896.93 83.54 3565.79 2675.68 2053.67 919.39 5555.22

casper-u Sum t.(s) 9725.87 3916.51 114.35 3130.97 2912.66 2675.68 2053.67 919.39 5555.22

Sol. 33 74 8 19 42 282 294 225 370

#opt 367 1184 105 3724 106 -

Sol. 101 48 25 14 5 -

pyqasp Sum t.(s) 18076.72 6451.46 3621.92 1845.59 904.65 -

#opt 410 253 278 152 5 -

Table 1: Overall results ltentrup/quabs) as backend solver. Then, we consider also the proposed techniques denoted as casper-u (upper-bound improving) and casper-l (lower-bound improving).

Results Obtained results are summarized in Table 1 which reports, for each benchmark, the number of instances (#inst), the type of task (TT) (opt for optimal answer set and coh for coherence), and, for each system, the number of solved instances (Sol.), total execution time (Sum t,(s)), and number of optimization steps (#Opt.). This latter is the sum of the number of quantified answer sets found to reach the solution; it is omitted for lower-bound improving, and is not meaningful for local-weak-constraints-only problems. We first focus on the benchmarks containing only local weak constraints, namely: pap-nec, pap-rel, and mmc-bound. Observe that, in these cases, pyqasp could not be run (it does not support local weak constraints), and casper-l and casper-u clearly coincide, since the first winning move is the solution. For these benchmarks, nearly all instances were solved by casper within 2 minutes (only 12 of 813 timed out), confirming effectiveness of the systems herein introduced. To further assess the scalability of casper, we considered the CC benchmark. In particular, we compare casper with an enumeration-based solver, denoted as nested-aspq, which evaluates programs by enumerating answer sets of each subprogram according to the 2-ASPw (Q) semantics. Figure 2 reports the execution times of the systems for graphs with fixed edge density. Instances are sorted by increasing graph size, and each point (x, y) represents the average runtime y (over 10 generated instances) required by a system on graphs with x nodes and a given edge density. 1,600 casper-u casper-l pyqasp

600 400 200 0

0

50 100 150 200 250 300 Number of solved instances

Fig. 1: Overall execution time - opt

Execution time(s)

Execution time(s)

800

casper-0.25 casper-0.50 casper-0.75 nested-aspq-0.25 nested-aspq-0.50 nested-aspq-0.75

1,200 800 400 0

0

40 80 Number of nodes

120

Fig. 2: Solving time for CC The generated instances are hard to solve and nested-aspq is unable to scale beyond

2-ASP(Q) with weak constraints

15

graphs with 30 nodes, regardless of the edge density. In contrast, casper exhibits significantly better scalability, solving instances with up to 120 nodes. Furthermore, the edge density has a noticeable impact on casper runtime. For dense graphs, the runtime is considerably small, as dense graphs admits few maximal cliques and so the number of possible counterexample is reduced. Conversely, for sparse graphs, the runtime increases, due to the larger number of maximal cliques, which in turn leads to a higher number of counterexamples to be explored. Let’s now shift the attention to optimum quantified answer set search. For mtd and coloring, the upper-bound improving strategy, implemented in pyqasp and casper-u, is preferred over the lower-bound improving strategy adopted by casper-l. The ASPbased casper-u is preferable to the QBF-based pyqasp in mtd, whereas the opposite holds for coloring. Diving in the details, pyqasp could compute for coloring quantified answer sets that are closer to the optimum so requiring few optimization steps; on the other hand casper-u shows a faster computation of quantified answer sets leading to better performance. On the other hand, casper-l likely computes many locally optimal moves that are not quantified answer sets, thus resulting slower than upper-bound improving alternatives. Conversely, for pap-opt, mmc-opt, and smokers, casper-l solves substantially more instances than the others (146 more than pyqasp and 172 more than casper-u), since locally optimal moves frequently correspond to optimal solutions. Overall, casper-l solves 134 more instances than pyqasp, and 151 more instances than casper-u with a lower average runtime. Figure 1 reports a traditional cactus plot on all the instances, confirming casper-l is the most effective system overall.

7 Related Work Many ASP extensions have been proposed for modeling hard combinatorial optimization problems. The standard ASP construct for expressing optimization problems is weak constraints (Buccafurri et al. 2000), which is equivalent to optimize statements (Gebser et al. 2012). The ASPw (Q) language is based on the same construct, but expands the modeling capabilities of ASP in the entire PH. For alternative formalism to ASP(Q), such as stable-unstable (Bogaerts et al. 2016) and quantified ASP (Fandinno et al. 2021), we are not aware of any extension considering optimization statements explicitly. Optimization in ASP might also be handled within the asprin framework (Brewka et al. 2023), which however targets preference modeling. An in-depth comparison of ASP(Q) with these formalism was provided by Amendola et al. (2019) and Fandinno et al. (2021). Among ASP(Q) systems, we mention qasp (Amendola et al. 2022), pyqasp (Faber et al. 2023), and casper (Cuteri et al. 2026). The first two are based on a translation of ASP(Q) in QBF, they support an arbitrary number of quantifiers, but originally lacked support for weak constraints. Recently, pyqasp was extended to handle global weak constraints using an upper-bound improving strategy (Azzolini et al. 2025), though local weak constraints remain unsupported. casper (Cuteri et al. 2026) is the only CEGARbased ASP(Q) system and originally supported only 2-ASP(Q) programs without weak constraints. This paper extends casper to support local and global weak constraints, yielding the first implementation capable of evaluating 2-ASPw (Q) programs. Solvers for ASPw (Q) exploit optimization strategies used in ASP solvers (Alviano et al. 2020),

16

A. Cuteri, G. Mazzotta, F. Ricca

however our lower-bound improving approach departs from existing methods by realizing improvements via abstraction refinement. 8 Conclusion w

This paper focuses on 2-ASP (Q), the class of ASPw (Q) programs with two quantifiers, for which tight complexity bounds and concrete implementations were previously missing. We fill this gap by providing a detailed complexity analysis and establishing tight completeness results: coherence checking is complete for the second level of the PH (i.e., P ΣP 2 for existential programs and Π2 for universal ones), while reasoning over optimal quantified answer sets is ∆P 3 -complete. Moreover, building on the CEGAR framework, we developed two optimization techniques based on lower- and upper-bound improvement strategies. Experimental results demonstrate the effectiveness of our approach, advancing the state of the art in 2-ASPw (Q) solving. Future work includes extending both the complexity analysis and evaluation techniques to ASPw (Q) programs with an arbitrary number of quantifiers. References Alviano, M., Dodaro, C., Marques-Silva, J., and Ricca, F. 2020. Optimum stable model search: algorithms and implementation. J. Log. Comput. 30, 4, 863–897. Amendola, G., Cuteri, B., Ricca, F., and Truszczynski, M. 2022. Solving problems in the polynomial hierarchy with ASP(Q). In LPNMR. LNCS, vol. 13416. 373–386. Amendola, G., Ricca, F., and Truszczynski, M. 2019. Beyond NP: quantifying over answer sets. TPLP 19, 5-6, 705–721. Azzolini, D., Leone, N., Mazzotta, G., and Ricca, F. 2025. Solving hard combinatorial optimization problems with pyqasp. N. Amin and J. Arias, Eds. LNCS, vol. 16401. Springer, 199–217. Azzolini, D., Mazzotta, G., Ricca, F., and Riguzzi, F. 2025. Most probable explanation in probabilistic answer set programming. In Proceedings of IJCAI 2025. 9049–9057. Bellusci, P., Mazzotta, G., and Ricca, F. 2022. Modelling the outlier detection problem in ASP(Q). In PADL. LNCS, vol. 13165. Springer, 15–23. Bogaerts, B., Janhunen, T., and Tasharrofi, S. 2016. Stable-unstable semantics: Beyond NP with normal logic programs. TPLP 16, 5-6, 570–586. Brewka, G., Delgrande, J. P., Romero, J., and Schaub, T. 2023. A general framework for preferences in answer set programming. Artif. Intell. 325, 104023. Brewka, G., Eiter, T., and Truszczynski, M. 2011. Answer set programming at a glance. Commun. ACM 54, 12, 92–103. Buccafurri, F., Leone, N., and Rullo, P. 2000. Enhancing disjunctive datalog by constraints. TKDE 12, 5, 845–860. Cao, F., Du, D.-Z., Gao, B., Wan, P.-J., and Pardalos, P. M. 1995. Minimax Problems in Combinatorial Optimization. Boston, MA, 269–292. Cardellini, M., Nardi, P. D., Dodaro, C., Galatà, G., Giardini, A., Maratea, M., and Porro, I. 2021. A two-phase ASP encoding for solving rehabilitation scheduling. In RuleML+RR. LNCS, vol. 12851. Springer, 111–125. Ceri, S., Gottlob, G., and Tanca, L. 1990. Logic Programming and Databases. Surveys in computer science. Chiariello, F., Fionda, V., Ielo, A., and Ricca, F. 2024. A direct ASP encoding for declare. In PADL. Lecture Notes in Computer Science. Springer, 116–133.

2-ASP(Q) with weak constraints

17

Clarke, E. M., Fehnker, A., Han, Z., Krogh, B. H., Ouaknine, J., Stursberg, O., and Theobald, M. 2003. Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. Found. Comput. Sci. 14, 4, 583–604. Cuteri, A., Mazzotta, G., and Ricca, F. 2026. 2-asp(q) solving based on cegar. Proceedings of the AAAI Conference on Artificial Intelligence 40, 23 (Mar.), 19030–19038. Dantsin, E., Eiter, T., Gottlob, G., and Voronkov, A. 2001. Complexity and expressive power of logic programming. ACM Computing Surveys 33, 3, 374–425. Dodaro, C., Galatà, G., Maratea, M., and Porro, I. 2018. Operating room scheduling via answer set programming. In AI*IA. LNCS, vol. 11298. Springer, 445–459. Eiter, T., Fink, M., Greco, G., and Lembo, D. 2008. Repair localization for query answering from inconsistent databases. ACM Trans. Database Syst. 33, 2, 10:1–10:51. Eiter, T. and Gottlob, G. 1995. The complexity of logic-based abduction. J. ACM 42, 1, 3–42. Faber, W. 2024. Solving argumentation problems using answer set programming with quantifiers: Preliminary report. In ICLP Workshops. CEUR, vol. 3799. CEUR-WS.org. Faber, W., Mazzotta, G., and Ricca, F. 2023. An efficient solver for ASP(Q). TPLP 23, 4, 948–964. Faber, W., Morak, M., and Chrpa, L. 2022. Determining action reversibility in STRIPS using answer set programming with quantifiers. In PADL. LNCS, vol. 13165. Springer, 42–56. Faber, W., Pfeifer, G., and Leone, N. 2011. Semantics and complexity of recursive aggregates in answer set programming. Artif. Intell. 175, 1, 278–298. Fandinno, J., Laferrière, F., Romero, J., Schaub, T., and Son, T. C. 2021. Planning with incomplete information in quantified answer set programming. TPLP 21, 5, 663–679. Fionda, V., Ielo, A., and Ricca, F. 2024. Ltlf2asp: Ltlf bounded satisfiability in ASP. In LPNMR. Lecture Notes in Computer Science. Springer, 373–386. Garey, M. R. and Johnson, D. S. 1979. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman. Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T., and Wanko, P. 2016. Theory solving made easy with clingo 5. In ICLP (Technical Communications). OASIcs, vol. 52. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2:1–2:15. Gebser, M., Kaminski, R., Kaufmann, B., and Schaub, T. 2012. Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers. Gelfond, M. and Lifschitz, V. 1991. Classical negation in logic programs and disjunctive databases. New Gener. Comput. 9, 3/4, 365–386. Janota, M., Klieber, W., Marques-Silva, J., and Clarke, E. M. 2016. Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1–25. Lifschitz, V. and Turner, H. 1994. Splitting a logic program. In Proc. of ICLP 1994. 23–37. Mazzotta, G., Ricca, F., and Truszczynski, M. 2024. Quantifying over optimum answer sets. TPLP 24, 4, 716–736. Papadimitriou, C. H. 1994. Computational complexity. Addison-Wesley. Schaefer, M. and Umans, C. 2002. Completeness in the polynomial-time hierarchy: A compendium. SIGACT news 33, 3, 32–49. Son, T. C., Pontelli, E., Balduccini, M., and Schaub, T. 2023. Answer set planning: A survey. TPLP 23, 1, 226–298. Stockmeyer, L. J. 1976. The polynomial-time hierarchy. Theor. Comput. Sci. 3, 1, 1–22.

18

A. Cuteri, G. Mazzotta, F. Ricca Appendix A Extended Preliminaries A.1 Complexity Classes

In this section, we recall some basic definitions of complexity classes that are used to study the complexity of 2-ASPw (Q). For further details about N P -completeness and complexity theory we refer the reader to dedicated literature (Papadimitriou 1994). We recall that P P the classes ∆P k , Σk , and Πk of the polynomial time hierarchy (PH)(Stockmeyer 1976) are defined as follows (rf. Garey and Johnson (1979)): P P ∆P 0 = Σ0 = Π0 = P

and, for all k > 0 P

P

P

Σk Σk Σk ∆P , ΣP , ΠP , k+1 = P k+1 = N P k+1 = coN P P NP where, N P = ΣP . 1 , coN P = Π1 , and ∆2 = P C C In general, P (resp. N P ) denotes the class of problems that can be solved in polynomial time on a deterministic (resp. nondeterministic) Turing machine with an oracle in the class C. Note that, the usage of an oracle O ∈ C for solving a problem π is referred to as a subroutine call, during the evaluation of π, to O. The latter is evaluated in a unit of time.

A.2 Answer Set Programming Syntax. A term is a constant (i.e., an integer or a string starting with lowercase letter) or a variable (i.e., a string starting with uppercase letter). A standard atom is an expression of the form p(⃗t) with ⃗t = t1 , . . . , tn being a list of terms and p being a predicate of arity n ≥ 0. A standard atom p(⃗t) is ground if all terms in ⃗t are constants. A standard literal is either a standard atom a or its negation ∼a. An aggregate element is a pair t1 , . . . , tn : conj where t1 , . . . , tn is a list of terms and conj is a conjunction of standard literals. An aggregate atom is of the form f {e1 , . . . , en } ≺ t, where f ∈ {#count, #sum} is an aggregate function, ≺∈ {<, ≤, >, ≥, =} is a comparison operator, t is a term called guard, and e1 , . . . , en is a list of aggregate elements. An atom can be either a standard atom or an aggregate atom. A literal is either an atom (positive literal) or its negation (negative literal). The complement of a literal l is denoted by l. The complement of a literal l = a is ∼a, while the complement of a literal l = ∼a is a. Given a set of literals L, L+ (resp. L− ) denotes the set of positive (resp. negative) literals appearing in L. A normal rule is an expression of the form h ← l1 , . . . , ln where h is standard atom referred to as head, and l1 , . . . , ln with n ≥ 0 is a conjunction of literals referred to as body. A normal rule with empty body is called fact, while a normal rule with empty head is called hard constraint or strong constraint. A weak constraint is an expression of the form ←w l1 , . . . , ln [w@l, ⃗t] where l1 , . . . , ln are literals referred to as body, w and l are terms, and ⃗t = t1 , . . . , tm is a possibly empty list of terms. A rule r is either a normal rule or a weak constraint. Given a rule r, Hr denotes the set of atoms appearing in the head of r while Br denotes the set of atoms appearing in the body of r. Given an expression ϵ (atom, rule, etc.), V(ϵ) denotes the set of variables appearing in ϵ. For a normal rule r the global variables of r are the variables appearing in Hr , in standard literals in Br or as the guard of aggregate literals of the form f {e1 , . . . , en } = V . A normal rule r is safe if (i)

2-ASP(Q) with weak constraints

19

its global variables appear at least in one positive standard literal, and (ii) each variable appearing in an aggregate element e is either a global variable or appears in some positive literal in e. A weak constraint r is safe if it respects the safety condition for normal rules and variables in V(w) ∪ V(l) ∪ V(⃗t) also appear in at least one positive standard literal in the body. A program P is a set of safe rules. Given a program P , R(P ) and W(P ) denote the sets of normal rules and weak rules appearing in P , respectively, while H(P ) denotes the set of atoms appearing as heads of rules in P . Given an expression ϵ (atom, rule, program, etc.), at(ϵ) denotes the set of atoms appearing in ϵ. A choice rule is of the form {e1 ; . . . ; en } ← l1 , . . . , lm , where e1 ; . . . ; en are called choice elements and l1 , . . . , lm are literals. A choice element ei is of the form ai : bi1 , . . . , bik with ai being a standard atom and bi1 , . . . , bik being standard literals. A program P with choice rules can be rewritten into a program without choice rules. More in detail, each choice element ei can be seen as the pair of rules ai ← bi1 , . . . bim , l1 , . . . lm , ∼nai and nai ← bi1 , . . . bim , l1 , . . . lm , ∼ai , with nai being a fresh predicate not appearing in P . Semantics. Given an ASP program P , the Herbrand Universe, HUP , of P is the set of all constants appearing in P ; the Herbrand Base, BP , is the set of all possible ground atoms that can be constructed using predicates from P and constants from HUB ; ground(P ) denotes the set of all ground rules that can be obtained from P by proper substitutions of variables in P with constants in HUP . An interpretation I ⊆ HBP is a set of standard atoms. A ground standard literal l = a (resp. l = ∼a) is true w.r.t. I if a ∈ I (resp. a ∈ / I), false otherwise. A conjunction of standard literals conj is true w.r.t. I if all the literals in conj are true w.r.t. I, false otherwise. For a given set of aggregate elements S = {e1 ; . . . ; en }, eval(S, I) denotes the set of tuples (t1 , . . . , tm ) such that there exists an aggregate element ei ∈ S of the form t1 , . . . , tm : conj and conj is true w.r.t. I; I(S) denotes the multi-set [t1 |(t1 , . . . , tm ) ∈ eval(S, I)]. A ground aggregate literal of the form f {e1; . . . ; en } ≺ t (resp. ∼f {e1; . . . ; en } ≺ t) is true w.r.t. I if f (I(e1 ; . . . ; en )) ≺ t holds (resp. does not hold); otherwise is false. An interpretation I is an answer set of a program P iff (i) I is a model of P , namely for each rule r ∈ ground(P ) either the head of r is true w.r.t. I or the body of r is false w.r.t. I; and (ii) I is a minimal model of its FLP-reduct (Faber et al. 2011). Let AS(P ) be the set of answer set of a program P then P is coherent iff AS(P ) ̸= ∅. For a program P and an interpretation I, let the set of weak constraint violations be ws(P, I) = {(w, l, T ) | ←ω b1 , . . . , bm [w@l, ⃗t] ∈ ground(P ) and b1 , . . . , bm are true w.r.t. P I}, then the cost function of P is defined as C(P, I, k) = (w,k,T )∈ws(P,I) w for every integer k. Let M1 , M2 ∈ AS(P ) then M1 is dominated by M2 if there exists an integer l such that C(P, M1 , l) > C(P, M2 , l) and for each l′ > l, C(P, M1 , l′ ) = C(P, M2 , l′ ). Let M ∈ AS(P ) then M is an optimal answer set iff M is not dominated by any M ′ ∈ AS(P ). We denote by OptAS(P ) the set of optimal answer set of P .

Appendix B Full proof of Complexity Results The coherence problem for ASPw (Q) programs has been investigated in recent years (Mazzotta et al. 2024), but several complexity-theoretic results are still missing. Mazzotta et al. (2024) studied the complexity of ASPw (Q) when weak constraints are used both glob-

20

A. Cuteri, G. Mazzotta, F. Ricca

ally (i.e. to define optimal quantified answer sets) and locally (i.e. within the different subprograms). In particular, the following results have been established. Theorem 5 (Thm 2 by Mazzotta et al. (2024)) The coherence problem of a 2-ASP(Q) with weak constraints is in: (i) ΣP 3 for existential programs; (ii) ΠP for universal programs. 3 Theorem 6 (Thm 3 by Mazzotta et al. (2024)) The coherence problem of a 2-ASP(Q) with weak constraints is hard for: (i) ΣP 2 for existential programs; (ii) ΠP for universal programs. 2 Starting from this results we further studied the complexity for 2-ASPw (Q) to provide complete results for such class of ASPw (Q) programs. More precisely, we focus on the general case of ASPw (Q) programs where weak constraints appears locally within each ASP programs. To present our result we first introduce some notation which will be instrumental in the proofs. First of all, we recall the notion of splitting set by Lifschitz and Turner (1994). Definition 9 Let P be an ASP program and U ⊆ BP . Then U is a splitting set for P if for each rule r ∈ P such that H(r) ⊆ U then also at(r) ⊆ U . Intuitively, a splitting set U for a program P allows to split the program P into two programs referred to as bottom, denoted by bU (P ), and top, denoted by tU (P ). More precisely, bU (P ) contains all those rules r ∈ P such that at(r) ⊆ U , and tU (P ) contains all the remaining rules, that is, tU (P ) = P \ bU (P ). Let U and X ⊆ U be two set of atoms eU (P, X) denotes the program obtained from rules r ∈ P such that Br+ ∩ U ⊆ X and Br− ∩ X = ∅, by removing all literals in Br whose atom is in U . By exploiting the notion of splitting set, the task of computing an answer set of P can be divided in two stages. The following theorem formalizes such intuition. Theorem 7 (Lifschitz and Turner (1994)) Let P be a program and U be a splitting set for P then M ∈ AS(P ) if and only if M = X ∪ Y where X ∈ AS(bU (P )) and Y ∈ eU (tU (P ), X). Example 2 Let P be the following program: a ← b, not c b ← c, not a c← Then U = {c} is a splitting set for P , with bU (P ) = {c ←}. Here the program bU (P ) has only one answer set that is X = {c} and the program eU (tU (P ), X) contains only the rule b ← not a. As a result, the program eU (tU (P ), X) has only one answer set that is Y = {b}, and so, M = X ∪ Y = {c, b} is the unique answer set of P . In what follows, we leverage the notion of splitting set to obtain some relevant properties of the program transformation we are going to introduce. The first program transformation guarantees the coherence of an ASP program.

2-ASP(Q) with weak constraints

21

Definition 10 Let P be an ASP program then sat(P ) denotes the program:  Hr ← Br , not sat ∀r ∈ P sat(P ) = {sat} ← Intuitively, for each ASP program P , the transformation sat(P ) prevents P from being incoherent as it introduces a choice rule over the fresh atom sat which controls the activation of the rules in P . If sat is chosen as true, then all the rules of P are trivially satisfied as not sat appears in all rules’ body. On the contrary, if sat is chosen as false, then sat(P ) is coherent if and only if P is coherent as not sat can be removed from the body of each rule. Observation 1 Let P be an program, then AS(sat(P )) = {{sat}} ∪ AS(P ). Example 3 Let P and sat(P ) be the following programs:   {sat} ←          a ← not b, not sat  sat(P ) = b ← not a, not sat        c ← not d, not sat    d ← not c, not sat Here it is important to observe that the choice rule {sat} ← is a shorthand for the normal rules sat ← not nsat and nsat ← not sat where nsat is a fresh atom not appearing anywhere else. In particular, {sat} is trivially an answer set. On the other hand, if we pick {a, c} ∈ AS(P ) it is to see the {nsat, a, c} ∈ AS(sat(P )). In general, since the atom nsat does not appear anywhere else then it is customary in the literature to consider it as an hidden atom and so, with a slightly abuse of notation we can state that AS(sat(P )) = {{sat}} ∪ AS(P ).      a ← not b    b ← not a P =    c ← not d    d ← not c

Thanks to such a property, we can deal with incoherent ASP programs and preserve the ASP(Q) semantics by proper program transformations. Lemma 1 Let P1 and P2 be two ASP programs such that H(P2 ) ∩ at(P1 ) = ∅, then M ∈ AS(P1 ∪ sat(P2 )) iff M is of the form M1 ∪ M2 where M1 ∈ AS(P1 ) and M2 ⊆ H(sat(P2 )) is either equal to {sat} or M2 is such that M1 ∪ M2 ∈ AS(P2 ∪ fixP1 (M1 )). Proof Since H(P2 )∩at(P1 ) = ∅, then U = at(P1 ) is a splitting set of P = P1 ∪sat(P2 ). Thus M ∈ AS(P ) iff M = X ∪ Y , where X ∈ AS(bU (P )) = AS(P1 ) and Y ∈ AS(eU (tU (P ), X)) = AS(eU (sat(P2 ), X)). Let X ∈ AS(P1 ), then the program eU (sat(P2 ), X) is obtained from rules in sat(P2 ) that have no body literals over at(P1 ) which are false w.r.t. to X and by removing all the literals over atoms in at(P1 ). Since the atom sat does not appear in P1 , then the choice rule {sat} remains as it is and the literal not sat is not removed from any rule. As a result, eU (sat(P2 ), X) is of the form: {sat} Hr ← Br , not sat

∀r ∈ eU (P2 , X)

22

A. Cuteri, G. Mazzotta, F. Ricca

Thus, eU (sat(P2 ), X) = sat(eU (P2 , X)), and so Y ∈ AS(sat(eU (P2 , X))) iff Y = {sat} or Y ∈ AS(eU (P2 , X)). As a result, M ∈ AS(P ) iff M = X ∪ Y where X ∈ AS(P1 ) and Y is either equal to {sat} or Y ∈ AS(eU (P2 , X)). In particular, if Y ∈ AS(eU (P2 , X)), then M = X ∪ Y ∈ AS(P2 ∪ fixP1 (X )) since U is also a splitting set for P2′ = P2 ∪ fixP1 (X ) and so M ∈ AS(P2′ ) iff X ∈ AS(bU (P2′ )) = AS(fixP1 (X )) = {X} and Y ∈ AS(eU (tU (P2′ ), X)) = AS(eU (P2 , X)). Thus, the thesis follows. Lemma 2 Let P1 and P2 be two ASP programs such that H(P2 ) ∩ at(P1 ) = ∅ and W1 be a set of weak constraints such that at(W1 ) ⊆ at(P1 ) then M ∈ OptAS(P1 ∪ W1 ∪ sat(P2 )) iff M is of the form M1 ∪ M2 where M1 ∈ OptAS(P1 ∪ W1 ) and M2 ⊆ H(sat(P2 )) is either equal to {sat} or M2 is such that M1 ∪ M2 ∈ AS(P2 ∪ fixP1 (M1 )). Proof Let P = P1 ∪ W1 ∪ sat(P2 ). From Lemma 1, M ∈ AS(P ) iff M is of the form M1 ∪ M2 , where M1 ∈ AS(P1 ) and M2 is either equal to {sat} or M2 is such that M1 ∪ M2 ∈ AS(P2 ∪ fixP1 (M1 )). Thus, by contradiction, let us assume that there exists M = M1 ∪ M2 ∈ OptAS(P ) such that M1 ∈ / OptAS(P1 ). At this point, we can construct an answer set M ′ = M1′ ∪ M2′ ∈ AS(P ) such that M1 ∈ OptAS(P1 ). Since at(W1 ) ⊆ BP1 then the cost of M and M ′ is given, respectively, by M1 and M1′ . Since M1 ∈ / OptAS(P1 ) and ′ ′ M1 ∈ OptAS(P1 ), then M1 is dominated by M1 and consequently M is dominated by M ′ . This is a contradiction as M ∈ OptAS(P ) and so M cannot be dominated by any answer set of P . Thus, the thesis follows. The next transformation we propose is used to obtain a clone of an ASP program, so that we can duplicate an ASP program in order to compare the cost of two answer sets of a given program. To this end, we need a predicate substitution function that maps each predicate p with a fresh ones of the form pα β , where α and β are strings. More in detail, let L be a set of literals and ϵ be an ASP expression (i.e. rule, program, etc.), then σβα (L, ϵ) denotes the expression obtained from ϵ by mapping each positive (resp. negative) ⃗ ∼ α ⃗ literal p(⃗t) ∈ L (resp. ∼p(⃗t) ∈ L) with pα β (t) (resp. pβ (t)). Let P be an ASP program, then clone(P ) = σclone (H(P ) ∪ H(P ), P ), which generates a clone of the program P . Intuitively, a clone of an ASP program P is obtained by mapping all the predicates defined in P (i.e. appearing in some rule head) to a clone signature (i.e. pclone ) not appearing anywhere else; whereas all the other predicates are kept in their original form as they can be seen as input predicates. As a result, the clone transformation preserves the answer sets of the program P by mapping atoms in H(P ) to fresh atoms over the clone signature. Observation 2 Let P be an ASP program, then M ∈ AS(P ) if and only if {pclone (. . .) | p(. . .) ∈ H(P ) ∩ M }. Lemma 3 Let P1 and P2 be two ASP programs such that H(P2 ) ∩ at(P1 ) = ∅, M1 ∈ AS(P1 ), and M = M1 ∪M2 be an answer set of P = P1 ∪sat(clone(P2 )). Then, M ′ ∈ AS(P2 ∪fixP (M )) iff M ′ is of the form M2 ∪ M2′ , with M2′ ∈ AS(P2 ∪ fixP1 (M1 )).

2-ASP(Q) with weak constraints

23

Proof Let P = P1 ∪ sat(clone(P2 )) and A = H(sat(clone(P2 ))), then BP = BP1 ∩ A, with BP1 ∪ A = ∅. To this end, for each M ∈ AS(P ), M = M1 ∪ M2 where M1 ⊆ BP1 and M2 ⊆ A. More precisely, from Lemma 1, M1 ∈ AS(P1 ) and M2 is either equal to {sat} or M2 is such that M1 ∪ M2 is an answer set of clone(P2 ) ∪ fixP1 (M1 ). Thus, let M = M1 ∪ M2 ∈ AS(P ), with M1 ∈ AS(P1 ), then fixP (M ) = fixP1 (M1 ) ∪ fixA (M2 ). Since atoms in A do not appear neither in P2 nor in fixP1 (M1 ), then A is a splitting set for P2′ = P2 ∪ fixP (M ) = P2 ∪ fixP1 (M1 ) ∪ fixA (M2 ). Thus, M ′ ∈ AS(P2′ ) iff M ′ = X ∪ Y where X is an answer set of bA (P2 ) = fixA (M2 ) and Y is an answer set of eA (tU (P2′ ), X) = eA (P2 ∪ fixP1 (M1 ), X). Here, fixA (M2 ) has only one answer set, that is M2 ; whereas eA (P2 ∪fixP1 (M1 ), X) = P2 ∪fixP1 (M1 ) since none of the atoms in X appears in P2 ∪ fixP1 (M1 ) and so no rule can be simplified according to X. Thus, M ′ ∈ AS(P2′ ) iff M ′ = M2 ∪ Y where Y ∈ AS(P2 ∪ fixP1 (M )). Finally, the last transformation is used to compute the cost of an answer set as atoms over a fresh predicate cost/2. Definition 5 (Cost Program) Let P be an ASP program, L be the set of priority levels in W(P ), and vP and clP are fresh predicates not appearing in P . Then, cost(P ) is defined as:  vP (w, l, ⃗t) ← l1 , . . . , ln ∀ ←ω l1 , . . . , ln [w@l, ⃗t] ∈ P cost(P ) = ⃗ ⃗ clP (T , l) ← #sum{C, t : vP (C, l, t)} = T . ∀l ∈ L Basically, Definition 5 is a revised version of the check transformation by Mazzotta et al. (2024), where each weak constraint is transformed into a rule whose head atoms represent the violation tuples of the weak constraint, and then the each rule with aggregate sums up all the weights assigned to each violation at level l. Example 4 Let P and W be of the form:     ←ω a, c [1@1]  a ← not b            ←ω a, d [2@1] b ← not a W = P =  c ← not d    ←ω b, c [1@2]         ←ω b, d [2@2] d ← not c In this case, the optimization levels are 1 and 2 and so cost(P ∪ W ) is of the form: vP (1, 1) ← a, c vP (2, 1) ← a, d vP (1, 2) ← b, c vP (2, 2) ← b, d costP (C, 1) ← #sum{1 : vP (1, 1), 2 : vP (2, 1)} = C costP (C, 2) ← #sum{1 : vP (1, 2), 2 : vP (2, 2)} = C As a result, the cost(P ) transformation returns a set of rules which serves as post processing to compute the cost of an answer set of P w.r.t. a set of weak constraints W . The cost of the answer set at each level l is denoted by auxiliary atoms of the form cost(c, l). We are now ready to study the complexity of the coherence problem of 2-ASP(Q).

24

A. Cuteri, G. Mazzotta, F. Ricca

Theorem 1 (Membership) The coherence problem for 2-ASPw (Q) programs of the form □1 P1 □2 P2 : C is in: ΣP 2 if st st □1 = ∃st ; ΠP otherwise, no matter whether □ = ∃ or □ = ∀ . 2 2 2 Proof For the sake of the presentation, in what follows we keep separate weak constraints from rules of ASP subprogram. Thus, we consider 2-ASPw (Q) programs of the form □1 P1 ∪ W1 □2 P2 ∪ W2 : C, where P1 and P2 are ASP programs without weak constraints; whereas W1 and W2 are set of weak constraints. To prove our thesis we need to distinguish three different scenarios. Uniform quantifiers □1 = □2 . By applying the transformation (Algorithm 1) by Mazzotta et al. (2024), it is possible to obtain an alternating plain 2-ASP(Q) program Π′ of the form □1 P1′ □1 P2′ : C ′ such that Π′ is coherent if and only if Π is coherent. From st the result of Amendola et al. (2019), verifying the coherence of Π′ is in ΣP 2 if □1 = ∃ ; P otherwise is in Π2 . Thus the thesis holds for uniform quantifiers. Case □1 = ∃st and □2 = ∀st . In this case, Π can be encoded into a plain 2-ASP(Q) program. Such translation requires two steps: first of all we remove weak constraints in W2 , thus obtaining a 2-ASP(Q) program Π′ where weak constraint occurs only in the first program. Then, by applying the transformation (Algorithm 1) by Mazzotta et al. (2024), we get rid of weak constraint in W1 and obtain a plain 2-ASP(Q) program that is coherent iff and only if Π is coherent. Let us now focus on the first step. To remove weak constraint in W2 while preserving the coherence of Π we can construct a 2-ASP(Q) Π′ of the form ∃st P1 ∪ W1 ∪ sat(clone(P2 ))∀st P2 : C ′ , where C ′ = cost(clone(P2 ∪ W2 )) ∪ cost(P2 ∪ W2 ) ∪ C opt , and C opt is of the form: dif f (L) ← cost(C1, L), constclone (C2, L), C1 ̸= C2 hasHigher(L1) ← dif f (L1), dif f (L2), L2 > L1 highest(L) ← dif f (L), not hasHigher(L) domclone ← highest(L), constclone (C1, L), cost(C2, L), C1 > C2 dif f Cost ← dif f (L) equalCost ← not dif f Cost Hr ← Br , equalCost ← domclone ← sat

∀r ∈ C

Intuitively, P1 ∪ W1 ∪ sat(clone(P2 )) augments P1 ∪ W1 with a clone of P2 which always admits an answer set, the program P2 is kept in its original form, and, finally, the program C ′ computes the cost of answer sets of sat(clone(P2 )) and P2 , respectively. Moreover, the program C ′ contains also the rules which: • compare the cost of the two answer sets and derive an atom of the form dif f (l) iff the cost of the compared answer sets differs at level l, and as consequence the atom dif f Cost is derived as well; • derive an atom of the form highest(l) if and only if l is the highest level at which the cost of the two answer sets differs;

2-ASP(Q) with weak constraints

25

• derive an atom domclone iff the answer set of clone(P2 ) is dominated by the answer set of P2 ; • derive an atom equalCost if and only if there is no level at which the cost of the two answer sets differs, and thus the two answer sets have the same cost. Finally, the atom equalCost is used to control the activation of the rules from the original constraint program C. More precisely, if equalCost is derived as false, then all the rules of C are trivially satisfied. On the contrary, if equalCost is derived as true, then all the rules of C are obtained back as equalCost can be removed from all rules bodies. We now prove that Π is coherent if and only if Π′ is coherent. (⇒) We assume Π to be coherent and we prove that Π′ is coherent as well. Since Π is coherent, then there exists M1 ∈ OptAS(P1 ∪ W1 ) such that ∀st P2 ∪ W2 ∪ fixP1 (M1 ) : C is coherent. This means that either P2 ∪fixP1 (M1 ) is incoherent (if there are no answer sets then the forall check is trivially satisfied) or there is no optimal answer set of P2 ∪ W2 ∪ fixP1 (M1 ) that violates the program C. In both cases, we will show that it is possible construct a quantified answer set of Π′ , and so Π′ is coherent as well. We recall that Π′ is of the form ∃st P1 ∪ W1 ∪ sat(clone(P2 ))∀st P2 : C ′ . • P2 ∪ fixP1 (M1 ) is incoherent. In this case, we show that M = M1 ∪ {sat} is a quantified answer set of Π′ . From Lemma 2, M is an optimal answer set of P = P1 ∪ W1 ∪ sat(clone(P2 )), and so, to prove that M is also a quantified answer set of Π′ , we show that ∀st P2 ∪ fixP (M ) : C is coherent. From Lemma 3, M ′ ∈ AS(P2 ∪ fixP (M )) iff M ′ is of the form {sat} ∪ M2′ , with M2′ ∈ AS(P2 ∪fixP1 (M1 )). Since P2 ∪fixP1 (M1 ) is incoherent, then AS(P2 ∪fixP1 (M1 )) = ∅ and so P2 ∪ fixP (M ) is incoherent as well. Thus, ∀st P2 ∪ fixP (M ) : C is coherent and M is a quantified answer set of Π′ . • No optimal answer set of P2 ∪ W2 ∪ fixP1 (M1 ) violates C. Let M2c ⊆ H(sat(clone(P2 ))) be such that M1 ∪M2c ∈ OptAS(clone(P2 ∪W2 )∪fixP1 (M1 )), then we are going to show that M = M1 ∪ M2c is a quantified answer set of Π′ . Let P = P1 ∪ W1 ∪ sat(clone(P2 )), then, from Lemma 1, M ∈ OptAS(P ) and so M is a quantified answer set of Π′ iff ∀st P2 ∪ fixP (M ) : C ′ is coherent. From Lemma 3, M ′ is an answer set of P2 ∪fixP (M ) iff M ′ is of the form M2c ∪M2′ , where M2′ ∈ AS(P2 ∪fixP1 (M1 )). Thus, let M ′ = M2c ∪ M2′ ∈ AS(P2 ∪ fixP (M )), we show that M ′ satisfies C ′ . First of all, we observe that the constraint ← sat ∈ C ′ is trivially satisfied as sat is false w.r.t. M . Moreover, we observe that since M is optimal w.r.t. weak constraint in W2 , then M is not dominated by M ′ . This means that domclone is derived as false and the constraint ← domclone is satisfied. Finally, we need to prove that all the rules of the form Hr ← Br , equalCost in C ′ , with r ∈ C, are satisfied w.r.t. M ′ . To this end, we need to distinguish two cases depending on whether M2′ is optimal or not w.r.t. weak constraint W2 . If M2′ is not optimal then M ′ is dominated by M and so there exists a level l such that the cost of M ′ is greater than the cost of M . Thus, the cost of M ′ is not equal to the cost of M and so the atom equalCost is derived as false. Since equalCost appears positively in all the remaining rules, then they are satisfied w.r.t. M ′ . On the other hand, when M2 is optimal, then M ′ and M have the same cost for each level l and so the atom equalCost is derived as true. This means that for each r ∈ C, Hr ← Br , equalCost ∈ C ′ is satisfied w.r.t. M ′ iff Hr ← Br is satisfied w.r.t. M ′ which means the constraint program C is

26

A. Cuteri, G. Mazzotta, F. Ricca

satisfied w.r.t. M ′ . Since none of the atoms in H(sat(clone(P2 ))) appears in C, then C is satisfied w.r.t. M ′ = M2c ∪ M2′ iff C is satisfied w.r.t. M2′ . By assumption, no optimal answer set of P2 ∪ W2 ∪ fixP1 (M1 ) violates C and so C is satisfied w.r.t. M2′ and C ′ is satisfied also w.r.t. M ′ . Here we observe that M ′ was chosen arbitrarily among answer set of P2 ∪ fixP (M ) and M ′ satisfies C ′ . Thus, this means that C ′ is satisfied w.r.t. each M ′ ∈ AS(P2 ∪ fixP (M )) and so M is a quantified answer set of Π′ . (⇐) We assume Π′ to be coherent and we prove that Π is coherent as well. Let P = P1 ∪ W1 ∪ sat(clone(P2 )), then there exists M ∈ AS(P ) such that ∀st P2 ∪ fixP (M ) : C ′ is coherent. From Lemma 2, M is of the form M1 ∪ M2c where M1 ∈ OptAS(P1 ∪ W1 ) and M2c is either equal to {sat} or M2c is such that M1 ∪ M2c ∈ AS(clone(P2 ) ∪ fixP1 (M1 )). Thus, to prove the coherence of Π, we are going to show that M1 is quantified answer set of Π. • M2c = {sat}. Since ∀st P2 ∪ fixP (M ) : C ′ is coherent and C ′ contains the constraint ← sat, then P2 ∪ fixP (M ) is incoherent. From Lemma 3, we know that M ′ ∈ AS(P2 ∪ fixP (M )) if and only if M ′ is of the form {sat} ∪ M2′ , with M2′ ∈ AS(P2 ∪ fixP1 (M1 )). Since P2 ∪ fixP (M ) is incoherent, then P2 ∪ W2 ∪ fixP1 (M1 ) is incoherent as well, and thus, ∀st P2 ∪ W2 ∪ fixP1 (M1 ) : C is coherent and M1 is a quantified answer set of Π. • M = M1 ∪ M2c ∈ AS(clone(P2 ) ∪ fixP1 (M1 )). Let M2 ∈ OptAS(P2 ∪ W2 ∪ fixP1 (M1 )). From Lemma 3, we know that M ′ = M2c ∪ M2 ∈ AS(P2 ∪ fixP (M )), and so, by assumption, M ′ satisfies C ′ . So this means the each rule of C ′ is satisfied. More precisely, the constraint ← sat is satisfied as the atom sat is false w.r.t. M ; to satisfy the constraint ← domclone then M cannot be dominated by M ′ and so M is optimal w.r.t. weak constraints in clone(P2 ∪ W2 ). At this point, the last rules to satisfy from C ′ are of the form Hr ← Br , equalCost, with r ∈ C. Since both M and M ′ are optimal, then the cost of M is equal to the cost of M ′ for each level l and thus the atom equalCost is derived as true. This means that, Hr ← Br , equalCost is satisfied w.r.t. M ′ iff Hr ← Br is satisfied w.r.t. M ′ . Since none of the atoms in H(sat(clone(P2 ))) occurs in C, then Hr ← Br is satisfied w.r.t. M ′ = M2c ∪ M2 iff Hr ← Br is satisfied w.r.t. M2 . So this means the the constraint program C is satisfied w.r.t. M2 . Since M2 was chosen arbitrarily among optimal answer sets of P2 ∪ W2 ∪ fixP1 (M1 ), it follows that every optimal answer set of P2 ∪ fixP1 (M1 ) satisfies C, and so M1 is a quantified answer set of Π. Thus, we can conclude that Π is coherent iff Π′ is coherent. At this point, we observe that Π′ contains weak constraints only in the first program. Thus, by applying the transformations by Mazzotta et al. (2024) (i.e. col5 (·)) it is possible to obtain a plain 2-ASP(Q) program Π′′ of the form ∃st P1′′ ∀st P2′′ : C ′′ which is coherent iff Π′ is coherent. Since verifying the coherence of Π′′ is a ΣP 2 -complete problem (Amendola et al. 2019), then the thesis holds in this case. Case □1 = ∀st and □2 = ∃st . As in the previous case, Π can be encoded into a plain 2-ASP(Q) program. Again, the translation requires two steps: first of all we remove weak constraints in W2 , thus obtaining a 2-ASP(Q) program Π′ where weak constraints occur only in the first program. Then, by applying the transformations by Mazzotta et al. (2024), we get rid of weak constraints in W1 and obtain a plain 2-ASP(Q) program which is coherent iff and only if Π is coherent.

2-ASP(Q) with weak constraints

27

More precisely, the 2-ASP(Q) program Π can be encoded into a 2-ASP(Q) program Π′ of the form ∀st P1 ∪sat(clone(P2 ))∃st P2 : C ′ , where C ′ = cost(clone(P2 ∪W2 ))∪cost(P2 ∪ W2 ) ∪ C opt , and C opt is of the form: dif f (L) ← cost(C1, L), constclone (C2, L), C1 ̸= C2 hasHigher(L1) ← dif f (L1), dif f (L2), L2 > L1 highest(L) ← dif f (L), not hasHigher(L) domclone ← constclone (C1, L), cost(C2, L), C1 > C2 dif f Cost ← highest(L) equalCost ← not dif f Cost ← not domclone , not equalCost, not sat Hr ← Br , not domclone , not sat

∀r ∈ C

More precisely, Π is incoherent iff Π′ is incoherent. (⇒) Let us assume Π to be incoherent, then we show that Π′ is incoherent as well. Since Π is incoherent, then there exists M1 ∈ OptAS(P1 ∪ W1 ) such that ∃st P2 ∪ W2 ∪ fixP1 (M1 ) : C is incoherent. Thus, to prove the incoherence of Π′ , we construct a witness of its incoherence, that is M ∈ OptAS(P ), with P = P1 ∪ W1 ∪ sat(clone(P2 )), such that ∃st P2 ∪ fixP (M ) : C ′ is incoherent. More in detail, since ∃st P2 ∪W2 ∪fixP1 (M1 ) : C is incoherent, then either P2 ∪fixP1 (M1 ) is incoherent or there is no optimal answer set of P2 ∪ W2 ∪ fixP1 (M1 ) that satisfies C. Let us distinguish the two cases separately. • P2 ∪ fixP1 (M1 ) is incoherent. In this case, we construct an answer set M = M1 ∪ {sat} that serve as witness for the incoherence of Π′ . Specifically, from Lemma 2, M = M1 ∪ {sat} ∈ OptAS(P ). Moreover, from Lemma 3, M ′ ∈ AS(P2 ∪ fixP (M )) if and only if M ′ is of the form {sat} ∪ M2′ , with M2′ ∈ AS(P2 ∪ fixP1 (M1 )). Since P2 ∪ fixP1 (M1 ) is incoherent, then AS(P2 ∪ fixP1 (M1 )) = ∅, and AS(P2 ∪ fixP (M )) = ∅. As a result, P2 ∪ fixP1 (M1 ) is incoherent and M is a witness for the incoherence of Π′ . • There is no optimal answer set of P2 ∪ W2 ∪ fixP1 (M1 ) that satisfies C. Let M2c ⊆ H(sat(clone(P2 ))) be such that M1 ∪M2c ∈ OptAS(clone(P2 ∪W2 )∪fixP1 (M1 )). Then, from Lemma 2, M = M1 ∪ M2c ∈ OptAS(P ), thus we need to prove that M is a witness for the incoherence of Π′ . To this end, we show that there is no M ′ ∈ AS(P2 ∪ fixP (M )) that satisfies C ′ . More precisely, from Lemma 3, M ′ ∈ AS(P2 ∪ fixP (M )) iff M ′ is of the form M2c ∪ M2′ , with M2′ ∈ AS(P2 ∪ fixP1 (M1 )). Thus, let M ′ = M2c ∪ M2′ ∈ AS(P2 ∪ fixP (M )), with M2′ ∈ AS(P2 ∪ fixP1 (M1 )), we show that M ′ violates C ′ . To this end, we distinguish two possible cases depending on whether M2′ is optimal w.r.t. weak constraints in W2 or not. If M2′ is optimal, then the cost of M is equal to the cost of M ′ for each level l, and so the atom equalCost is derived as true. Since equalCost is true, then the constraint ← not domclone , not equalCost, not sat is satisfied. Moreover, since the atom sat is false w.r.t. M and the atom domclone is derived as false as M is not dominated by M ′ , then each rule Hr ← Br , not domclone , not sat ∈ C ′ , with r ∈ C, is satisfied w.r.t. M ′ iff Hr ← Br is satisfied w.r.t. M ′ . Since none of the atoms in H(sat(clone(P2 ))) appears in C, then Hr ← Br is satisfied w.r.t. M ′ = M2c ∪ M2′ iff Hr ← Br is satisfied w.r.t. M2′ which means M2′ satisfies the constraint program C. By assumption, M2′ does not satisfy C and so C ′ is not satisfied w.r.t. M ′ .

28

A. Cuteri, G. Mazzotta, F. Ricca

Conversely, if M2′ is not optimal then M ′ is dominated by M and so, there exists at least on level l such that the cost of M ′ at level l is greater than the cost of M at level l. As a result, the atom equalCost is derived as false. Moreover, both atoms sat and domclone are derived as false since sat is false w.r.t. M and M is optimal w.r.t. weak constraints in clone(P2 ∪ W2 ) and so M cannot be dominated by M ′ . As a result, the constraint ← not domclone , not equalCost, not sat is violated and so C ′ is not satisfied w.r.t. M ′ . Since in both cases M ′ violates C ′ and M ′ can be any answer set of P2 ∪ fixP (M ), then no answer set of P2 ∪ fixP (M ) satisfies C ′ and thus M = M1 ∪ M2c is a witness for the incoherence of Π′ . (⇐) Let us assume that Π′ is incoherent, then we show that Π is incoherent as well. More precisely, since Π′ is incoherent, then there exists M ∈ OptAS(P ), with P = P1 ∪ W1 ∪ sat(clone(P2 )), such that ∃st P2 ∪ fixP (M ) : C ′ is incoherent. From Lemma 2, M is of the form M1 ∪ M2c , where M1 ∈ OptAS(P1 ∪ W1 ) and M2c ⊆ H(sat(clone(P2 ))) is either equal to {sat} or it is such that M1 ∪ M2c ∈ AS(clone(P2 ) ∪ fixP1 (M1 )). Thus, to prove the incoherence of Π, we are going to show that M1 is a witness for the incoherence of Π in both cases. • (M = M1 ∪ {sat}) Since the atom sat is true w.r.t. M and sat appears negatively in each constraint in C ′ , then the only way for making ∃st P2 ∪ fixP (M ) : C ′ be incoherent is that P2 ∪ fixP (M ) is incoherent. From Lemma 3, M ′ ∈ AS(P2 ∪fixP (M )) iff M ′ is of the form {sat}∪M2′ , with M2′ ∈ AS(P2 ∪ fixP1 (M1 )). Since P2 ∪ fixP (M ) is incoherent, then AS(P2 ∪ fixP (M )) = ∅ and so, also AS(P2 ∪ fixP1 (M1 )) = ∅. Thus, P2 ∪ fixP1 (M1 ) is incoherent and so M1 is a witness for the incoherence of Π. • (M = M1 ∪ M2c ∈ AS(clone(P2 ) ∪ fixP1 (M1 ))) Here we observe that the atom domclone appears negatively in each constraint of C ′ . This means that if M is not optimal w.r.t. weak constraint in clone(P2 ∪ W2 ), then M would be dominated by some answer set of P2 ∪ fixP (M ) and the program C ′ would be satisfied. Since by assumption ∃st P2 ∪ fixP (M ) : C ′ is incoherent, then M is optimal w.r.t. weak constraints in clone(P2 ∪ W2 ). Moreover, we observe that the atom sat is false w.r.t. M and so it cannot trivially satisfy the constraints in C ′ . Let M2 ∈ OptAS(P2 ∪W2 ∪fixP1 (M1 )), then, from Lemma 3, M ′ = M2c ∪M2 is an answer set of P2 ∪ fixP (M ). Since M2 is optimal, then the cost of M is equal to the cost of M ′ for each level l and so the atom equalCost is derived as true and thus the constraint ← not domclone , not equalCost, not sat ∈ C ′ is satisfied. By assumption, M ′ violates C ′ which means that there exists at least one rule Hr ← Br , not domclone , not sat ∈ C ′ , with r ∈ C, that is violated w.r.t. M ′ . Since domclone and sat are derived as false and none of the atoms in H(sat(clone(P2 ))) appears in Hr ← Br ∈ C, then Hr ← Br is violated w.r.t. M ′ = M2c ∪ M2 iff Hr ← Br is violated w.r.t. M2 . Thus, M2 violates the original constraint program C. Since M2 can be any optimal answer set of P2 ∪ W2 ∪ fixP1 (M1 ) and M2 violates C, then no optimal answer set of P2 ∪W2 ∪fixP1 (M1 ) satisfies C. Thus, ∃st P2 ∪W2 ∪fixP1 (M1 ) : C is incoherent and so M1 is a witness for the incoherence of Π. At this point we have showed that Π′ preserves the (in)coherence of Π. As in the previous case, we observe that Π′ contains only weak constraints (i.e., W1 ) in the first program and

2-ASP(Q) with weak constraints

29

so, to get rid of such weak constraints it is possible to use the transformation by Mazzotta et al. (2024) (i.e. col6 (·)) which returns a plain 2-ASP(Q) Π′′ of the form ∀st P1′′ ∃P2′′ : C ′′ that is cohrent iff Π′ is coherent. Since verifying the coherence of Π′′ is a ΠP 2 -complete problem (Amendola et al. 2019), then the thesis holds also in this last case. Theorem 2 (Hardness) The coherence problem for 2-ASPw (Q) programs of the form □1 P1 □2 P2 : C is hard for: st P st ΣP or □2 = ∀st . 2 if □1 = ∃ ; Π2 otherwise, no matter whether □2 = ∃ Proof For the sake of the presentation, in what follows we keep separate weak constraints from rules of ASP subprogram. Thus, we consider 2-ASPw (Q) programs of the form □1 P1 ∪ W1 □2 P2 ∪ W2 : C, where P1 and P2 are ASP programs without weak constraints; whereas W1 and W2 are set of weak constraints. As in the previous case, to prove our thesis we need to distinguish different scenarios according to possible pairs of quantifiers. Case □1 = □2 = ∃st . In this case, Mazzotta et al. (2024) proved that the coherence problem for Π is ΣP 2 -complete if W1 is empty. Since this is a particular case, then the thesis holds also for the general one. Case □1 = □2 = ∀st . In this case, we prove the hardness for the particular case in which W1 is empty which inherently gives us the hardness for the general one. Let Φ = ∀X∃Y ϕ be a 2-QBF, where X and Y are disjoint set of variables and ϕ is a boolean formula in 3-CNF. We recall that a formula in 3-CNF is of the form c1 ∧ . . . ∧ cn , where each ci , with 1 ≤ i ≤ n, is a disjunction of the form l1i ∨ l2i ∨ l3i and each lji is either a positive (i.e., a ∈ X ∪Y ) or negative (i.e., ¬a, with a ∈ X ∪ Y ) literal. Given the 2-QBF Φ, verifying that Φ is true is a ΠP 2 -complete problem (Schaefer and Umans 2002). Such a problem can be encoded as a 2-ASP(Q) program Π of the form ∀st P1 ∀st P2 ∪ W2 : C that is coherent if and only if Φ is true. More precisely, the program P1 is made of rules of the form tau′ (x, t) ← not tau′ (x, f ) and tau′ (x, f ) ← not tau′ (x, t) for each x ∈ X. The program P2 is of the form tau(x, t) ← tau′ (x, f ) tau(x, t) ← tau′ (x, t) tau(y, t) ← not tau(y, f ) tau(y, f ) ← not tau(y, t) sat(ci ) ← tau(a, f ) sat(ci ) ← tau(a, t) unsat ← not sat(ci )

∀x ∈ X ∀x ∈ X ∀y ∈ Y ∀y ∈ Y ∀ci ∈ ϕ, lji = ¬a ∈ ci ∀ci ∈ ϕ, lji = x ∈ ci , a ∈ a ∪ Y ∀ci ∈ ϕ

The set of weak constraints W2 = {←ω unsat [1]}, and the constraint program C contains only the constraint ← unsat. In this case, the answer set of the program P1 are in one-to-one correspondence with possible truth assignment τ ′ for the variables in X. Thus, there exists M1 ∈ AS(P1 ) if and only if there exists a truth assignment τ ′ for variables in X. Then, the program P2′ = P2 ∪ W2 ∪ fixP1 (M1 ) guesses a truth assignment τ for the variables in Y by extending the assignment τ ′ encoded by M1 . Moreover, the program P2 checks whether τ satisfies ϕ. To this end, for each clause ci ∈ ϕ, sat(ci ) is derived iff there exists a positive (resp. negative) literal lij = a (resp. lij = ¬a), with

30

A. Cuteri, G. Mazzotta, F. Ricca

a ∈ X ∪ Y , such that τ (a) is true (resp. τ (a) is false). So, sat(ci ) is derived as true if and only if the clause ci in ϕ is satisfies w.r.t. τ . Then, the atom unsat is derived if and only if there is at least one clause that is not satisfied w.r.t. τ that is ϕ is false w.r.t. τ . Thus, let M2 ∈ AS(P2′ ) then unsat ∈ M2 iff there exists τ which extends τ ′ and ϕ is false w.r.t. τ . In this case, the weak constraint ←ω unsat [1] add a penalty to M2 . Thus, answer sets of P2′ that do not contain unsat are preferred as they do not add any penalty. So, let M2 ∈ OptAS(P2′ ) if unsat ∈ M2 , then the program C ∪ fixP2′ (M2 ) is incoherent and so also the program Π is incoherent. At the same time, we observe that for every M2′ ∈ AS(P2′ ), unsat ∈ M2′ because otherwise M2 would not be optimal. Thus, for each assignment τ of variables in Y which extends τ ′ , ϕ is false w.r.t. τ and so for the truth assignment τ ′ of variables in X, it does not exists an assignment τ of variables in Y that make ϕ true. Thus Φ is not true. On the other hand, if unsat ∈ / M2 then for each / M2′ because otherwise M2′ would be dominated by M2 and it M2′ ∈ OptAS(P2′ ), unsat ∈ would not be optimal. Thus, for each M2 ∈ OptAS(P2′ ), C ∪ fixP2′ (M2 ) is coherent and so M1 is not a witness for the incoherence of Π. At the same, since unsat ∈ / M2 then ϕ is true w.r.t. τ and so for the assignment τ ′ of variables in X there exists the assignment τ of variables in Y which extends τ ′ and make ϕ true, and so τ is not a witness for Φ not being true. Thus, we can conclude that Π is incoherent iff Φ is not true, and so the thesis follows. Case □1 ̸= □2 . Here the results follows from the complexity of the coherence problem for plain 2-ASP(Q) programs. Indeed, a plain 2-ASP(Q) of the form □1 P1 □2 P2 : C is a 2-ASP(Q) program of the form □1 P1 ∪ W1 □2 P2 ∪ W2 : C, where W1 and W2 are empty. Amendola et al. (2019) proved that verifying the coherence of □1 P1 □2 P2 : C is st P ΣP 2 -complete if □1 = ∃ ; otherwise it is Π2 -complete. Thus, the thesis follows. Theorem 3 (Completeness) The coherence problem for 2-ASPw (Q) programs of the form □1 P1 □2 P2 : C is: ΣP 2st complete if □1 = ∃st ; ΠP or □2 = ∀st . 2 -complete otherwise, no matter whether □2 = ∃

Proof The thesis follows from Lemma 1 and 2. Theorem 3 gives as an important results which allows to give completeness results for the brave reasoning tasks in 2-ASPw (Q), which consists of verifying whether an atom a is true in at least one optimal quantified answer set. Theorem 4 Let Π be an existential 2-ASPw (Q) program of the form □1 P1 □2 P2 : C : C ω and a be a ground atom, then verifying whether a ∈ M , with M ∈ OptQAS(Π), is ∆P 3 -complete no st st matter whether □2 = ∃ or □2 = ∀ . Proof (Hardness) If we consider the particular case where W(P1 ) = W(P2 ) = ∅ then verifying whether there exists M ∈ OptQAS(Π) such that a ∈ M is ∆P 3 -complete (Mazzotta et al. 2024). Thus, it holds also for the general case. (Membership) As it has been observed by Mazzotta et al. (2024) an optimal quantified

2-ASP(Q) with weak constraints

31

answer set of Π can be obtained with binary search on the value of maximum possible cost, namely k. Since k can be exponential in the general case, then an optimal quantified answer set of Π can be obtained with a polynomial number of calls to the oracle in ΣP 2 which decides the coherence of a 2-ASPw (Q) program. Finally, an extra oracle call checks that the atom a appears in some optimal quantified answer sets. Appendix C Examples: Program Transformation In this section, we redefine all the transformations required by our CEGAR-based approach for solving 2-ASPw (Q). We then illustrate each transformation through examples, with particular emphasis on counterexample search and abstraction refinement stages. We recall that the 2-ASPw (Q) programs we consider in our approach are of the form: □P1 □P2 : C : C ω

(C1)

C.1 Counterexample Search Definition 1 (Complement of stratified program) Let P be a stratified ASP program with hard constraints, then the complement of P , denoted by ¬P , is obtained from P by (i) transforming hard constraints ← l1 , . . . , ln into rules of the form v ← l1 , . . . , ln ; and (ii) adding an hard constraint of the form ← ∼v. The complement of a stratified program P with constraints is obtained by (i) transforming each hard constraint into a rule having as head the fresh atom v and by (ii) adding an hard constraint which forces the fresh atom v to be true. As a result, at least one hard constraint from P must be violated for v to be derived as true and thus for ¬P to be incoherent. The following example clarifies how the complement of a stratified program works. Example 5 Consider the following stratified program C and its complement ¬C where v ∈ B¬C is the fresh symbol introduced to capture constraint violations from C.      l ← d, c.  l ← d, c. C= ¬C = v ← l, b.   ← l, b ∼v. ← Intuitively, whenever the constraint ← l, b in C is violated, the rule v ← l, b in ¬C derives v, thereby preventing ¬C from being coherent. Conversely, when the constraint ← l, b in C is satisfied, v cannot be derived in ¬C, and hence ¬C is incoherent. Proposition 2 Given a stratified ASP program P , its complement ¬P is coherent iff P is incoherent. Definition 2 (Relaxed program) Let P be a stratified program with hard constraints, l be an integer, and unsat be a fresh atom not appearing anywhere else. Then relaxed(P, l) is defined as:   ← Br . ∀r ∈ P s.t.Hr ̸= ∅   Hr relaxed(P, l) = unsat ← Br . ∀r ∈ P s.t.Hr = ∅   ←w unsat.[1@l]

32

A. Cuteri, G. Mazzotta, F. Ricca

Intuitively, relaxed(·, ·) is similar to ¬C but the fresh atom introduced as head of hard constraints of P is used to assign a penalty if P is incoherent. The following example better clarifies how the transformation works. Example 6 Let us consider the following stratified program C and relaxed(C, 0)     ← d, c  a  a ← d, c C= relaxed(C, 0) = unsat ← a, b   ← a, b ←ω unsat [1@0] In this case, relaxed(C, 0) is obtained from C by introducing the atom unsat in the head of each hard constraint in C. Such an atom explicitly represents constraint violations. Moreover, the weak constraint ←ω unsat [1@l] assigns a penalty of 1 at priority level 0 whenever unsat is true, thereby enforcing a preference to satisfy all hard constraints in C. Definition 3 (Countermove program) Let Π be a 2-ASPw (Q) of the form (C1) and lmin be the smallest priority level among weak constraints in P2 , then the countermove program for Π is:  P2 ∪ relaxed(¬C, lmin − 1) if □ = ∃st ctr(Π) = P2 ∪ relaxed(C, lmin − 1) if □ = ∀st Proposition 4 Let Π be a 2-ASPw (Q) program of the form (C1), M1 ∈ OptAS(P1 ) be a move for □. There exists M2 ∈ OptAS(ctr(Π) ∪ fixP1 (M1 )) such that unsat ∈ / M2 if and only if M2 |H(P2 ) is a countermove to M1 for □. The following example better clarifies the intuition behind Proposition 4. Example 7 Let Π be the following 2-ASPw (Q):    c ← a ← ∼na          nc ← na ← ∼a P1 = P2 =   ←ω b ← ∼nb        ←ω nb ← ∼b

∼nc ∼c

a, ∼c [1@1] b, ∼nc [1@1]

In this case ctr(Π) is the following program:  c ← ∼nc nc ← ∼c    ω ← a, ∼c [1@1] ←ω b, ∼nc [1@1] ctr(Π) =  v ← b, c v ← nb, nc   unsat ← ∼v ←ω unsat [1@0]

   

   ← b, c  C= ← nb, nc      ← b, a, nc

    v ← b, a, nc   

Let us consider M1 = {na, nb} ∈ OptAS(P1 ). In this case, the optimal answer sets of P2 ∪ fixP1 (M1 ) are {na, nb, c} and {na, nb, nc}. Since {na, nb, nc} violates the hard constraint ← nb, nc ∈ C then {nc} is a countermove to M1 for □. Similarly, let P = ctr(Π) ∪ fixP1 (M1 ) admits two answer sets, M2 = {na, nb, c, unsat} and M2′ = {na, nb, nc, v}, which correspond to optimal answer sets of P2 ∪ fixP1 (M1 ). Here we observe that, C(P, M2 , 1) = C(P, M2′ , 1) = 0 whereas C(P, M2 , 0) > C(P, M2′ , 0) as M2 contains unsat

2-ASP(Q) with weak constraints

33

and M2′ does not. Thus, M2′ is the only optimal answer set of P . Since unsat is false w.r.t. M2′ , then M2′ |H(P2 ) = {nc} is a countermove to M1 for □. Let us now consider M1 = {na, b}. In this case, the answer sets of P2 ∪ fixP1 (M1 ) are {na, b, c} and {na, b, nc}. Here we can observe that {na, b, c} violates the weak constraint ←ω b, ∼nc ∈ P2 whereas {na, b, nc} satisfies all weak constraints in P2 . Thus, {na, b, nc} is the only optimal answer set of P2 ∪ fixP1 (M1 ). Since {na, b, nc} satisfies C then no countermoves to M1 for □ exists. Similarly, the answer sets of P = ctr(Π) ∪ fixP1 (M1 ) are M2 = {na, b, c, v} and M2′ = {na, b, nc, unsat}. In this case, M2 is dominated by M2′ as C(P, M2 , 1) > C(P, M2′ , 1), and thus the only optimal answer set of P is M2′ . Moreover, unsat is true w.r.t M2′ then no countermove to M1 for □ exists.

C.2 Abstraction Refinement Let Π be a 2-ASPw (Q) of the form C1, M1 , M1′ be two moves for □, and M2 be a countermove to M1 for □. Then, then M2 is not a countermove to M1′ for □ if one of the following condition holds: 1. there is no M2′ ∈ AS(P2 ∪ fixP1 (M1′ )) such that M2′ |H(P2 ) = M2 ; 2. there exists M2′ ∈ AS(P2 ∪ fixP1 (M1′ )) such that M2′ |H(P2 ) = M2 but M2′ ∈ / OptAS(P2 ∪fixP1 (M1′ )) (i.e. M2′ is dominated by some answer set of P2 ∪fixP1 (M1′ )); 3. there exists M2′ ∈ OptAS(P2 ∪fixP1 (M1′ )) such that M2′ |H(P2 ) = M2 but M2′ satisfies C and □ = ∃st (resp. violates C and □ = ∀st ). The following transformation will be instrumental for defining the Refinement program. For producing rules over a fresh signature we need to introduce a rewriting transformation. To this end, we introduce a predicate substitution function that maps each predicate p with a fresh ones of the form pα β , where α and β are strings, to obtain rules over a fresh signature for each discovered countermove. More in detail, let L be a set of literals and ϵ be an ASP expression (i.e. rule, program, etc.), then σβα (L, ϵ) denotes the expression obtained from ϵ by mapping each positive (resp. negative) literal p(⃗t) ∈ L ⃗ ∼ α ⃗ (resp. ∼p(⃗t) ∈ L) with pα β (t) (resp. pβ (t)). Definition 4 (Check Answer Set) Let P be an ASP program and M be an interpretation, then checkAS(P, M ) is:  − σM (H(P ), {a ← |a ∈ M })    −   ∀r ∈ P, Hr ̸= ∅ σ + (H(P ), σM (H(P ), r))    M + − f ailM ← σM (H(P ), σM (H(P ), Br )) ∀r ∈ P, Hr = ∅ checkAS(P, M ) = − ∼ ⃗  f ailM ← p(⃗t)+ ∀ p(⃗t) ∈ H(P )  M , p(t)M   − + ⃗ ⃗  ∼ f ail ← p( t ) , p( t ) ∀ p(⃗t) ∈ H(P ) M  M M   asM ← ∼f ailM The following example better clarifies how CheckAS(·, ·) works. Example 8

34

A. Cuteri, G. Mazzotta, F. Ricca

Consider P2 from Example 7 and M = {c} then checkAS(P2 , M ) is of the following form:   + − ∼ c ← ∼nc− nc+   M M ← cM  M    −    cM ←  + − + − ∼ ∼ checkAS(P2 , M ) = f ailM ← cM , cM f ailM ← ncM , ncM  − + +    ∼   f ailM ← nc−  f ailM ← cM , ∼cM  M , ncM   asM ← ∼f ailM In this case, the program P2 is made of rules c ← ∼nc and nc ← ∼c. These two rules are rewritten as follows: (i) negative literals over atoms in H(P2 ) (i.e. H(P2 ) = {∼c, ∼nc}) − ∼ are replaced, respectively, by ∼c− M and ncM , which form the negative signature; and (ii) positive literals over atoms in H(P2 ) (i.e. H(P2 ) = {c, nc}) are replaced, respectively, by + c+ M and ncM , which form positive signature. The interpretation M = {c} is then encoded as facts over the negative signature, which allows the previous rules to be simplified thus yielding the the GL-reduct of P2 w.r.t. M (i.e. P2M ). Next, the rules having f ailM in the head check whether the truth values of atoms over the positive signature (i.e. a model of the reduct) match the truth value of those over the negative signature (i.e. the interpretation M ). Finally, the atom asM is derived if and only if the truth values of all atoms over the two signatures coincide, that is, f ailM cannot be derived as true. Definition 6 (Dominated program) Let P1 and P2 be two ASP programs, then checkDom(P1 , P2 ) is the following program: dif fP1 ,P2 ← clP1 (C1, L), clP2 (C2, L), C1 ̸= C2. hasHigherP1 ,P2 (L) ← dif fP1 ,P2 (L), dif fP1 ,P2 (L1), L < L1. highestP1 ,P2 (L) ← dif fP1 ,P2 (L), ∼hasHigherP1 ,P2 (L). domP1 ,P2 ← highestP1 ,P2 (L), clP1 (C1, L), clP2 (C2, L), C2 < C1 where clP1 and clP2 are, respectively, the predicates introduced by cost(P1 ) and cost(P2 ) (Definition 5); whereas dif f , hasHigher, highest, and dominated are fresh predicates. Definition 7 (Controlled program) Let P be an ASP program and l be a literal not appearing in P , then or(P, l) is the program of the form {Hr ← Br , l | r ∈ P } Definition 8 (Refinement Program) Let Π be a 2-ASPw (Q) program of the form (C1), M be a move for □ and CE be a countermove to M for □. The refinement program is defined as follows:   checkAS(P2 , CE)         ←w asCE [1@lmin − 1]         CE   or(cost(P2 ), asCE )      or(clone(R(P )), as )  2 CE ref (Π, CE) = or(cost(clone(P2 )), asCE )         CE   or(checkDom(P , clone(P )), as ) 2 CE   2     w   ∼domP CE ,clone(P ) [1@lmin − 2] ← as ,   CE 2   2   − ′ ′ or(σCE (lits(P2 ) ∪ lits(C ), C ), asCE ) − where P2CE = σCE (lits(P2 ), P2 ), asCE is the predicate introduced by checkAS(P2 , CE),

2-ASP(Q) with weak constraints

35

C ′ = relaxed(C, lmin − 3) if □ = ∃st ; otherwise C ′ = relaxed(¬C, lmin − 3), and lmin is the smallest priority level among weak constraints of P1 . To explain the idea behind ref (Π, CE) we use the following example. Example 9 Let Π be the 2-ASPw (Q) program from Example 7, we know that M1 = {na, nb} ∈ OptAS(P1 ) is a move for □ and M2 = {nc} is a countermove to M1 for □. We therefore aim to refine the abstraction P1 as to avoid all those optimal answer sets of P1 that admit M2 as countermove. To this end, we use the rules obtained by Ref (Π, M2 ) which are reported below. % or(cost(P2M2 ), asM2 )

% checkAS(P2 , M2 ) − ∼ c+ M2 ← ncM2 + ncM2 ← ∼c− M2 nc− ← M2 − ∼ f ailM2 ← c+ M2 cM2 + f ailM2 ← ncM2 ∼nc− M2 asM2 ← ∼f ailM2 ←ω asM2 [1@ − 1]

vP M2 (1, 1) ← a, ∼c− M2 , asM2 2

vP M2 (1, 1) ← b, ∼nc− M2 , asM2 2

clP M2 (C, 1) ← #sum{1, 1 : vP M2 (1, 1)} = C, asM2 2

2

% or(clone(R(P2 )), asM2 )

% or(cost(clone(P2 )), asM2 )

cclone ← ∼ncclone , asM2 ncclone ← ∼cclone , asM2

vclone(P2 ) (1, 1) ← a, ∼cclone , asM2 vclone(P2 ) (1, 1) ← b, ∼ncclone , asM2 clclone(P2 ) (C, 1) ← #sum{1, 1 : vclone(P2 ) (1, 1)} = C, asM2

% or(checkDom(P2M2 , clone(P2 )), asM2 )) dif fP M2 ,clone(P2 ) ← clP M2 (C1, L), clclone(P2 ) (C2, L), C1 ̸= C2, asM2 2

2

hasHigherP M2 ,clone(P2 ) (L) ← dif fP M2 ,clone(P2 ) (L), dif fP M2 ,clone(P2 ) (L1), L < L1, asM2 2

2

2

highestP M2 ,clone(P2 ) (L) ← dif fP M2 ,clone(P2 ) (L), ∼hasHigherP M2 ,clone(P2 ) (L), asM2 2

2

2

domP M2 ,clone(P2 ) ← highestP M2 ,clone(P2 ) (L), clP M2 ,clone(P2 ) (C1, L), asM2 2

2

←ω ∼asM2 , ∼domP M2 ,clone(P2 ) [1@ − 2]

2

2

− % or(σM (lits(P2 ) ∪ lits(C), relaxed(C, −3)), asM2 ) 2 − unsat− M2 ← b, cM 2 , asM2 . − unsatM2 ← nb, nc− M2 , asM2 . − unsat− ← b, a, nc M2 M2 , asM2 . − ω ← unsatM2 . [1@ − 3] As it can be observed, the refinement rules are made of several blocks which encode the the three conditions for detecting if M2 is again a countermove. More precisely, the first block contains checkAS(P2 , M2 ) and thus simulates the reduct of P2 w.r.t. M2 . Here, we can observe that M2 = {nc} is encoded as the fact nc− M2 ← over the negative + − ∼nc signature. Since nc− is true, the rule c ← has a false body, whereas the rule M2 M2 M2 − − ∼c nc+ ← can be simplified as c does not appear in the head of any rule and M2 M2 M2 is therefore false. As a result, during the evaluation we will obtain the reduct of P2 w.r.t. M2 . The remaining rules derive the atom asM2 if and only if the negative signature matches the positive one (i.e. f ailM2 is false). If asM2 is derived as false, then condition 1

36

A. Cuteri, G. Mazzotta, F. Ricca

is satisfied. Consequently, the weak constraint ←ω asM2 enforces a preference for moves that satisfy condition 1. Moreover, when asM2 is derived as false, since asM2 appears in the body all the remaining rules, then these rules are trivially satisfied and no further checks are required. Conversely, if asM2 is derived as true, all the remaining rules are activated in order to verify the other conditions. To check condition 2, we instead use the blocks %or(cost(P2M2 ), asM2 ) - %or(checkDom(P2M2 and clone(P2 )), asM2 ). More precisely, the rules in cost(P2M2 ) compute the cost of M2 − (lits(P2 ), P2 ) since M2 w.r.t. weak constraints in P2 . Note that, P2M2 is obtained as σM 2 − has been encoded as facts over the negative signature (i.e. ncM2 ). Thus, the negative signature for atoms in P2 is used to compute the cost of M2 . To verify that M2 is optimal, it must be compared with all answer sets of P2 . This one-to-one comparison, is achieved by adding a clone of the rules from program P2 (i.e. the block clone(R(P2 ))). Note that, the weak constraints in P2 are not cloned in order to preserve all the answer sets of P2 . The rules in cost(clone(P2 )) are then used to compute the cost of an answer set Mclone of clone(P2 ), in the same spirit as cost(P2M2 ). As a result, atoms of the form clP M2 (·, ·) 2 and clclone(P2 ) (·, ·) encode the cost of M2 ∈ AS(P2 ) and Mclone ∈ AS(clone(P2 )), respectively. Finally, rules in the block checkDom(P2M2 , clone(P2 )) verify whether M2 is dominated by Mclone . More precisely, the atom domP M2 ,clone(P2 ) is derived as true if and 2 only if M2 is dominated by Mclone , and thus condition 2 is satisfied. Consequently, the weak constraint ←ω asM2 , ∼domP M2 ,clone(P2 ) [1@lmin −2] enforces a preference for moves 2 that satisfy condition 2. − The last condition, namely condition 3, is encoded by the block or(σM (lits(P2 ) ∪ 2 lits(C), relaxed(C, −3)), asM2 ). The rules contained in this block check whether C is satisfied or not. In this example, condition 3 is satisfied if and only if C is coherent. Accordingly, relaxed(C, −3) is used to capture the incoherence of C by means of the atom unsat. Note that the program C may contain atoms appearing in P2 . Since M2 has been encoded as facts over the negative signature (i.e., nc− M2 ),the rules from relaxed(C, −3) − must be mapped onto this signature using σM (·). As a result, the atom unsat is mapped 2 to unsat− , which is derived as false if and only if M 2 satisfies C, and thus condition 3 M2 − ω holds. Consequently, the weak constraint ← unsatM2 [1@ − 3] enforces a preference for moves that satisfy condition 3. Finally, the next move for □ can be computed from an optimal answer set M1′ of P1 ∪ ref (Π, M2 ). Note that, if all the weak constraints introduced by ref (Π, M2 ) are violated w.r.t. M1′ , then conditions 1, 2, and 3 are violated, and so, M2 is a countermove also to M1′ . Hence, M1′ can be considered as the next move for □ if and only if at least one weak constraint in ref (Π, M2 ) is satisfied w.r.t. M1′ . Conversely, if M1′ violates all the weak constraints of ref (Π, M2 ), then all the optimal answer sets of P1 ∪ ref (Π, M2 ) violate the weak constraints in ref (Π, M2 ). In this case, all possible moves for □ have M2 as countermove and thus no further move exists for □. Appendix D Solving 2-ASPw (Q) Programs In this section we give a more detailed description of the CEGAR-based algorithm for solving 2-ASPw (Q). Based on the definitions of countermove program (i.e., Definition 3) and refinement program (i.e., Definition 8), we can construct a procedure based on CEGAR for deciding

2-ASP(Q) with weak constraints

37

Algorithm 1 CEGAR for 2-ASPw (Q) Input: A 2-ASPw (Q) of the form □1 P1 □1 P2 : C Output:M1 if a winning move exists for □1 , N U LL otherwise 1: CMS = ∅ 2: M1 = solveOpt(P1 ) 3: while M1 ̸= ⊥ do 4: M2 = solveOpt(ctr(Π) ∪ fixP1 (M1 )) 5: if M2 = ⊥ ∨ C(ctr(Π) ∪ fixP1 (M1 ), M2 , 0) = 1 then 6: return M1 7: else 8: CE = M2 |H(P2 ) 9: CMs = CMs ∪ CE 10: end if S 11: A = P1 CE∈CMs ref (Π, CE) 12: N = solveOpt(A) 13: if (C(A, M1 , lmin − 1) = 1 ∧ C(A, M1 , lmin − 2) = 1 ∧ C(A, M1 , lmin − 3) = 1) then 14: return N U LL 15: end if M1 = N |H(P1 ) 16: end while 17: return N U LL

the coherence of 2-ASPw (Q) programs (see Algorithm 1). In particular, such a procedure relies on an off-the-shelf ASP solver, which is used to compute optimal answer sets of both the (refined) abstraction and the countermove program. We denote by solveOpt(P ) the call to an ASP solver that returns an optimal answer set of an ASP program P , if one exists. Algorithm 1 takes as input a 2-ASPw (Q) of the form C1 and returns a winning move for □ if any, otherwise returns N U LL. The algorithm starts by initializing the set of countermoves to the empty set (line 1) and by computing an optimal answer set of the abstraction P1 (line 2). If P1 is incoherent, the algorithm terminates returning N U LL, since no winning move for □ exists (line 17). Otherwise, P1 admits an optimal answer set M1 , which is a move for □. Algorithm 1 then enters the CEGAR loop, which alternates countermove search and abstraction refinement steps (line 3). Let M1 be a move for □. At each iteration of the loop, a countermove to M1 is searched by solving ctr(Π) ∪ fixP1 (M1 ) (line 4). If ctr(Π) ∪ fixP1 (M1 ) is incoherent, then P2 ∪ fixP1 (M1 ) is incoherent and hence no candidate countermove to M1 for □ exists. In this case, Algorithm 1 returns M1 as winning move. Otherwise, crt(Π) ∪ fixP1 (M1 ) is coherent, and solveOpt(crt(Π) ∪ fixP1 (M1 )) returns an optimal answer set M2 . If unsat ∈ M2 , then there exists no M2′ ∈ OptAS(ctr(Π) ∪ fixP1 (M1 )) such that unsat ∈ / ′ ′ M2 , otherwise M2 would be dominated by M2 . Hence, from Proposition 4, none of the candidate countermoves is an actual countermove to M1 for □, and so Algorithm 1 returns M1 as winning move. If, instead, M2 does not contain the atom unsat, then from Proposition 4, M2 |H(P2 ) is a countermove to M1 for □. Accordingly, Algorithm 1 extracts the countermove CE by projecting M2 onto the atoms appearing in the heads of the rules in P2 (line 8), and adds CE to the set of countermoves CM s (line 9). The algorithm then computes the refined abstraction A by refining the abstraction P1 according to the the countermoves in CM s (line 11). The refined abstraction is subsequently solved to compute the next move for □ (line 12). Let N be an answer set of the refined abstraction A, and M1 = N |H(P1 ) be a move for □. If there exists some CE ∈ CM s such that N violates all the weak constraints in ref (Π, CE), then CE is again a valid countermove to M1 . In this case, the cost of N at priority levels lmin − 1, lmin − 2, and lmin − 3 is equal

38

A. Cuteri, G. Mazzotta, F. Ricca

to 1, which is the maximum possible cost at these levels. Accordingly, if the cost of an optimal answer set of the refined abstraction A at levels lmin − 1, lmin − 2, and lmin − 3 is equal to 1, then every possible move admits at least one CE ∈ CM s as a countermove. Hence, no winning move for □ exists, and Algorithm 1 returns N U LL (line 14). In all other cases, M1 does not admit any countermove in CM s, and the loop continues by taking M1 as the next move for □.