2-ASP(Q) programs with weak constraints: Complexity... | AI Research

What the paper is about

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-ASP(Q)^w. 2-ASP(Q)^w is a practically relevant fragment of ASP(Q) that is expressive enough to capture optimization problems up to the class Delta_3^P. On the theoretical side, we provide a complete complexity characterization of the main computational tasks for 2-ASP(Q)^w 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.

What it covers

\jdate \pagerange 2-ASP(Q) programs with weak constraints: Complexity and efficient implementation † † thanks: 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. ANDREA CUTERI GIUSEPPE MAZZOTTA FRANCESCO RICCA University of Calabria Rende Italy 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-ASP w (Q). 2-ASP w (Q) is a practically relevant fragment of ASP(Q) that is expressive enough to capture optimization problems up to the class Δ 3 P \Delta^{P}{3} . On the theoretical side, we provide a complete complexity characterization of the main computational tasks for 2-ASP w (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 [ 9 ] (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 [ 34 ] , scheduling [ 18 , 12 ] , business process management [ 14 , 26 ] , among many others [ 19 ] . A substantial body of research has focused on extending ASP modeling and solving capabilities, leading to the proposal of several language extensions [ 3 , 7 , 25 ] . Among these, Answer Set Programming with Quantifiers [ 3 ] (ASP(Q)) introduces the possibility to quantify over answer sets [ 29 ] . This extension enhances the expressive power of ASP, allowing for the natural modeling of problems spanning the entire Polynomial Hierarchy (PH). ASP(Q) has found interesting applications in several contexts, including outlier detection [ 6 ] , planning [ 22 ] and related domains [ 24 ] , establishing it as a promising framework for solving problems beyond NP. More recently, ASP(Q) has been extended with weak constraints , denoted by ASP w (Q) [ 31 ] , further enhancing its ability to naturally represent hard optimization problems. Weak constraints in ASP w (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 [ 4 ] . Within this context, we focus on ASP(Q) programs with two quantifiers and weak constraints, denoted as 2-ASP w (Q), which are expressive enough to model complex optimization problems up to Δ 3 P \Delta^{P}{3} . Indeed, the expressive power of 2-ASP w (Q) is not yet fully characterized, as existing completeness results are available only for specific language fragments [ 31 ] . As a consequence, the development of efficient and complexity-aware implementations for the entire 2-ASP w (Q) has so far been left unexplored. To fill this gap, this paper undertakes a complexity analysis of the main reasoning tasks for 2-ASP w (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-ASP w (Q). In particular, we propose an efficient evaluation technique based in Counterexample-Guided Abstraction Refinement (CEGAR) [ 15 , 30 ] , 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 [ 1 ] , 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 [ 16 ] . 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 → ) p(\vec{t}) with t → = t 1 , … , t n \vec{t}=t_{1},\ldots,t_{n} being a list of terms and p p being a predicate of arity n ≥ 0 n\geq 0 . An atom p ​ ( t → ) p(\vec{t}) is ground if all terms in t → \vec{t} are constants. A literal is either an atom a a or its negation ∼ a \raise 0.73193pt\hbox{$\scriptstyle\mathtt{\sim}$}a . The complement of a literal l = a l=a (resp. l = ∼ a l=\raise 0.73193pt\hbox{$\scriptstyle\mathtt{\sim}$}a ) is l ¯ = ∼ a \overline{l}=\raise 0.73193pt\hbox{$\scriptstyle\mathtt{\sim}$}a (resp. l ¯ = a \overline{l}=a ). Given a set of literals L L , L + L^{+} (resp. L − L^{-} ) denotes the set of positive (resp. negative) literals appearing in L L . A rule is an expression of the form h ← l 1 , … , l n h\leftarrow l_{1},\ldots,l_{n} where h h is an atom referred to as head , and l 1 , … , l n l_{1},\ldots,l_{n} with n ≥ 0 n\geq 0 is a conjunction of literals referred 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 ← ω l 1 , … , l n ​ [ w ​ @ ​ l , t → ] \leftarrow^{\omega}l_{1},\ldots,l_{n}\ [w@l,\vec{t}] where l 1 , … , l n l_{1},\ldots,l_{n} is a conjunction of literals referred to as body, w w and l l are terms, and t → = t 1 , … , t m \vec{t}=t_{1},\ldots,t_{m} is a possibly empty list of terms. Given a rule (resp. a weak constraint) r r , H r H_{r} denotes the set of atoms appearing in the head of r r while B r B_{r} denotes the set of literals appearing in the body of r r . A rule r r (resp. a weak constraint) is safe if each variable appears in at least one literal in B r + B_{r}^{+} . A program P P is a set of safe rules and weak constraints. Given a program P P , ℛ ​ ( P ) \mathcal{R}(P) and 𝒲 ​ ( P ) \mathcal{W}(P) denote, respectively, the sets of rules and weak constraints appearing in P P ; while ℋ ​ ( P ) \mathcal{H}(P) denotes the set of atoms appearing in the head of some rules in P P . Given an expression ϵ \epsilon (atom, program, etc.), a ​ t ​ ( ϵ ) at(\epsilon) denotes the set of atoms appearing in ϵ \epsilon . Semantics Given an ASP program P P , the Herbrand Universe , H ​ U P HU_{P} , of P P is the set of all constants appearing in P P ; the Herbrand Base , B P B_{P} , is the set of all possible ground atoms that can be obtained from predicates and constants in P P ; g ​ r ​ o ​ u ​ n ​ d ​ ( P ) ground(P) denotes the set of all ground rules that can be obtained from P P by proper substitutions of variables in P P with constants in H ​ U P HU_{P} . An interpretation I ⊆ B P I\subseteq B_{P} is a set of atoms. A ground literal l = a l=a (resp. l = ∼ a l=\raise 0.73193pt\hbox{$\scriptstyle\mathtt{\sim}$}a ) is true w.r.t. I I if a ∈ I a\in I (resp. a ∉ I a\notin I ), false otherwise. A conjunction of literals c ​ o ​ n ​ j conj is true w.r.t. I I if all the literals in c ​ o ​ n ​ j conj are true w.r.t. I I , false otherwise. An interpretation I I is an answer set of P P iff ( i i ) I I is a model of P P , namely for each rule r ∈ g ​ r ​ o ​ u ​ n ​ d ​ ( P ) r\in ground(P) either H r H_{r} is true w.r.t. I I or B r B_{r} is false w.r.t. I I ; and ( i ​ i ii ) I I is a minimal model of its GL-reduct [ 29 ] . Let A ​ S ​ ( P ) AS(P) be the set of answer set of a program P P , then P P is coherent iff A ​ S ​ ( P ) ≠ ∅ AS(P)\neq\emptyset . For a program P P and an interpretation I I , let the set of weak constraint violations be w s ( P , I ) = { ( w , l , t → ) ∣ ← ω b 1 , … , b m [ w @ l , t → ] ∈ g r o u n d ( P ) ws(P,I)={(w,l,\vec{t})\mid\ \leftarrow^{\omega}b_{1},\ldots,b_{m}\ [w@l,\vec{t}]\in ground(P) and b 1 , … , b m b_{1},\ldots,b_{m} are true w.r.t. I } I} , then the cost function of P P is defined as 𝒞 ​ ( P , I , k ) = ∑ ( w , k , t → ) ∈ w ​ s ​ ( P , I ) w \mathcal{C}(P,I,k)=\sum_{(w,k,\vec{t})\in ws(P,I)}w for every integer k k . Let M 1 , M 2 ∈ A ​ S ​ ( P ) M_{1},M_{2}\in AS(P) then M 1 M_{1} is dominated by M 2 M_{2} if there exists an integer l l such that 𝒞 ​ ( P , M 1 , l ) > 𝒞 ​ ( P , M 2 , l ) \mathcal{C}(P,M_{1},l)>\mathcal{C}(P,M_{2},l) and for each l ′ > l l^{\prime}>l , 𝒞 ​ ( P , M 1 , l ′ ) = 𝒞 ​ ( P , M 2 , l ′ ) \mathcal{C}(P,M_{1},l^{\prime})=\mathcal{C}(P,M_{2},l^{\prime}) . Let M ∈ A ​ S ​ ( P ) M\in AS(P) then M M is an optimal answer set iff M M is not dominated by any M ′ ∈ A ​ S ​ ( P ) M^{\prime}\in AS(P) . We denote by O ​ p ​ t ​ A ​ S ​ ( P ) OptAS(P) the set of optimal answer set of P P . 2.2 ASP with Two Quantifiers A 2-ASP w (Q) program [ 31 ] is an expression of the form □ 1 ​ P 1 ​ □ 2 ​ P 2 : C : C ω \Box_{1}P_{1}\Box_{2}P_{2}:C:C^{\omega} , where □ 1 , □ 2 \Box_{1},\Box_{2} are quantifiers in { ∃ s ​ t , ∀ s ​ t } {\exists^{st},\forall^{st}} , P 1 , P 2 P_{1},P_{2} are ASP programs possibly with weak constraints, C C is a stratified program [ 13 ] with hard constraints, and C ω C^{\omega} is a set of weak constraints such that B C ω ⊆ B P 1 B_{C^{\omega}}\subseteq B_{P_{1}} . Weak constraints appearing P 1 P_{1} and P 2 P_{2} are said local ; whereas those in C ω C^{\omega} are said global . A 2-ASP w (Q) program Π \Pi is said to be existential if □ 1 = ∃ s ​ t \Box_{1}=\exists^{st} , otherwise it is universal . Moreover, Π \Pi is said to be alternating if □ 1 ≠ □ 2 \Box_{1}\neq\Box_{2} , and plain if it contains no weak constraints. We now define the semantics of 2-ASP w (Q) programs. Let P P be an ASP program and M ⊆ B P M\subseteq B_{P} , then 𝑓𝑖𝑥 P ​ ( M ) \mathit{fix_{P}(M)} denotes the set of facts and hard constraints of the form { a ← ∣ a ∈ M } ∪ { ← a ∣ a ∈ B P ∖ M } {a\leftarrow\mid a\in M}\cup{\leftarrow a\mid a\in B_{P}\setminus M} . Then, M ∈ A ​ S ​ ( P ) M\in AS(P) satisfies a program P ′ P^{\prime} if P ′ ∪ 𝑓𝑖𝑥 P ​ ( M ) P^{\prime}\cup\mathit{fix_{P}(M)} is coherent. At this point the coherence of 2-ASP w (Q) can be defined as follows: • ∃ s ​ t P : C : C ω \exists^{st}P:C:C^{\omega} is coherent iff there exists M ∈ O ​ p ​ t ​ A ​ S ​ ( P ) M\in OptAS(P) such that M M satisfies C C . • ∀ s ​ t P : C : C ω \forall^{st}P:C:C^{\omega} is coherent iff for each M ∈ O ​ p ​ t ​ A ​ S ​ ( P ) M\in OptAS(P) , M M satisfies C C . • ∃ s ​ t P 1 ​ □ 2 ​ P 2 : C : C ω \exists^{st}P_{1}\Box_{2}P_{2}:C:C^{\omega} is coherent iff there exists M 1 ∈ O ​ p ​ t ​ A ​ S ​ ( P 1 ) M_{1}\in OptAS(P_{1}) such that □ 2 ​ P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) : C : C ω \Box_{2}P_{2}\cup\mathit{fix_{P_{1}}(M_{1})}:C:C^{\omega} is coherent. • ∀ s ​ t P 1 ​ □ 2 ​ P 2 : C : C ω \forall^{st}P_{1}\Box_{2}P_{2}:C:C^{\omega} is coherent iff for each M 1 ∈ O ​ p ​ t ​ A ​ S ​ ( P 1 ) M_{1}\in OptAS(P_{1}) , □ 2 ​ P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) : C : C ω \Box_{2}P_{2}\cup\mathit{fix_{P_{1}}(M_{1})}:C:C^{\omega} is coherent. For an existential 2-ASP w (Q) program Π \Pi , an optimal answer set M 1 ∈ O ​ p ​ t ​ A ​ S ​ ( P 1 ) M_{1}\in OptAS(P_{1}) is a quantified answer set of Π \Pi if □ 2 ​ P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) : C : C ω \Box_{2}P_{2}\cup\mathit{fix_{P_{1}}(M_{1})}:C:C^{\omega} is coherent. We denote by Q ​ A ​ S ​ ( Π ) QAS(\Pi) the set of quantified answer sets of Π \Pi . Let Π \Pi be an existential 2-ASP w (Q) program, l l be an integer, and M ∈ Q ​ A ​ S ​ ( Π ) M\in QAS(\Pi) , then the cost of M M at level l l is defined as 𝒞 ​ ( M , Π , l ) = 𝒞 ​ ( M , P 1 ∪ C ω , l ) \mathcal{C}(M,\Pi,l)=\mathcal{C}(M,P_{1}\cup C^{\omega},l) . Let M 1 , M 2 ∈ Q ​ A ​ S ​ ( Π ) M_{1},M_{2}\in QAS(\Pi) , then M 1 M_{1} is dominated by M 2 M_{2} if there exists l l such that 𝒞 ​ ( M 1 , Π , l ) > 𝒞 ​ ( M 2 , Π , l ) \mathcal{C}(M_{1},\Pi,l)>\mathcal{C}(M_{2},\Pi,l) and for each l ′ > l l^{\prime}>l , 𝒞 ​ ( M 1 , Π , l ′ ) = 𝒞 ​ ( M 2 , Π , l ′ ) \mathcal{C}(M_{1},\Pi,l^{\prime})=\mathcal{C}(M_{2},\Pi,l^{\prime}) . Thus, M M is an optimal quantified answer set if M M is not dominated by any M ′ ∈ Q ​ A ​ S ​ ( Π ) M^{\prime}\in QAS(\Pi) . We denote by O ​ p ​ t ​ Q ​ A ​ S ​ ( Π ) OptQAS(\Pi) the set of optimal quantified answer sets. Example 1 Let Π \Pi be a 2-ASP w (Q) program of the form ∃ s ​ t P 1 ​ ∀ s ​ t P 2 : C \exists^{st}P_{1}\forall^{st}P_{2}:C , where C = { ← n b , n c } C={\leftarrow nb,\ nc} and P 1 = { a ← ∼ n a b ← ∼ n b n a ← ∼ a n b ← ∼ b } P_{1}=\left{\begin{array}[]{lr}a\leftarrow\raise 0.73193pt\hbox{$\scriptstyle\mathtt{\sim}$}na\qquad&b\leftarrow\raise 0.73193pt\hbox{$\scriptstyle\mathtt{\sim}$}nb\ na\leftarrow\raise 0.73193pt\hbox{$\scriptstyle\mathtt{\sim}$}a\qquad&nb\leftarrow\raise 0.73193pt\hbox{$\scriptstyle\mathtt{\sim}$}b\ \end{array}\right} P 2 = { c ← ∼ n c ← ω a , ∼ c [ 1 @ 1 ] n c ← ∼ c ← ω b , ∼ n c [ 1 @ 1 ] } P_{2}=\left{\begin{array}[]{ll}c\leftarrow\raise 0.73193pt\hbox{$\scriptstyle\mathtt{\sim}$}nc\qquad&\leftarrow^{\omega}a,\ \raise 0.73193pt\hbox{$\scriptstyle\mathtt{\sim}$}c\ [1@1]\ nc\leftarrow\raise 0.73193pt\hbox{$\scriptstyle\mathtt{\sim}$}c\qquad&\leftarrow^{\omega}b,\ \raise 0.73193pt\hbox{$\scriptstyle\mathtt{\sim}$}nc\ [1@1]\ \end{array}\right} Let us consider M 1 = { n ​ a , n ​ b } ∈ A ​ S ​ ( P 1 ) M_{1}={na,nb}\in AS(P_{1}) . In this case, { n ​ a , n ​ b , n ​ c } ∈ O ​ p ​ t ​ A ​ S ​ ( P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) ) {na,nb,nc}\in OptAS(P_{2}\cup\mathit{fix_{P_{1}}(M_{1})}) violates the constraint ← n ​ b , n ​ c ∈ C \leftarrow nb,nc\in C . Thus, M 1 ∉ Q ​ A ​ S ​ ( Π ) M_{1}\notin QAS(\Pi) . Conversely, M 1 ′ = { a , n ​ b } ∈ A ​ S ​ ( P 1 ) M_{1}^{\prime}={a,nb}\in AS(P_{1}) is such that P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ′ ) P_{2}\cup\mathit{fix_{P_{1}}(M_{1}^{\prime})} admits only one optimal answer set M 2 = { a , n ​ b , c } M_{2}={a,nb,c} which satisfies the constraint in C C and so M 1 ∈ Q ​ A ​ S ​ ( Π ) M_{1}\in QAS(\Pi) . If we remove weak constraints from P 2 P_{2} , then A ​ S ​ ( P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) ) = { M 2 , M 2 ′ } AS(P_{2}\cup\mathit{fix_{P_{1}}(M_{1})})={M_{2},M_{2}^{\prime}} where M 2 ′ = { a , n ​ b , n ​ c } M_{2}^{\prime}={a,nb,nc} . Here, M 2 ′ M_{2}^{\prime} violates the constraint in C C and so M 1 M_{1} is not a quantified answer set anymore. 3 Complexity Results for 2-ASP w (Q) In this section, we study the main computational tasks for 2-ASP w (Q): Coherence and Brave reasoning. For 2-ASP w (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 ASP w (Q) programs introduce an additional source of computational complexity, as observed by \citeN DBLP:journals/tplp/MazzottaRT24. Even though complexity results for these tasks have been established for specific subclasses of ASP w (Q), a complete characterization is still missing. In particular, it was shown that verifying the coherence for 2-ASP w (Q) programs ( i i ) is in Σ 3 P \Sigma_{3}^{P} for existential programs and in Π 3 P \Pi_{3}^{P} for universal programs, and ( i ​ i ii ) is hard for Σ 2 P \Sigma_{2}^{P} and Π 2 P \Pi_{2}^{P} , respectively. Starting from these results, we prove that the coherence problem for 2-ASP w (Q) is complete for the second level of the PH, namely Σ 2 P \Sigma_{2}^{P} for existential programs and Π 2 P \Pi_{2}^{P} for universal programs (full proofs in B ). Theorem 1 (Membership) The coherence problem for 2-ASP w (Q) programs of the form □ 1 ​ P 1 ​ □ 2 ​ P 2 : C \Box_{1}P_{1}\Box_{2}P_{2}:C is in: Σ 2 P \Sigma_{2}^{P} if □ 1 = ∃ s ​ t \Box_{1}=\exists^{st} ; Π 2 P \Pi_{2}^{P} otherwise, no matter whether □ 2 = ∃ s ​ t \Box_{2}=\exists^{st} or □ 2 = ∀ s ​ t \Box_{2}=\forall^{st} . Proof 3.2 (Proof (Sketch)) . To prove our thesis we need to distinguish three different scenarios. Uniform quantifiers □ 1 = □ 2 \Box_{1}=\Box_{2} . By applying the transformation (Algorithm 1) by \citeN DBLP:journals/tplp/MazzottaRT24, it is possible to obtain a plain 2-ASP(Q) program Π ′ \Pi^{\prime} such that Π ′ \Pi^{\prime} is coherent if and only if Π \Pi is coherent. From the result of \citeN DBLP:journals/tplp/AmendolaRT19, verifying the coherence of Π ′ \Pi^{\prime} is Σ 2 P \Sigma_{2}^{P} -complete if □ 1 = ∃ s ​ t \Box_{1}=\exists^{st} ; otherwise is in Π 2 P \Pi_{2}^{P} -complete. Thus the thesis holds for uniform quantifiers. Case □ 1 = ∃ s ​ t \Box_{1}=\exists^{st} and □ 2 = ∀ s ​ t \Box_{2}=\forall^{st} . In this case, it is possible to translate Π \Pi into an existential 2-ASP w (Q) program Π ′ \Pi^{\prime} where weak constraints appear only in the first subprogram. Since verifying the coherence of Π ′ \Pi^{\prime} is Σ 2 P \Sigma_{2}^{P} -complete (Corollary 3.1 by \citeN DBLP:journals/tplp/MazzottaRT24) , then the thesis holds also in this case. More precisely, the 2-ASP w (Q) program Π ′ \Pi^{\prime} can be obtained by copying the rules of the program P 2 P_{2} in P 1 P_{1} and then adding rules in the program C C for verifying the optimality of an answer sets of P 2 P_{2} . As a result, we obtain Π ′ \Pi^{\prime} of the form ∃ P 1 ′ ​ ∀ P 2 ′ : C ′ \exists P_{1}^{\prime}\forall P_{2}^{\prime}:C^{\prime} where: • optimal answer sets M M of P 1 ′ P_{1}^{\prime} are of the form M 1 ∪ M 2 c M_{1}\cup M_{2}^{c} where M 1 M_{1} is an optimal answer set of P 1 P_{1} and M M corresponds to an answer set of P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) P_{2}\cup\mathit{fix_{P_{1}}(M_{1})} ; • answer sets N N of P 2 ′ ∪ 𝑓𝑖𝑥 P 1 ′ ​ ( M ) P_{2}^{\prime}\cup\mathit{fix_{P_{1}^{\prime}}(M)} are of the form M 1 ∪ M 2 c ∪ M 2 M_{1}\cup M_{2}^{c}\cup M_{2} where M 1 ∪ M 2 M_{1}\cup M_{2} is an answer set of P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) P_{2}\cup\mathit{fix_{P_{1}}(M_{1})} ; • an answer set N N of P 2 ′ ∪ 𝑓𝑖𝑥 P 1 ′ ​ ( M ) P_{2}^{\prime}\cup\mathit{fix_{P_{1}^{\prime}}(M)} satisfies C ′ C^{\prime} if and only if M 1 ∪ M 2 c M_{1}\cup M_{2}^{c} is not dominated by M 1 ∪ M 2 M_{1}\cup M_{2} and one of the following holds: 1. there exists l l such that the cost of M 1 ∪ M 2 M_{1}\cup M_{2} is different from the cost of M 1 ∪ M 2 c M_{1}\cup M_{2}^{c} ; 2. the cost of M 1 ∪ M 2 M_{1}\cup M_{2} is equal to the cost of M 1 ∪ M 2 c M_{1}\cup M_{2}^{c} for each level and M 1 ∪ M 2 M_{1}\cup M_{2} satisfies C C . Let M = M 1 ∪ M 2 c M=M_{1}\cup M_{2}^{c} be an optimal answer set of P 1 ′ P_{1}^{\prime} . If M M is not an optimal answer set of P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) P_{2}\cup\mathit{fix_{P_{1}}(M_{1})} , then M M cannot be a quantified answer set as there exists N = M 1 ∪ M 2 c ∪ M 2 N=M_{1}\cup M_{2}^{c}\cup M_{2} in the answer sets of P 2 ′ ∪ 𝑓𝑖𝑥 P ​ ( M ) P_{2}^{\prime}\cup\mathit{fix_{P}(M)} , where M 1 ∪ M 2 M_{1}\cup M_{2} is an optimal answer set of P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) P_{2}\cup\mathit{fix_{P_{1}}(M_{1})} and N N violates C ′ C^{\prime} since M 1 ∪ M 2 c M_{1}\cup M_{2}^{c} is dominated by M 1 ∪ M 2 M_{1}\cup M_{2} . On the other hand, since M M is an optimal answer set of P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) P_{2}\cup\mathit{fix_{P_{1}}(M_{1})} , then for each N = M 1 ∪ M 2 c ∪ M 2 N=M_{1}\cup M_{2}^{c}\cup M_{2} in the answer sets of P 2 ′ ∪ 𝑓𝑖𝑥 P 1 ′ ​ ( M ) P_{2}^{\prime}\cup\mathit{fix_{P_{1}^{\prime}}(M)} , M 1 ∪ M 2 c M_{1}\cup M_{2}^{c} is not dominated by M 1 ∪ M 2 M_{1}\cup M_{2} (i.e., Condition 1 is always satisfied). Thus, let N = M 1 ∪ M 2 c ∪ M 2 N=M_{1}\cup M_{2}^{c}\cup M_{2} be an answer set of P 2 ∪ 𝑓𝑖𝑥 P 1 ′ ​ ( M ) P_{2}\cup\mathit{fix_{P_{1}^{\prime}}(M)} , then N N satisfies C ′ C^{\prime} if and only if one between conditions 1 and 2 holds. Here we can observe that Condition 1 holds if and only if M 1 ∪ M 2 M_{1}\cup M_{2} is not an optimal answer set of P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) P_{2}\cup\mathit{fix_{P_{1}}(M_{1})} ; whereas Condition 2 holds if and only if M 1 ∪ M 2 M_{1}\cup M_{2} is an optimal answer set of P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) P_{2}\cup\mathit{fix_{P_{1}}(M_{1})} and M 1 ∪ M 2 M_{1}\cup M_{2} satisfies C C . Thus, M M is a quantified answer set of Π ′ \Pi^{\prime} if and only if each optimal answer set M 1 ∪ M 2 M_{1}\cup M_{2} of P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) P_{2}\cup\mathit{fix_{P_{1}}(M_{1})} satisfies C C . Hence, M M is a quantified answer set of Π ′ \Pi^{\prime} if and only if M 1 M_{1} is a quantified answer set of Π \Pi . Finally, we can conclude that Π \Pi is coherent iff Π ′ \Pi^{\prime} is coherent. Case □ 1 = ∀ s ​ t \Box_{1}=\forall^{st} and □ 2 = ∃ s ​ t \Box_{2}=\exists^{st} . By following the same working principle as before, it is possible to encode Π \Pi into a 2-ASP w (Q) program Π ′ \Pi^{\prime} which preserves the coherence of Π \Pi and in which weak constraints appear only in the first subprogram. In this case, verifying the coherence of Π ′ \Pi^{\prime} is Π 2 P \Pi_{2}^{P} -complete (Corollary 3.1 by \citeN DBLP:journals/tplp/MazzottaRT24) , then the thesis holds also in this last case. In this case, the 2-ASP w (Q) program Π ′ \Pi^{\prime} is of the form ∀ P 1 ′ ​ ∃ P 2 ′ : C ′ \forall P_{1}^{\prime}\exists P_{2}^{\prime}:C^{\prime} where: • optimal answer sets M M of P 1 ′ P_{1}^{\prime} are of the form M 1 ∪ M 2 c M_{1}\cup M_{2}^{c} where M 1 M_{1} is an answer set of P 1 P_{1} and M M is an answer set of P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) P_{2}\cup\mathit{fix_{P_{1}}(M_{1})} ; • answer sets N N of P 2 ′ ∪ 𝑓𝑖𝑥 P 1 ′ ​ ( M ) P_{2}^{\prime}\cup\mathit{fix_{P_{1}^{\prime}}(M)} are of the form M 1 ∪ M 2 c ∪ M 2 M_{1}\cup M_{2}^{c}\cup M_{2} where M 1 ∪ M 2 M_{1}\cup M_{2} is an answer set of P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) P_{2}\cup\mathit{fix_{P_{1}}(M_{1})} ; • an answer set N N of P 2 ′ ∪ 𝑓𝑖𝑥 P 1 ′ ​ ( M ) P_{2}^{\prime}\cup\mathit{fix_{P_{1}^{\prime}}(M)} satisfies C ′ C^{\prime} if and only if one of the following holds: 1. M 1 ∪ M 2 c M_{1}\cup M_{2}^{c} is dominated by M 1 ∪ M 2 M_{1}\cup M_{2} ; 2. the cost of M 1 ∪ M 2 M_{1}\cup M_{2} is equal to the cost of M 1 ∪ M 2 c M_{1}\cup M_{2}^{c} for each level and M 1 ∪ M 2 M_{1}\cup M_{2} satisfies C C . According to the ASP w (Q) semantics, Π ′ \Pi^{\prime} is incoherent if and only if there exists an optimal answer set M 1 M_{1} of P 1 ′ P_{1}^{\prime} such that for every answer set N N of P 2 ′ ∪ 𝑓𝑖𝑥 P 1 ′ ( M ) ) P_{2}^{\prime}\cup\mathit{fix_{P_{1}^{\prime}}(M)}) , N N does not satisfy C ′ C^{\prime} . Let M = M 1 ∪ M 2 c M=M_{1}\cup M_{2}^{c} be an optimal answer set of P 1 ′ P_{1}^{\prime} , with M 1 ∈ O ​ p ​ t ​ A ​ S ​ ( P 1 ) M_{1}\in OptAS(P_{1}) and M ∈ A ​ S ​ ( P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) ) M\in AS(P_{2}\cup\mathit{fix_{P_{1}}(M_{1})}) . If M 1 ∪ M 2 c M_{1}\cup M_{2}^{c} is not an optimal answer set of P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) P_{2}\cup\mathit{fix_{P_{1}}(M_{1})} , then there exists M 1 ∪ M 2 ∈ O ​ p ​ t ​ A ​ S ​ ( P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) ) M_{1}\cup M_{2}\in OptAS(P_{2}\cup\mathit{fix_{P_{1}}(M_{1})}) such that M 1 ∪ M 2 c M_{1}\cup M_{2}^{c} is dominated by M 1 ∪ M 2 M_{1}\cup M_{2} . Consequently, N = M 1 ∪ M 2 c ∪ M 2 ∈ A ​ S ​ ( P 2 ′ ∪ 𝑓𝑖𝑥 P ​ ( M ) ) N=M_{1}\cup M_{2}^{c}\cup M_{2}\in AS(P_{2}^{\prime}\cup\mathit{fix_{P}(M)}) is such that Condition 1 is satisfied, and thus M M cannot witness the incoherence of Π ′ \Pi^{\prime} . Otherwise, M 1 ∪ M 2 c M_{1}\cup M_{2}^{c} is optimal for P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) P_{2}\cup\mathit{fix_{P_{1}}(M_{1})} . In this case, for every N = M 1 ∪ M 2 c ∪ M 2 ∈ A ​ S ​ ( P 2 ′ ∪ 𝑓𝑖𝑥 P 1 ′ ​ ( M ) ) N=M_{1}\cup M_{2}^{c}\cup M_{2}\in AS(P_{2}^{\prime}\cup\mathit{fix_{P_{1}^{\prime}}(M)}) , N N satisfies C ′ C^{\prime} if and only if Condition 2 holds, that is, if and only if M 1 ∪ M 2 M_{1}\cup M_{2} has the same cost of M 1 ∪ M 2 c M_{1}\cup M_{2}^{c} (i.e., M 1 ∪ M 2 ∈ O ​ p ​ t ​ A ​ S ​ ( P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) ) M_{1}\cup M_{2}\in OptAS(P_{2}\cup\mathit{fix_{P_{1}}(M_{1})}) ) and M 1 ∪ M 2 M_{1}\cup M_{2} satisfies C C . Therefore, Π ′ \Pi^{\prime} is incoherent if and only if there exists M 1 ∈ A ​ S ​ ( P 1 ) M_{1}\in AS(P_{1}) such that no M 1 ∪ M 2 ∈ O ​ p ​ t ​ A ​ S ​ ( P 2 ∪ 𝑓𝑖𝑥 P 1 ​ ( M 1 ) ) M_{1}\cup M_{2}\in OptAS(P_{2}\cup\mathit{fix_{P_{1}}(M_{1})}) satisfies C C , which is exactly the condition for Π \Pi to be incoherent. Hence, Π ′ \Pi^{\prime} preserves the coherence of Π \Pi . 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 \citeN DBLP:journals/tplp/MazzottaRT24 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 \Box_{1}\neq\Box_{2} . Theorem 3.3 (Hardness) . The coherence problem for 2-ASP w (Q) programs of the form □ 1 ​ P 1 ​ □ 2 ​ P 2 : C \Box_{1}P_{1}\Box_{2}P_{2}:C is hard for: Σ 2 P \Sigma_{2}^{P} if □ 1 = ∃ s ​ t \Box_{1}=\exists^{st} ; Π 2 P \Pi_{2}^{P} otherwise, no matter whether □ 2 = ∃ s ​ t \Box_{2}=\exists^{st} or □ 2 = ∀ s ​ t \Box_{2}=\forall^{st} . Proof 3.4 (Proof (Sketch)) . Let us consider the different combination of quantifiers separately. (Case □ 1 = □ 2 = ∃ s ​ t \Box_{1}=\Box_{2}=\exists^{st} ). From Thm 4 by \citeN DBLP:journals/tplp/MazzottaRT24, deciding the coherence of Π \Pi is Σ 2 P \Sigma_{2}^{P} -complete if 𝒲 ​ ( P 1 ) = ∅ \mathcal{W}(P_{1})=\emptyset . Thus, the thesis holds since this is a particular case. (Case □ 1 = □ 2 = ∀ s ​ t \Box_{1}=\Box_{2}=\forall^{st} ). Let Φ = ∀ X ​ ∃ Y ​ ϕ \Phi=\forall X\exists Y\phi be a 2 2 -QBF, where X X and Y Y are disjoint set of variables and ϕ \phi is a boolean formula in 3-CNF. Verifying that Φ \Phi is true is a Π 2 P \Pi_{2}^{P} -complete problem [ 33 ] . We encode in polynomial time any Φ \Phi in a 2-ASP w (Q) program of the form ∀ s ​ t P 1 ​ ∀ s ​ t P 2 : C \forall^{st}P_{1}\forall^{st}P_{2}:C , as detailed in B . (Case □ 1 ≠ □ 2 \Box_{1}\neq\Box_{2} ). Deciding the coherence of plain alternating 2-ASP(Q) programs Σ 2 P \Sigma_{2}^{P} -complete if □ 1 = ∃ s ​ t \Box_{1}=\exists^{st} ; otherwise it is Π 2 P \Pi_{2}^{P} -complete [ 3 ] . Since this is a particular case of 2-ASP w (Q) (i.e. 𝒲 ​ ( P 1 ) = 𝒲 ​ ( P 2 ) = ∅ \mathcal{W}(P_{1})=\mathcal{W}(P_{2})=\emptyset ), then the thesis follows. Theorem 3.5 (Completeness) . The coherence problem for 2-ASP w (Q) programs of the form □ 1 ​ P 1 ​ □ 2 ​ P 2 : C \Box_{1}P_{1}\Box_{2}P_{2}:C is: Σ 2 P \Sigma_{2}^{P} -complete if □ 1 = ∃ s ​ t \Box_{1}=\exists^{st} ; Π 2 P \Pi_{2}^{P} -complete otherwise, no matter whether □ 2 = ∃ s ​ t \Box_{2}=\exists^{st} or □ 2 = ∀ s ​ t \Box_{2}=\forall^{st} . Proof 3.6 . The thesis follows from Theorem 1 and 3.3 . From Theorem 3.5 , we derive complete results for the brave reasoning task in 2-ASP w (Q), which asks whether an atom a a is true in some optimal quantified answer set. Theorem 3.7 . Let Π \Pi be an existential 2-ASP w (Q) program of the form □ 1 ​ P 1 ​ □ 2 ​ P 2 : C : C ω \Box_{1}P_{1}\Box_{2}P_{2}:C:C^{\omega} and a a be a ground atom, then verifying whether a ∈ M a\in M , with M ∈ O ​ p ​ t ​ Q ​ A ​ S ​ ( Π ) M\in OptQAS(\Pi) , is Δ 3 P \Delta_{3}^{P} -complete no matter whether □ 2 = ∃ s ​ t \Box_{2}=\exists^{st} or □ 2 = ∀ s ​ t \Box_{2}=\forall^{st} . These results strengthen those of \citeN DBLP:journals/tplp/MazzottaRT24, as they establish completeness for all combinations of quantifiers, rather than for alternating programs only. 4 Solving 2-ASP w (Q) via CEGAR Counterexample-Guided Abstraction Refinement (CEGAR) [ 15 ] 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 [ 30 ] and 2-ASP(Q) solving [ 16 ] . Building on these ideas, we propose a CEGAR-based approach for the evaluation of 2-ASP w (Q) programs. In the following we give a game-theoretic characterization of the semantics of 2-ASP w (Q) and then we focus on the two stages of CEGAR: abstraction refinement and counterexample search . 4.1 The 2-ASP w (Q) Game Let □ ∈ { ∃ s ​ t , ∀ s ​ t } \Box\in{\exists^{st},\forall^{st}} be a quantifier, then the opponent of □ \Box is □ ¯ = ∀ s ​ t \overline{\Box}=\forall^{st} if □ = ∃ s ​ t \Box=\exists^{st} ; otherwise □ ¯ = ∃ s ​ t \overline{\Box}=\exists^{st} . Thus, for any alternating 2-ASP w (Q) program □ 2 \Box_{2} is the opponent of □ 1 \Box_{1} , that is, □ 2 = □ 1 ¯ \Box_{2}=\overline{\Box_{1}} . In what follows, w.l.o.g., we consider 2-ASP w (Q) programs of the form: □ ​ P 1 ​ □ ¯ ​ P 2 : C : C ω \Box P_{1}\overline{\Box}P_{2}:C:C^{\omega} (1) Let Π \Pi be a 2-ASP w (Q) program of the form ( 1 ), then a move for □ \Box is an answer set M 1 ∈ O ​ p ​ t ​ A ​ S ​ ( P 1 ) M_{1}\in OptAS(P_{1}) . Given a move M 1 M_{1} for □ \Box , for each M 2 ∈ O ​ p ​ t ​ A ​ S ​ ( P 2 ∪ 𝑓