Beyond NP: Quantifying over Answer Sets

TL;DR

This paper introduces ASP with Quantifiers (ASP(Q)), an extension of Answer Set Programming that enables modeling of problems in the Polynomial Hierarchy by adding quantifiers over stable models, thus expanding ASP's expressiveness.

Contribution

The paper proposes ASP(Q), a novel extension of ASP that incorporates quantifiers over stable models, allowing direct modeling of problems beyond NP in the Polynomial Hierarchy.

Findings

ASP(Q) can model problems in the Polynomial Hierarchy.

ASP(Q) demonstrates natural encodings for complex AI and number theory problems.

Comparison shows ASP(Q) extends ASP's modeling capabilities significantly.

Abstract

Answer Set Programming (ASP) is a logic programming paradigm featuring a purely declarative language with comparatively high modeling capabilities. Indeed, ASP can model problems in NP in a compact and elegant way. However, modeling problems beyond NP with ASP is known to be complicated, on the one hand, and limited to problems in {\Sigma}^P_2 on the other. Inspired by the way Quantified Boolean Formulas extend SAT formulas to model problems beyond NP, we propose an extension of ASP that introduces quantifiers over stable models of programs. We name the new language ASP with Quantifiers (ASP(Q)). In the paper we identify computational properties of ASP(Q); we highlight its modeling capabilities by reporting natural encodings of several complex problems with applications in artificial intelligence and number theory; and we compare ASP(Q) with related languages. Arguably, ASP(Q) allows one to model problems in the Polynomial Hierarchy in a direct way, providing an elegant expansion of ASP beyond the class NP. Under consideration for acceptance in TPLP.

Equations

$$a_1\vee \dots \vee a_l\leftarrow b_1,\dots ,b_m,not{c}_1,\dots ,not{c}_n,$$

$${\square }_1{P}_1{\square }_2{P}_2\cdots {\square }_n{P}_n:C,$$

$$\min_{f\in J^{I}}\;\max\{|Q|:\mbox{$Q$ is a clique of $G_{f}$}\}\geq k.$$

$$\min_{f\in J^{I}}\;\max\{|Q|:\mbox{$Q$ is a clique of $G_{f}$}\}\geq k$$

$$P_1=\{\{x_1,\dots ,x_n\}\},P_2=\{\{y_1,\dots ,y_m\}\},$$

$$C=\{sat\leftarrow\sigma(L_{i,1}),\ldots,\sigma(L_{i,k_{i}})\mid\forall i=1,\ldots,m\}\cup\{\leftarrow{\color[rgb]{0,0,0}not}\ sat\}.$$

Full text

1 Introduction

Answer Set Programming (ASP) [Brewka et al. (2011)] is a logic programming paradigm for modeling and solving search and optimization problems. It is supported by a purely declarative formalism of logic programs with the semantics of stable models [Gelfond and Lifschitz (1991)] (also known as answer sets [Lifschitz (2002)]), and by several systems able to compute them [Gebser et al. (2018)]. ASP was primarily aimed at problems whose decision versions are in the class NP. Indeed, ASP can model problems in NP in a compact and elegant way by means of an intuitive and easy to follow methodology known as generate-define-test [Lifschitz (2002)] (also known as guess and check [Eiter et al. (2000)]). Furthermore, implementations such as clasp [Gebser et al. (2015)], and wasp [Alviano et al. (2015)] have been shown to be effective in solving problems of practical interest on industrial-grade instances [Erdem et al. (2016)].

Modeling problems beyond the class NP with ASP is possible to some extent. Namely, when disjunctions are allowed in the heads of rules, every decision problem in the class $\Sigma_{2}^{P}$ can be modeled in a uniform way by a finite program [Dantsin et al. (2001)]. However, modeling problems beyond NP with ASP is complicated and the generate-define-test approach is no longer sufficient in general. Additional techniques such as saturation [Eiter and Gottlob (1995)] are needed but they are difficult to use, and may introduce constraints that have no direct relation to constraints of the problem being modeled. As stated explicitly in [Gebser et al. (2011)] “unlike the ease of common ASP modeling, […] these techniques are rather involved and hardly usable by ASP laymen.”

The primary goal of our work is to address the shortcomings of ASP in modeling problems beyond NP. Building on the way Quantified Boolean formulas (QBFs) extend SAT formulas to model problems from PSPACE, we propose a generalization of ASP that introduces quantifiers over stable models of programs. We name the new language ASP with Quantifiers (ASP(Q)) and refer to programs in that language as quantified programs.

In the paper we formally introduce the language ASP(Q) and its semantics. We identify computational properties of ASP(Q). In particular, we show that every problem in the Polynomial Hierarchy can be uniformly modeled by a quantified program. Moreover, we show that no loss of expressivity results if we restrict programs defining quantifiers to be normal. An important consequence of that observation is that when using ASP(Q) to model problems, one can resort to the generate-define-test approach to specify these “quantifying” programs. This typically simplifies modeling and verifying correctness. We illustrate these claims by presenting natural encodings of several complex problems with applications in artificial intelligence and mathematics.

In the last part of the paper, we compare ASP(Q) with alternative approaches for modeling problems beyond NP. Earlier efforts in this direction include: the stable-unstable formalism [Bogaerts et al. (2016)], various program transformations [Eiter and Polleres (2006), Redl (2017), Faber and Woltran (2011)], applications of meta-programming [Redl (2017), Gebser et al. (2011)] and more.111For example, weak constraints allow to model decision problems that are $\Delta_{3}^{P}$-complete [Buccafurri et al. (2000)]. In particular, we deepen the comparison with disjunctive programs and the stable-unstable formalism, indicating key differences and their implications by means of additional modeling examples. We also extensively compare ASP(Q) with the language of QBFs, which served as a direct inspiration for our work. A single sentence summary of our work is: ASP(Q) allows one to model problems in the Polynomial Hierarchy in a direct way, providing an elegant expansion of ASP beyond the class NP.

2 Formal Framework

We start by recalling syntax and semantics of Answer Set Programming (ASP). We then introduce syntax and semantics of ASP with Quantifiers (ASP(Q)).

2.1 Answer Set Programming

Let $\mathcal{R}$ be a set of predicates, $C$ a set of constants, and $V$ a set of variables. A term is a constant or a variable. An atom $a$ of arity $n\in\mathbb{N}$ is of the form $p(t_{1},...,t_{n})$, where $p$ is a predicate from $\mathcal{R}$ and $t_{1},...,t_{n}$ are terms. A disjunctive rule $r$ is of the form

[TABLE]

where all $a_{i}$, $b_{j}$, and $c_{k}$ are atoms; $l,m,n\geq 0$ and $l+m+n>0$; $not$ represents negation-as-failure, also known as default negation. The set $H(r)=\{a_{1},...,a_{l}\}$ is the head of $r$; the sets $B^{+}(r)=\{b_{1},...,b_{m}\}$ and $B^{-}(r)=\{c_{1},\ldots,c_{n}\}$ are the sets of the positive body and the negative body atoms of $r$, respectively. A rule $r$ is safe if each of its variables occurs in some positive body atom. We restrict attention to programs built of safe rules only. A rule $r$ is a fact, if $B^{+}(r)\cup B^{-}(r)=\emptyset$ (we then omit $\leftarrow$ from the notation); a constraint, if $H(r)=\emptyset$; normal, if $|H(r)|\leq 1$; and positive, if $B^{-}(r)=\emptyset$. A (disjunctive logic) program $P$ is a finite set of disjunctive rules. $P$ is called normal [resp. positive] if each $r\in P$ is normal [resp. positive]. We define $At(P)=\bigcup_{r\in P}At(r)$, that $At(P)$ is the set of all atoms occurring in the program $P$. A program $P$ is stratified if there is a level mapping $\|.\|_{s}$ of $P$ such that for every rule $r$ of $P$: $(i)$ For any predicate $p$ occurring in $B^{+}(r)$, and for any $p^{\prime}$ occurring in $H(r)$, $\|p\|_{s}\leq\|p^{\prime}\|_{s}$, and $(ii)$ For any predicate $p$ occurring in $B^{-}(r)$, and for any $p^{\prime}$ occurring in $H(r)$, $\|p\|_{s}<\|p^{\prime}\|_{s}$.

The Herbrand universe of $P$, denoted by $U_{P}$, is the set of all constants appearing in $P$, except that when no constants appear in $P$, we take $U_{P}=\{a\}$, where $a$ is an arbitrary constant. The Herbrand base of $P$, denoted as $B_{P}$, is the set of all ground atoms that can be obtained from the predicate symbols appearing in $P$ and the constants of $U_{P}$. Given a rule $r$ occurring in a program $P$, a ground instance of $r$ is a rule obtained from $r$ by replacing every variable $X$ in $r$ by $\sigma(X)$, where $\sigma$ is a substitution mapping the variables occurring in $r$ to constants in $U_{P}$. The ground instantiation of $P$, denoted by $ground(P)$, is the set of all the ground instances of the rules occurring in $P$. Any set $I\subseteq B_{P}$ is an interpretation; it is a model of a program $P$ (denoted $I\models P$) if for each rule $r\in ground(P)$, we have $I\cap H(r)\neq\emptyset$ whenever $B^{+}(r)\subseteq I$ and $B^{-}(r)\cap I=\emptyset$ (in such case, $I$ is a model of $r$, denoted $I\models r$). A model $M$ of $P$ is minimal if no model $M^{\prime}\subset M$ of $P$ exists. We denote by $MM(P)$ the set of all minimal models of $P$.

For a program $P$ without constraints we write $P^{I}$ for the well-known Gelfond-Lifschitz reduct [Gelfond and Lifschitz (1991)] with respect to interpretation $I$, that is, the set of rules $H(r)\leftarrow B^{+}(r)$, obtained from rules $r\in ground(P)$ such that $B^{-}(r)\cap I=\emptyset$. An answer set (or stable model) of a program $P$ without constraints is an interpretation $I$ such that $I\in MM(P^{I})$. For the general case, we write $P_{\leftarrow}$ for the set of constraints of a disjunctive logic program $P$. We denote by $AS(P)$ the set of all answer sets (or stable models) of such programs $P$, that is, the set of all answer sets of $P\setminus P_{\leftarrow}$ that are models for $P_{\leftarrow}$.

We say that a program $P$ is coherent, if it has at least one answer set (that is, $AS(P)\neq\emptyset$), otherwise, $P$ is incoherent.

2.2 Answer Set Programming with Quantifiers

An ASP with Quantifiers (ASP(Q)) program $\Pi$ is an expression of the form:

[TABLE]

where, for each $i=1,\ldots,n$, $\Box_{i}\in\{\exists^{st},\forall^{st}\}$, $P_{i}$ is an ASP program, and $C$ is a stratified normal ASP program.222This condition is sufficient to model compactly constraints by exploiting the modeling advantages of inductive definitions. $C$ is contemplated in the definition of ASP(Q) just because it makes more natural the modeling of problems. Symbols $\exists^{st}$ and $\forall^{st}$ are named existential and universal answer set quantifiers, respectively. An ASP(Q) program $\Pi$ of the form (2) is existential (universal, respectively) if $\Box_{1}=\exists^{st}$ ($=\forall^{st}$, respectively). If for each $i=1,\ldots,n$ the ASP program $P_{i}$ is normal, then $\Pi$ is called a normal ASP(Q) program. Given a logic program $P$ and an intepretation $I$ over $B_{P}$, and an ASP(Q) program $\Pi$ the form (2), we denote by $fix_{P}(I)$ the set of facts and constraints $\{a\mid a\in I\}\cup\{\leftarrow a\mid a\in B_{P}\setminus I\}$, and by $\Pi_{P,I}$ the ASP(Q) program of the form (2), where $P_{1}$ is replaced by $P_{1}\cup fix_{P}(I)$, that is, $\Pi_{P,I}$ $=$ $\Box_{1}(P_{1}\cup fix_{P}(I))\cdots\Box_{n}P_{n}:C$. We now define coherence of ASP(Q) programs by induction on the number of quantifiers in the program.

• •

$\exists^{st}P:C$ is coherent, if there exists $M\in AS(P)$ such that $C\cup fix_{P}(M)$ is coherent;

• •

$\forall^{st}P:C$ is coherent, if for every $M\in AS(P)$, $C\cup fix_{P}(M)$ is coherent;

• •

$\exists^{st}P\ \Pi$ is coherent, if there exists $M\in AS(P)$ such that $\Pi_{P,M}$ is coherent;

• •

$\forall^{st}P\ \Pi$ is coherent, if for every $M\in AS(P)$, $\Pi_{P,M}$ is coherent.

For instance, an ASP(Q) program $\Pi=\exists^{st}P_{1}\forall^{st}P_{2}\cdots\exists^{st}P_{n-1}\forall^{st}P_{n}:C$ is coherent if there exists an answer set $M_{1}$ of $P_{1}^{\prime}$ such that for each answer set $M_{2}$ of $P_{2}^{\prime}$ there is an answer set $M_{3}$ of $P_{3}^{\prime},\ldots,$ there is an answer set $M_{n-1}$ of $P_{n-1}^{\prime}$ such that for each answer set $M_{n}$ of $P_{n}^{\prime}$, there is an answer set of $C\cup fix_{P_{n}^{\prime}}(M_{n})$, where $P_{1}^{\prime}=P_{1}$, and $P_{i}^{\prime}=P_{i}\cup fix_{P_{i-1}^{\prime}}(M_{i-1})$, if $i\geq 2$.

For an ASP(Q) program $\Pi$ of the form (2) such that $\Box_{1}=\exists^{st}$, we say that $M\in AS(P_{1})$ is a quantified answer set of $\Pi$, whenever $(\Box_{2}P_{2}\cdots\Box_{n}P_{n}:C)_{P_{1},M}$ is coherent, in case of $n>1$, and whenever $C\cup fix_{P_{1}}(M)$ is coherent, in case of $n=1$. We denote by $QAS(\Pi)$ the set of all quantified answer sets of $\Pi$. Finally, note that the definition of quantified answer set can be naturally extended to programs with strong negation, choice rules, aggregates and other extensions [Gebser and Schaub (2016)]. Thus, in the examples we resort also to these extensions that are part of the ASPCore standard input language [Gebser et al. (2018)].

Example 1

Consider the ASP(Q) program $\Pi=\exists^{st}P_{1}\forall^{st}P_{2}:C$, where $P_{1}=\{a(1)\vee a(2)\}$, $P_{2}=\{b(1)\vee b(2)\leftarrow a(1);\ b(2)\leftarrow a(2)\}$, and $C=\{\leftarrow b(1),\ not\ b(2)\}$. The program $P_{1}$ has two answer sets $\{a(1)\}$ and $\{a(2)\}$. Hence, to establish the coherence of $\Pi$, we have to check if at least one of $\{a(1)\}$ and $\{a(2)\}$ is a quantified answer set of $\Pi$. Considering $\{a(1)\}$, we have $fix_{P_{1}}(\{a(1)\})=\{a(1);\leftarrow a(2)\}$. Under the notation used above, $P_{2}^{\prime}=P_{2}\cup fix_{P_{1}}(\{a(1)\})$. Thus, $AS(P_{2}\cup fix_{P_{1}}(\{a(1)\}))=\{\{a(1),b(1)\},\{a(1),b(2)\}\}$. For $M=\{a(1),b(1)\}$ we have $fix_{P_{2}^{\prime}}(M)=\{a(1);$ $b(1);\;\leftarrow a(2);\;\leftarrow b(2)\}$, and it is clear that the program $C\cup fix_{P_{2}^{\prime}}(M)$ is not coherent. Therefore, $\{a(1)\}$ is not a quantified answer set of $\Pi$. On the other hand, a similar analysis for the other answer set of $P_{1}$, $\{a(2)\}$, shows that it is a quantified answer set of $\Pi$.

ASP(Q) is a straightforward generalization of ASP in a sense made formal in the following theorem.

Theorem 1

Let $P$ be an ASP program, and let $\Pi$ be the ASP(Q) program of the form (2), where $n=1$, $\Box_{1}=\exists^{st}$, $P_{1}=P$, and $C=\emptyset$. Then, $AS(P)=QAS(\Pi)$.

Proof 2.2**.**

By definition, $M$ is a quantified answer set of $\Pi$ if and only if $M$ is an answer set of $P$ and $\emptyset\cup fix_{P}(M)=fix_{P}(M)$ is coherent. The latter condition is trivially true as $M$ is an answer set of $fix_{P}(M)$.

3 Complexity issues

We now study the computational properties of the ASP(Q) language. As it is customary in the literature we focus on the ground case, that is we assume that no variable occurs in programs.

Because it is possible to alternate universal and existential answer set quantifiers, it is clear that ASP(Q) can model probelms beyond NP. In particular, each problem in PSPACE can be modeled by using an ASP(Q) program. Formally, we define the Coherence problem as follows: Given an ASP(Q) program $\Pi$ as input, decide whether $\Pi$ is coherent.

Theorem 3.3**.**

The Coherence problem is PSPACE-complete, even under the restriction to normal ASP(Q) programs.

Proof 3.4**.**

(Membership) It is well known that answer sets of a disjunctive logic program can be enumerated in polynomial space in the size of the program. Let us assume that $p$ is a polynomial providing that bound. We prove that the coherence of an $ASP(Q)$ program $\Pi$ of the form (2) can be decided in space $O(n\times p(s(\Pi)))$, where $s(\Pi)$ is the size of $\Pi$, and $n$ is the number of quantifiers in $\Pi$.

To this end, we consider the following recursive algorithm. It consists of enumerating all answer sets of $P_{1}$. If $n=1$, we have $\Pi=\Box P_{1}:C$. To decide coherence, for each enumerated answer set $M$ of $P_{1}$, we decide whether $C\cup fix_{P_{1}}(M)$ is coherent. Depending on whether $\Box=\exists^{st}$ or $\forall^{st}$, if for some (every) answer set $M$ of ${P_{1}}$, $C\cup fix_{P_{1}}(M)$ is coherent, we return that $\Pi$ is coherent. Otherwise, we return that $\Pi$ is not coherent. For $n\geq 2$, for each enumerated answer set $M$ of ${P_{1}}$, we recursively check whether $\Pi^{\prime}=(\Box_{2}P_{2}\ldots\Box_{n}P_{n}:C)_{P_{1},M}$ is coherent, and decide about coherence of $\Pi$ similarly as in the case $n=1$, depending on the outermost quantifier.

By the comment above, we can enumerate all answer sets $M$ of $P_{1}$ in space $O(p(s(\Pi)))$ (indeed, $s(P_{1})=O(s(\Pi))$). Moreover, if $n=1$, testing coherence of $C\cup fix_{P_{1}}(M)$ can be accomplished in time and so, also in space $O(s(C\cup fix(M)))=O(s(\Pi))$. Thus, if $n=1$, the algorithm requires $O(p(s(\Pi)))$ space, establishing the base case of the induction. If $n\geq 2$, we need $O(p(s(\Pi)))$ space for enumerating answer sets and, using the induction hypothesis, $O((n-1)\times p(s(\Pi)))$ space for each recursive call. Thus, the total space requirement is $O(n\times p(s(\Pi)))$, completing the inductive step.

We now observe that $n=O(s(\Pi))$, which shows that the algorithm we described runs in space $O(s(\Pi)\times p(s(\Pi)))$. This implies the assertion.

(Hardness) We give a reduction from the problem of deciding the validity of a QBF formula $\Phi=Q_{1}x_{1}\ldots Q_{n}x_{n}\varphi$, where for every $i=1,\ldots,n$, $Q_{i}\in\{\exists,\forall\}$ and $x_{i}$ is a propositional variable, and where $\varphi$ is a propositional formula over $\{x_{1},\ldots,x_{n}\}$. The problem is PSPACE-complete even when $\varphi$ is in 3-CNF. Thus, let us assume that $\varphi=C_{1}\wedge\ldots\wedge C_{m}$, where $C_{j}=l_{j}^{1}\vee l_{j}^{2}\vee l_{j}^{3}$ and $l_{j}^{1},l_{j}^{2},l_{j}^{3}\in\{x_{i},\neg x_{i}\mid i=1,\ldots,n\}$, for each $j=1,\ldots,m$. We construct an ASP(Q) program $\Pi$ as follows. For each $i=1,\ldots,n$, we define $P_{i}=\{x_{i}\leftarrow not\ nx_{i};\ nx_{i}\leftarrow not\ x_{i}\}$ and $\Box_{i}=Q_{i}^{st}$. We also define $C=\{ok_{j}\leftarrow\sigma(l_{j}^{h})\mid j=1,\ldots,m\mbox{ and }h=1,2,3\}\cup\{\;\leftarrow not\ ok_{i}\mid i=1,\ldots,m\}$, where $\sigma(l)=x_{i}$ if $l=x_{i}$, and $\sigma(l)=nx_{i}$ if $l=\neg x_{i}$. It is easy to see that $\Pi$ is coherent iff $\Phi$ is valid. Moreover, as each program $P_{i}$ is normal, $\Pi$ is a normal ASP(Q) program.

As for QBFs, there is a direct correspondence between the number of alternating quantifiers and the level of the Polynomial Hierarchy (PH) for which we have competeness of the coherence problem.

Theorem 3.5**.**

The Coherence problem is $(i)$ $\Sigma^{P}_{n}$-complete for normal existential ASP(Q) programs with $n$ quantifiers in the prefix; and $(ii)$ $\Pi^{P}_{n}$-complete for normal universal ASP(Q) programs with $n$ quantifiers in the prefix.

Proof 3.6**.**

(Membership) We proceed by induction on $n$. We start with $n=1$. If $\Pi=\exists^{st}{P_{1}}:C$ then deciding coherence amounts to checking whether there is an answer set $I$ of ${P_{1}}$ such that $fix_{P_{1}}(I)\cup C$ is coherent. This problem is in NP ($=\Sigma_{1}^{P}$) because one can check coherence of a normal stratified program with constraints in polynomial time [Dantsin et al. (2001)]. If $\Pi=\forall^{st}{P_{1}}:C$ then deciding coherence amounts to checking whether there is no answer set $I$ of ${P_{1}}$ such that $fix_{P_{1}}(I)\cup C$ is not coherent. This problem is in co-NP ($=\Pi_{1}^{P}$) because its complement, the problem to decide whether there is an answer set $I$ of ${P_{1}}$ such that $fix_{P_{1}}(I)\cup C$ is not coherent, is in NP (indeed, one can check coherence of a normal stratified program with constraints in polynomial time).

Next, let us assume that $n\geq 2$. Further, let $\Pi$ be a normal ASP(Q) program of the form (2). If $\Box_{1}=\exists^{st}$, then to decide coherence of $\Pi$ we have to decide whether there is an interpretation $I$ such that $I$ is an answer set of $P_{1}$ and $\Pi_{P_{1},I}$ is coherent. Checking that $I$ is an answer set of $P$ is a polynomial-time task (we recall that $P_{1}$ is normal). Checking that $\Pi_{P_{1},I}$ is coherent can be accomplished with a call to an oracle for a problem in $\Sigma_{n-1}^{P}$ or in $\Pi_{n-1}^{P}$ depending on whether $\Box_{2}$ in $\Pi$ is $\exists^{st}$ or $\forall^{st}$. Indeed, by the induction hypothesis, the problem of deciding coherence for normal $ASP(Q)$ programs with $n-1$ quantifiers and with the outermost quantifier fixed to $\exists^{st}$ ($\forall^{st}$, respectively) is in $\Sigma_{n-1}^{P}$ ($\Pi_{n-1}^{P}$, respectively).

If $\Box_{1}=\forall^{st}$, to decide coherence of $\Pi$ we have to decide that for every answer set of $P_{1}$, $\Pi_{P_{1},I}$ is coherent. The complement to this problem consists of deciding whether there is an an answer set $I$ of $P_{1}$ such that $\Pi_{P_{1},I}$ is not coherent. By a similar argument as above, this problem is in $\Sigma_{n}^{P}$ (observe that an oracle deciding whether an $ASP(Q)$ program is coherent, can be used to decide whether an $ASP(Q)$ program is not coherent). It follows that deciding coherence for programs with $n$ quantifiers in the prefix and with $\forall^{st}$ as the outermost quantifier is in $\Pi_{n}^{P}$.

(Hardness) Let us consider a QBF $\Phi=Q_{1}X_{1}\ldots Q_{n}X_{n}\varphi$, where $X_{1},\ldots,X_{n}$ are disjoint sets of propositional variables, each $Q_{i}=\exists$ or $\forall$, the quantifiers alternate, and $\varphi$ is a 3-CNF or 3-DNF formula over the variables in $X_{1}\cup\ldots\cup X_{n}$. We encode $\Phi$ as an $ASP(Q)$ program $\Pi_{\Phi}$ of the form (2) as follows. For every $i=1,\ldots,n$, we set $\Box_{i}=Q_{i}^{st}$ and $P_{i}=\{x\leftarrow not\ nx\mid x\in X_{i}\}\cup\{nx\leftarrow not\ x\mid x\in X\}$ (similarly as in the previous proof). If $\varphi$ is a 3-CNF formula, we define a normal stratified program with constraints $C$ as in the previous proof. So, assume $\varphi$ is a 3-DNF formula, say $\varphi=D_{1}\vee\ldots\vee D_{m}$, where $D_{j}=l_{j}^{1}\wedge l_{j}^{2}\wedge l_{j}^{3}$ and $l_{j}^{1},l_{j}^{2},l_{j}^{3}\in X_{1}\cup\ldots\cup X_{n}$, for each $j=1,\ldots,m$. In this case, we set $C=\{ok_{j}\leftarrow\sigma(l_{j}^{1}),\sigma(l_{j}^{2}),\sigma(l_{j}^{3})\mid j=1,\ldots,m\}\cup\{\leftarrow not\ ok_{1},\ldots,not\ ok_{m}\}$, where $\sigma(l)=x$ if $l=x$, and $\sigma(l)=nx$ if $l=\neg x$.

It is easy to see that in both cases $\Phi$ is valid iff $\Pi_{\Phi}$ is coherent. Moreover, both encodings can be obtained by a polynomial-time procedure. Now, according to well-known complexity results [Stockmeyer (1976)] the problem to decide validity for QBFs such that (1) $Q_{1}=\exists$, $\varphi$ is in 3-DNF, and $n$ is even; (2) $Q_{1}=\exists$, $\varphi$ is in 3-CNF, and $n$ is odd; (3) $Q_{1}=\forall$, $\varphi$ is in 3-CNF, and $n$ is even; (4) $Q_{1}=\forall$, $\varphi$ is in 3-DNF and $n$ is odd is $\Sigma_{n}^{P}$-complete for the cases (1) and (2), and $\Pi_{n}^{P}$-complete for the cases (3) and (4). Thus, the hardness follows.

We note that, for classes of disjunctive programs that can be translated in polynomial time to normal ones, such as Head-Cycle Free (HCF) [Ben-Eliyahu and Dechter (1996)], the correspondence between quantifier alternations and the level of the Polynomial Hierarchy is preserved.

We also note that the theorem concerns, in each of the two cases, the corresponding class of all ASP(Q) programs with $n$ quantifiers. In particular, the membership part is proved for that class. The proof of hardness explicitly usues special programs in that class, the ones in which quantifiers alternate.

4 Modeling in ASP(Q)

In this section, we focus on the modeling capabilities of our language. Thus, we study some well-known problems that are computationally beyond NP, and show how to solve them in ASP(Q).

4.1 Minmax Clique

Minmax problems play a key role in various fields of research, including game theory, combinatorial optimization and computational complexity [Cao et al. (1995)]. A minimax problem can be formulated as $min_{x\in X}max_{y\in Y}f(x,y)$, where $f(x,y)$ is a function defined on the product set of $X$ and $Y$. Here, we focus on the so-called Minmax Clique problem [Ko (1995)], but our approach can be easily adapted to model other minmax problems.

Let $G=\langle N,E\rangle$ be a graph, $I$ and $J$ two finite sets of indices, and $(A_{i,j})_{i\in I,j\in J}$ a partition of $N$. We write $J^{I}$ for the set of all total functions from $I$ to $J$. For every total function $f\colon I\rightarrow J$ we denote by $G_{f}$ the subgraph of $G$ induced by $\bigcup_{i\in I}A_{i,f(i)}$. We define the Minmax Clique problem as follows: Given a graph $G$, sets of indices $I$ and $J$, a partition $(A_{i,j})_{i\in I,j\in J}$ (all as above), and an integer $k$, decide whether

[TABLE]

It is known that this problem is $\Pi_{2}^{p}$-complete [Ko (1995)].

Consider the following ASP(Q) program $\Pi=\forall^{st}P_{1}\exists^{st}P_{2}:C$. The ASP program $P_{1}$ is given by:

P_{1}=\left\{\begin{array}[]{rcll}\mathit{edge}(a,b)&&&\forall(a,b)\in E\\ \mathit{node}(a)&&&\forall a\in N\\ v(i,j,a)&&&\forall i\in I,\ j\in J,\ a\in A_{i,j}\\ setI(X)&\leftarrow&v(X,\_,\_)\\ setJ(X)&\leftarrow&v(\_,X,\_)\\ 1\{f(X,Y):setJ(Y)\}1&\leftarrow&setI(X)\end{array}\right\}

Informally, the role of $P_{1}$ is to specify the input graph, the sets $I$ and $J$ of indices, a partition $(A_{i,j})$, and the search space of all total functions from $I$ to $J$. Specifically, the first two sets of facts encode the graph by using two predicates: a binary one named $\mathit{edge}$, collecting all edges of the graph; and a unary one named $\mathit{node}$ collecting all nodes of the graph. Then, the third set of facts encodes the partition $(A_{i,j})$ by using a ternary predicate $v$. Projections applied to $v$ (rules four and five) define elements of the sets $I$ and $J$, respectively. Finally, the last rule defines the space of all total functions $f$ from $I$ to $J$. The ASP program $P_{2}$ is defined as follows:

P_{2}=\left\{\begin{array}[]{rcl}\mathit{inInduced}(Z)&\leftarrow&v(X,Y,Z),\ f(X,Y)\\ \mathit{edgeP}(X,Y)&\leftarrow&\mathit{edge}(X,Y),\ \mathit{inInduced}(X),\ \mathit{inInduced}(Y)\\ \{\mathit{inClique}(X)\,:\,\mathit{inInduced}(X)\}&&\\ &\leftarrow&\mathit{inClique}(X),\ \mathit{inClique}(Y),\ not\ \mathit{edgeP}(X,Y)\end{array}\right\}

Its role is to define the subgraph $G_{f}$ of $G$ determined by a total function $f$, and to select a clique in this subgraph. In particular, the first rule defines the set of nodes of the subgraph $G_{f}$ (whenever a node $Z$ belongs to the set $A_{X,Y}$, and the function $f$ maps $X$ to $Y$, then $Z$ is a node of $G_{f}$). The second rule ensures that whenever there is an edge from $X$ to $Y$, and both $X$ and $Y$ are nodes of $G_{f}$, then the edge $(X,Y)$ is an edge of $G_{f}$ ($G_{f}$ is the induced subgraph). The third rule allows to select nodes of the partition as candidates for a clique. The final constraint requires that it is not possible that two nodes $X$ and $Y$ are in a clique and there is no edge in the subgraph $G_{f}$ from $X$ to $Y$. Finally, the program $C$ is defined as follows.

C=\left\{\begin{array}[]{cl}\leftarrow&\#\mbox{count}\{X:\mathit{inClique}(X)\}<k\end{array}\right\}

The constraint forces the number of nodes in a clique to be greater or equal to $k$.

Intuitively, we check if for each answer set of $P_{1}$, that is for each total function $f$ from $I$ to $J$, there exists an answer set of $P_{2}$, that is a clique in the subgraph of $G$ induced by $f$, such that its cardinality is not less than $k$. If so, a quantified answer set of $\Pi$ exists.

Theorem 4.7**.**

Let $\mathcal{I}=\langle G,(A_{i,j})_{i\in I,j\in J},k\rangle$ be an instance of the Minmax Clique problem. Then,

[TABLE]

if and only if the ASP(Q) program $\Pi$, defined as above, has a quantified answer set.

4.2 Pebbling Number

Graph pebbling is a well-known mathematical game [Hurlbert (1999)]. It was first suggested as a tool for solving a particular problem in number theory [Chung (1989)]. The game consists of a graph with pebbles placed on (some of) its nodes. The goal is to place a pebble on a target node by performing a sequence of pebbling moves. More formally, let $G=\langle N,E\rangle$ be a directed graph whose nodes may contain pebbles. A pebbling move along an edge $(a,b)\in E$ requires that node $a$ contains at least two pebbles; the move removes two pebbles from $a$ and adds one pebble to $b$. The pebbling number, denoted by $\pi(G)$, is the smallest number of pebbles such that for every assignment of $k$ pebbles to nodes of $G$ and for every node $w\in N$ (the target), some sequence (possibly empty) of pebbling moves results in a pebble on $w$. The Pebbling number problem asks whether $\pi(G)$ is less than or equal to $k$. This problem is $\Pi_{2}^{p}$-complete, and it remains so also when the target node is part of the input [Milans and Clark (2006)]. (For the latter version,we redefine $\pi(G)$ accordingly.)

To capture the definition of the Pebbling number problem we construct an ASP(Q) program $\Pi=\forall^{st}P_{1}\exists^{st}P_{2}:C$. Its program $P_{1}$ is defined as follows:

P_{1}=\left\{\begin{array}[]{rcll}edge(a,b)&&\forall(a,b)\in E\\ node(a)&&\forall a\in N\\ pebble(i)&&\forall i=0,1,\ldots,k\\ 1\{onNode(X,N):pebble(N)\}1&\leftarrow&node(X)\\ &\leftarrow&\#\mbox{sum}\{N,X:onNode(X,N)\}\neq k&\\ 1\{target(X):node(X)\}1&&\end{array}\right\}

The first two sets of facts encode the input graph, and the third one the set of integers that can serve as the number of pebbles a node can have. The first rule of the program (line 4) selects, for each node $X$, the number $N$ of pebbles on $X$. The second rule (line 5) ensures the total number of pebbles on all nodes of $G$ is $k$. The last rule selects exactly one node as the target allowing any node to be selected. Thus, answer sets of $P_{1}$ capture all possible “input configurations” for $G$, each configuration defined by a distribution of $k$ pebbles among nodes of $G$ and the target node.

The ASP program $P_{2}$ in $\Pi$ is defined as follows:

P_{2}=\left\{\begin{array}[]{rcl}\step(i)&&\forall i=0,1,\ldots,k-1\\ 1\{\mathit{endstep}(S):\step(S)\}1\\ \mathit{onNode}(X,N,0)&\leftarrow&\mathit{onNode}(X,N)\\ 1\{\mathit{move}(X,Y,S):\mathit{edge}(X,Y)\}1&\leftarrow&\step(S),\mathit{endstep}(T),1\leq S,\ S\leq T\\ &\leftarrow&\mathit{move}(X,Y,S),\ \mathit{onNode}(X,N,S),\ N<2\\ \mathit{affected}(X,S)&\leftarrow&\mathit{move}(X,Y,S)\\ \mathit{affected}(Y,S)&\leftarrow&\mathit{move}(X,Y,S)\\ \mathit{onNode}(X,N-2,S)&\leftarrow&\mathit{onNode}(X,N,S-1),\mathit{move}(X,Y,S)\\ \mathit{onNode}(Y,M+1,S)&\leftarrow&\mathit{onNode}(Y,M,S-1),\mathit{move}(X,Y,S)\\ \mathit{onNode}(X,N,S)&\leftarrow&\mathit{onNode}(X,N,S-1),\textit{not}\ \mathit{affected}(X,S)\\ \end{array}\right\}

The first set of facts (line 1) encodes all integers $i$ that can serve as the number of pebbling moves. Since each pebbling move removes one pebble, any successful sequence of pebbling moves has length at most $k-1$. Consequently, we may (and do) restrict these integers to $0,1,\ldots,k-1$. The first rule of $P_{2}$ (line 2) selects a single integer to represent the number of pebbling moves. The second rule of $P_{2}$ (the next line) defines the initial state of the graph (before any pebbling moves). It is given by the initial distribution of pebbles obtained from an answer set of the program $P_{1}$ (we overload the notation here; the predicate $\mathit{onNode}$ defining the intial configuration in $P_{1}$ is binary, while the predicate $\mathit{onNode}$ defined in $P_{2}$ is ternary; it has an additional argument to represent the step). The third rule selects an edge for the pebbling move step $S=1,2,\ldots,T$, where $T$ is the end step (defined via $\mathit{endstep}$). The constraint that follows imposes the pebbling move precondition: there must be at least two pebbles on the node where the pebbling move originates. The next two rules define the two nodes affected by the move. The last three rules define the state of the graph after the pebbling move in step $S$ (applied to the graph after $S-1$ pebbling moves). The first two of these three rules describe how the number of pebbles change on the nodes that are involved in the move. The last rule is the inertia rule that keeps the number of pebbles unchanged on all nodes unaffected by the move. Informally, answer sets of $P_{2}$ correspond to all valid sequences of pebbling moves that do not eliminate all pebbles and start in the initial state of the graph, together with the corresponding sequence of states of the graph.

Finally, the program $C$ in $\Pi$ is defined as follows.

C=\left\{\begin{array}[]{rcl}ok(W)&\leftarrow&onNode(W,N,S),\ target(W),\mathit{endstep}(T)\ N>0\\ &\leftarrow&target(W),\ not\ ok(W)\end{array}\right\}

First rule defines $ok(W)$ to hold whenever $W$ is a target node and there is a pebble on it after the last pebbling move $T$. The constraint ensures no answer set if $ok(W)$ has not been inferred.

Intuitively then, $\Pi$ is coherent precisely when for each assignment of $k$ pebbles to nodes of a given graph and for every choice of a target node (that is, for every answer set $M_{1}$ of $P_{1}$) there is a sequence of pebbling moves of length at most $k-1$ (that is, there is an answer set $M_{2}$ for $P_{2}\cup fix_{P_{1}}(M_{1})=P_{1}^{\prime}$) such that the target node has a pebble on it (that is, $C\cup fix_{P_{1}^{\prime}}(M_{2})$ has an answer set).

Theorem 4.11**.**

Let $\mathcal{I}=\langle G,k\rangle$ be an instance of the Pebbling Number Problem. Then, $\pi(G)\leq k$ if and only if the ASP(Q) program $\Pi$, defined as above, is coherent.

4.3 Vapnik-Chervonenkis Dimension

The Vapnik-Chervonenkis dimension (VC dimension) is a fundamental concept in machine learning theory [Vapnik and Chervonenkis (2015)]. The VC dimension is a measure of the capacity of a space of functions that can be learned by a statistical classification algorithm [Blumer et al. (1989)]. In particular, it is the cardinality of the largest set of points that the algorithm can shatter. In statistical learning theory, the VC dimension can predict probabilistic upper bounds on the test error of a classification model [Vapnik (1998)]. Further applications include finite automata, complexity theory, computability theory, and computational geometry.

Here, we focus on the so-called discrete VC dimension problem, where the considered universe is finite. The problem concerns families of subsets that are represented by Boolean circuits. However, we assume that the representation is given by a logic program capturing the corresponding formula. Specifically, we assume that a program $P_{\mathcal{C}}$ representing a family $\mathcal{C}$ of subsets of $U$ contains a unary predicate $true$, and that extensions of the predicate $true$ in answer sets of $P_{\mathcal{C}}$ are precisely the elements of $\mathcal{C}$. Constructing a program $P_{\mathcal{C}}$ from a Boolean circuit representing $\mathcal{C}$ is a matter of routine and can be accomplished in linear time. Let $k$ be an integer, $U$ a finite set, and $\mathcal{C}=\{S_{1},\ldots,S_{n}\}\subseteq 2^{U}$ a collection of subsets of $U$ represented by a program $P_{\mathcal{C}}$. The VC Dimension problem asks whether there is a subset $X$ of $U$ of size at least $k$, such that for each subset $S$ of $X$, there exists $S_{i}$ such that $S=S_{i}\cap X$. The VC dimension of $\mathcal{C}$ is defined as maximum size of such a set $X$ and is denoted by $VC(\mathcal{C})$. Hence, the VC Dimension problem asks whether $VC(\mathcal{C})\geq k$. It is known that this problem (assuming a circuit or a program representation of $\mathcal{C}$) is $\Sigma_{3}^{p}$-complete [Schaefer (1999)]. We will show that the problem can be described by an ASP(Q) program $\Pi=\exists^{st}P_{1}\forall^{st}P_{2}\exists^{st}P_{3}:C$. The ASP program $P_{1}$ is defined as follows:

P_{1}=\left\{\begin{array}[]{rcll}inU(x)&&\forall x\in U\\ k\{inX(X):inU(X)\}&&\end{array}\right\}

The set of facts in line 1 encodes the elements of the set $U$, while the choice rule in line 2 selects a subset $X$ of $U$ with at least $k$ elements. It is clear that answer sets of $P_{1}$ are all subsetes of $U$ with at least $k$ elements.

The ASP program $P_{2}$ consists of a single choice rule:

P_{2}=\left\{\begin{array}[]{c}\{inS(X):inX(X)\}\end{array}\right\}

Thus, answer sets of $P_{2}$ are subsets of a set $X$ (determined by a selected answer set of $P_{1}$).

For $P_{3}$ we simply take $P_{\mathcal{C}}$. Wlog, we may assume that $P_{\mathcal{C}}$ shares no vocabulary elements with $P_{1}$ and $P_{2}$. Thus, for every possible “input” from $P_{1}$ and $P_{2}$, answer sets of $P_{3}^{\prime}$, that is, $P_{3}$ extended with the input from $P_{1}$ and $P_{2}$, determine elements of $\mathcal{C}$ via extensions of the predicate $true$.

Finally, the program $C$ is defined as follows (understanding $true$ as defined above):

C=\left\{\begin{array}[]{rcl}inIntersection(X)&\leftarrow&true(X),\ inX(X)\\ &\leftarrow&inIntersection(X),\ not\ inS(X)\\ &\leftarrow&not\ inIntersection(X),\ inS(X)\\ \end{array}\right\}

The first rule collects into predicate $inIntersection$, the intersection of the selected set $S_{i}$ from $\mathcal{C}$ (represented by an answer set of $P^{\prime}_{3}$ by means of the predicate $true$) and $X$, a subset of $U$ selected via an answer set of $P_{1}$. The two constraints force this intersection to coincide with the subset $S$ of $X$ (an answer set of $P_{2}$ extended with a selected answer set of $P_{1}$ as input representing $X$).

Intuitively, the program $\Pi$ is coherent when there exists an answer set $M_{1}$ of $P_{1}$ (that is, a subset $X$ of $U$ of size at least $k$) such that for each answer set $M_{2}$ of $P_{2}^{\prime}=P_{2}\cup fix_{P_{1}}(M_{1})$ (that is, for each subset $S$ of $X$), there exists an answer set $M_{3}$ of $P_{3}^{\prime}=P_{3}\cup fix_{P_{2}^{\prime}}(M_{2})$ (that is, an element $S_{i}$ of $\mathcal{C}$), such that $C\cup fix_{P_{3}^{\prime}}(M_{3})$ is coherent (that is, $S_{i}\cap X$ is equal to $S$).

Theorem 4.12**.**

Let $\mathcal{I}=\langle U,\mathcal{C},k\rangle$ be an instance of the VC dimension problem. Then, $VC(\mathcal{C})\geq k$ if and only if the ASP(Q) program $\Pi$ defined as above has a quantified answer set.

5 Related Work and Discussion

We now compare ASP(Q) with related work discussing pros and cons of the various approaches.

ASP(Q) vs QBF.

We first compare our proposal with Quantified Boolean Formulas (QBF) [Biere et al. (2009)]. QBF is a natural extension of propositional formulas with quantifiers $\exists$ (existential) and $\forall$ (universal) operating on propositional variables. QFB was motivated by questions arising from computational complexity [Stockmeyer and Meyer (1973)]. The problem of checking the satisfiability of a propositional formula (SAT) is the canonical problem for the complexity class NP. The addition of quantifiers increases the complexity of satisfiability problem (QSAT) to PSPACE [Stockmeyer (1976)], and prefixes of $k$ alternating quantifiers yield problems that are complete for each complexity class of the Polynomial Hierarchy. For this reason the satisfiability problem of QBF formulas with prefixes of alternating $k$ quantifiers ($k$-$QSAT$ becomes the canonical problem for the $k$-th level of the Polynomial Hierarchy). More precisely, $k$-$QSAT$ restricted to prefixes of length $k$ starting with an existential (resp. universal) quantifier is complete for $\Sigma_{k}^{P}$ (resp. $\Pi_{k}^{P}$). ASP(Q) and QBF share the same motivation and intuition, indeed ASP(Q) extends ASP with quantifiers (as QBF extends SAT) to increase the modeling capabilities of the language beyond NP. As studied in Section 3, propositional ASP(Q) and QBF have similar computational properties. In particular, the coherence problem for both is PSPACE-complete and an even tighter correspondence holds between propositional normal ASP(Q) and QSAT. Nonetheless, there are important differences among the two languages, some inherited form the relation between SAT and ASP, and other concerning the semantics of quantifiers.

First, ASP(Q) supports variables, which gives a modeling advantage, and supports rapid prototyping, program optimization and maintenance of problem solution. Indeed, variables allow one to encode uniform compact representation of a problem over varying instances, while in QBF (as in SAT) each instance of a problem needs to be encoded in a specific formula by means of an encoding procedure. Second, even if in general QBF and ASP(Q) can solve the same computational problems, ASP(Q) inherits from ASP the possibility of encoding inductive definitions [Denecker and Vennekens (2014)], which are useful in modeling properties such as reachability in graphs (inductive definitions require larger instances in SAT and QBF that slow down modeling and solving). Next, ASP supports modeling extensions such as aggregates, choice rules, strong negation, and disjunction in rule heads that significantly simplify encodings used in SAT [Brewka et al. (2011)]. We have made extensive use of inductive definitions and aggregates in our examples in Section 4. Finally, we note that in QBF quantifiers range over variable assignments, whereas in ASP(Q) they quantify over the answer sets of each subprogram. This is yet another difference and a reason that ASP(Q) cannot be seen as a straightforward porting of the ideas behind QBF.

ASP(Q) vs ASP.

One of the distinguishing features of ASP is the capability of modeling problems in $\Sigma_{2}^{P}$. This is possible because of the additional expressive power provided by disjunctive rules. Modeling in $\Sigma_{2}^{P}$ problems with ASP is rather natural if one can use only positive rules. For example, let us consider the strategic companies problem [Cadoli et al. (1997)]. In that problem, one has to compute a set of companies that cover the production of a set of goods also controlling other companies. A set of companies $S$ is said to be strategic if it: ($i$) covers the productions of all goods; ($ii$) is subset-minimal; and, ($iii$) every company $c$ controlled by at most three strategic companies is also strategic. In the setting in which each product is produced by at most two companies the problem is $\Sigma_{2}^{P}$-complete and can be modeled as follows [Leone et al. (2006)]:

\begin{array}[]{rcl}strat(Y)\vee strat(X)&\leftarrow&prod\_by(P,X,Y)\\ strat(W)&\leftarrow&contr\_by(W,X,Y,Z),strat(X),strat(Y),strat(Z)\\ \end{array}

The first rule models condition $(i)$, the second rule models condition ($iii$), and the minimality of answer sets ensures ($ii$). It is clear that this encoding of the problem can be directly translated to a single-quantifier disjunctive ASP(Q).

When problem constraints to be modeled involve negation, ASP modeling becomes less intuitive. In particular one has to resort to an encoding technique called saturation [Eiter and Gottlob (1995)]. It allows one to simulate a co-NP check in the program reduct. Saturation is at the basis of the celebrated encoding of 2-QBF by Eiter and Gottlob 1995 used to prove the complexity of checking existence of answer sets in presence of disjunction in rule heads. Given a 2-QBF formula $\Phi=\exists X\forall YG$, where $G=D_{1}\lor\ldots\lor D_{h}$ is a DNF, and $D_{i}=L_{i,1}\land\ldots\land L_{i,k_{i}}$ and $L_{i,j}$ are literals over $X\cup Y$, we encode $\Phi$ in an ASP program as follows. First introduce a fresh atom $sat$ modeling satisfiability, and a fresh atom $nz$ for every atom $z\in X\cup Y$; and set $\sigma(z)=z$ and $\sigma(\neg z)=nz$ for every $z\in X\cup Y$. Then write the program P_{\Phi}=\{z\vee nz|\forall z\in X\cup Y\}\cup\{y\leftarrow sat|\forall y\in Y\}$$\cup\{ny\leftarrow sat|\forall y\in Y\}\cup\{sat\leftarrow\sigma(L_{i,1}),\ldots,\sigma(L_{i,k_{i}})|i=1,\ldots,m\}\cup\{sat\leftarrow not\ sat\}.

Here the atoms corresponding to universally quantified variables $Y$ are “saturated” (i.e., they are forced to be true in any answer set), and since the last rule is always removed while computing the reduct, $sat$ must be derived for all assignments of truth values to $Y$ to have an answer set. This trick ensures that $\Phi$ is satisfiable if and only if $P_{\Phi}$ has an answers set. Again, one could reformulate the program above into a disjunctive program with a single quantifier. However, using saturation in modeling is considered difficult. ASP(Q) offers an alternative and more intuitive approach, It uses normal quantified programs with two quantifiers that also capture $\Sigma_{2}^{P}$ (see Theorem 3.5). Indeed, let us consider a normal quantified program $\Pi_{\Phi}=\exists^{st}P_{1}\forall^{st}P_{2}:C$ where

[TABLE]

[TABLE]

Here, a satisfiability of an existential 2-QBF is encoded directly. Indeed $P_{1}$ guesses an assignment to $X$ s.t. for all assignments to $Y$ generated by $P_{2}$, $sat$ must be derived by satisfying at least one conjunct in $\varphi$, i.e., $\Pi_{\Phi}$ is satisfiable iff $\Phi$ is. This discussion suggests that ASP(Q) improves on ASP modeling capabilities. It keeps the advantages of ASP in modeling concisely $\Sigma_{2}^{P}$ problems with positive programs, as for strategic companies, but also allows us to model other problems without resorting to difficult to use encoding techniques.

ASP(Q) vs Stable-Unstable.

To handle problems beyond NP, Bogaerts et al. 2016 proposed an extension of ASP inspired by an internal working principle of ASP solvers Gebser et al. (2018). Usually, in ASP solvers designed for problems in $\Sigma_{2}^{P}$ one procedure generates model candidates and another one, acting as an oracle, tests minimality of the candidates produced by the first procedure. It does so by verifying that a certain subprogram (in some cases, a SAT formula) has no stable models (is not satisfiable). Following this principle, Bogaerts et al. 2018 introduced combined logic programs, in which two normal logic programs play a role analogous to the one of the two procedures of ASP solvers mentioned above. A combined logic program is a pair $\Pi=(P_{g},P_{t})$ of normal logic programs. Its semantics is given by parameterized stable models Oikarinen and Janhunen (2006); Denecker et al. (2012); a stable-unstable model of a combined program $\Pi$ is a parameterized stable model of $P_{g}$, say $I$, such that no parameterized stable model of $P_{t}$ exists that coincides with $I$ in the intersection of the signatures of the two programs.

Comparing ASP(Q) programs with combined programs, we first note that combined programs involve the concept of parameters. In applications, the parameters of the generator program are used to represent problem instances (are “extensional”). This use of parameters is quite natural to ASP programmers and does not pose a conceptual difficulty. It is also used implicitly in ASP(Q) (stable models from each quantifier are passed on as “input” parameters to the next one).333We could also distinguish extensional predicates to specify “parameters,” that is, input instances, That would allow us to keep instance specification separate from the program. We decided not to do so here to simplify our presentation. However, the stable-unstable approach applies the notion of a parameterized stable model also in the checking phase using “negation,” that is, referring to non-existence of a certain parameterized stable model. This, arguably, makes the formalism much less direct than ASP(Q). It is especially clear when we move beyond the second level of the PH and the non-existence conditions become nested (incidentally, the stable-unstable paper contains no examples of modeling such problems).

If we factor out the issue of parameters, and limit ourselves to problems in $\Sigma_{2}^{P}$, combined programs and ASP(Q) are closely related. Indeed, in ASP(Q) one has direct means to model “testing” conditions of the form “for all stable models (answer sets) of some program, a certain property holds.” In contrast, combined programs provide direct means to model “testing” conditions of the form “there exists no stable model of some program such that a certain property holds.” Switching between ASP(Q) and combined programs amounts then to simulating conditions of one form with conditions of the other and vice versa (effectively, negating constraints in a program). Such simulations are easy to design with the use of a small number of auxiliary variables (often one such new variable suffices). Consequently, both formalisms are on par for modeling problems that are complete for $\Sigma_{2}^{P}$. However, for problem in $\Pi_{2}^{P}$, the difference between ASP(Q) and combined programs becomes evident. As an example, let us consider a 2-QBF formula $\Psi=\forall X\exists Y\psi$, where $\psi$ is a 3-CNF formula. This problem can be naturally represented in ASP(Q) by using the encoding employed in the proof of Theorem 3.3. However once we try to encode it using a combined logic program (for well-known complexity reasons) we have either to adopt an exponential encoding, something analogous to quantifier expansion in QBF, or we have to use an additional nesting of programs (i.e., we are have to push the entire computation in the oracle). In both cases, the modeling would not result in a solution as natural and direct as the one provided by ASP(Q). The reason is that combined programs (as well as their generalizations beyond the second level) represent existential statements. Hence, they model complements of $\Pi_{2}^{P}$ problems and not the problems themselves. In contrast, ASP(Q) can be used for such problems in a direct way providing representations closely following original problem descriptions (our examples illustrate this).

A related aspect concerns modeling itself, the process of mapping natural language specifications to formal expressions, which surfaces when one considers problems that require more than one quantifier alternation. It is important to note that combined logic programs were extended to deal with problems from any level of the PH in Bogaerts et al. (2016) by resorting to a recursive definition. This definition forces the programmer to think in terms of “nested oracles”, instead of translating problem description directly into a formal expression. Whereas for problems at the second level of the polynomial hierarchy it roughly corresponds to searching for a counterexample, for problems at higher levels, the recursion and the negation (needed because of the absence of direct means to represent universal statements), makes it harder to maintain the connection between problem description and oracles forming nested combined programs. In contrast, the interface between natural language problem description and ASP(Q) programs is transparent (in the same way as it is for QBF), as it is explicitly supported by the quantifiers, which may be existential or universal, as needed. In particular, the difficulty of modeling problems in $\Pi_{2}^{P}$, noted above, appears in the general setting of problems in $\Pi_{k}^{P}$, for $k\geq 2$: the stable-unstable formalism is not designed to directly express universal statements that characterize problems in $\Pi_{k}^{P}$.

The discussion above compares at an intutive informal level the modeling freatures of the two formalisms. It also suggests how the two are formally related. In the statement specifying the relation, the depth of the basic combined program is defined as 2. Each next level of nesting increments the depth by 1.

Theorem 5.13**.**

*(i) There is a polynomial-time reduction that assignes to every propositional nested combined program $\Pi$ of depth $n$, a normal existential ASP(Q) program $\Pi_{q}$ with $n\geq 2$ quantifiers such that answer sets of $\Pi$ and $\Pi_{q}$, correspond to each other.

(ii) There is a polynomial-time reduction that assignes to every propositional normal existential ASP(Q) program $\Pi$ with $n\geq 2$ quantifiers in the prefix, a propositional nested combined program $\Pi_{c}$ of depth $n$ such that answer sets of $\Pi$ and $\Pi_{c}$ correspond to each other.*

Thus, at the level of expressive power, combined programs of depth $n$ and existential $ASP(Q)$ programs with $n$ quantifiers are formally equivalent, even if from the modeling point of view, as we argued, ASP(Q) programs seem to have an advantage. However, unless the polynomial hierarchy collapses, no reduction from universal $ASP(Q)$ programs with $n$ quantifiers to combined nested programs of depth $n$ is possible. The following proposition specifies this property for the particular case of the validity of 2-QBFs, which we discussed above.

Proposition 5.14**.**

Unless the polynomial hierarchy collapses, there exists no polynomial reduction that encodes formulas $\Psi=\forall X\exists Y\psi$, where $\psi$ is a 3-CNF formula, as a combined program $P=(P_{1},P_{2})$, where $P_{1}$ and $P_{2}$ are normal logic programs, such that $\Psi$ is valid iff $P$ admits stable unstable models.

A trivial consequence of Theorem 3.3 is that this limitation is absent from ASP(Q).

Finally, we note that combined programs under stable-unstable semantics have been implemented in a proof of concept prototype Bogaerts et al. (2016) that can only handle problems at the second level of the polynomial hierarchy. A similar prototype implementation for ASP(Q) (programs with at most two quantifiers) is possible, too. However, devising efficient implementations for either formalism in their full generality remains a non-trivial open research problem.

Further related work.

The problem of modeling in a natural way $\Sigma_{2}^{P}$ problems with ASP was also addressed by Eiter and Polleres 2006. They model problems combining “guess” program $P_{solve}$ and “check” program $P_{check}$, which are transformed into a single disjunctive ASP program such that its answer sets encode the solutions of the original problem by means of a polynomial-time transformation. The programs $P_{solve}$ and $P_{check}$ must be HCF and propositional, thus limiting this approach to the modeling capabilities of propositional ASP. An idea analogous to that developed by Eiter and Polleres 2006 was also proposed by Redl 2017. Redl’s proposal appears to be conceptually simpler than the earlier one because of the use of conditional literals but suffers from the same limitations. A general technique to reuse existing ASP systems to evaluate problems of higher complexity (such as various forms of qualitative preferences among answer sets) was proposed by Gebser et al. 2011. The idea there was to use a meta program encoding the saturation technique which, in this way, became transparent to the user. As in the approach by Eiter and Polleres 2006, the resulting program is a plain ASP program which can be evaluated by a standard ASP system. Thus, the approach of Gebser et al. 2011 cannot be used to model problems beyond the second level of the polynomial hierarchy. Another solution that allows for reasoning within a program over the answer sets of another program, and thus encode reasoning tasks beyond NP, is provided by manifold programs Faber and Woltran (2011, 2009). In manifold programs the calling and the called program are encoded into a single program using weak constrains. The answer sets of the called program are thus represented within each answer set of the calling program. Also this approach is limited to the second level of the polynomial hierarchy, and might generate large specifications.

HEX-programs are an extension of ASP with external sources such as description logic ontologies and Web resources Eiter et al. (2008). In HEX-programs external atoms can exchange information from the logic program to eternal theories in terms of predicate extensions and constants.

Redl 2017 studied a way to avoid saturation for modeling $\Sigma_{2}^{P}$ problems with HEX-programs. In particular, the author proposes the modeling technique of query answering over subprograms. While encoding a problem on the second level of the polynomial hierarchy, one has to provide two components. A first program $P_{guess}$ modeling the NP part, and a second one $P_{check}$ modeling the co-NP check. The first program, $P_{guess}$, is a HEX program that can query on the answer sets of the normal ordinary ASP program $P_{check}$ using specific external atoms. This modeling approach avoids saturation without introducing quantifiers, but this nice modeling behavior is limited to $\Sigma_{2}^{P}$ problems. Indeed, the focus of query answering over subprograms is on overcoming saturation and not on reaching high expressibility Redl (2017). A recent proposal of an extension of propositional ASP to model planning problems was described in Romero et al. (2017). The main difference with ASP(Q) is on the nature of quantifiers allowed in the two specifications. Indeed, the proposal of  Romero et al. (2017), mimicking 2QBF, allows quantifiers over propositional atoms, whereas in ASP(Q) quantifiers are over answer sets.

As a final mention, we observe that the idea of extending the base language with quantifiers has been applied also in the neighboring area of Constraint Satisfaction Problems (CSP) Rossi et al. (2006), obtaining Quantified CSP (QCSP) Bordeaux and Monfroy (2002).

6 Conclusions

In this paper we approached the modeling of problems beyond NP with ASP programs. Inspired by the way QBFs extend SAT formulas, we have introduced ASP(Q), which extends ASP via quantifiers over stable models of programs. We have studied the computational properties of the language, provided a number of examples to demonstrate its modeling capabilities, and compared alternative approaches to the same problem. The analysis provided in the paper suggests that ASP(Q) is able to model uniformly problems in the Polynomial Hierarchy in the same compact and elegant way as ASP models problems in NP.

The definition of ASP(Q) allows for disjunctive programs, thus all the features of the basic language are retained. However, by limiting to normal (or HCF) programs (extended with aggregates and other useful modeling constructs) in ASP(Q), one can take advantage of the classic generate-define-test modular programming methodology and other modeling techniques developed for these best understood classes of programs to model any problem in the Polynomial Hierarchy. Indeed, the presence of quantifiers allows one to model complex properties in a direct way, without the need of recasting them in terms of checking the minimality of a model, e.g., using saturation. The examples provided in the paper, indeed, employ normal programs, and the solutions follow directly from the definition in natural language of the problem at hand.

The key task for the future is to implement ASP(Q). In this respect many possible solutions are possible, from encoding ASP(Q) in QBF and resorting to QBF solvers, to evolving ASP solvers to handle quantifiers over stable models.

Acknowledgements

The work of the third author has been partially supported by the NSF grant IIS-1707371. This work has been partially supported by MIUR under PRIN 2017 project n. $2017M9C25L\_001$ (CUP $H24I17000080001$).