This paper proposes an extension of Answer Set Programming (ASP) with quantifiers called Quantified ASP (QASP). This proposal is somehow inspired to the extension of SAT formulas in Quantified Boolean Formulas (QBF). The resulting language is more expressive than plain ASP (which remains a subclass of QASP), and allows modeling problems belonging to any level of the polynomial hierarchy.
Quantified boolean formulas (QBF) are a powerful generalization of the satisfiability
problem (SAT) in which the variables are also allowed to be universally as well as
existentially quantified [
Answer Set Programming (ASP) [
ASP is very related to SAT [
Inspired by the way SAT is extended in QBF, in this paper we propose an extension of ASP with quantifiers that is called QASP (Quantified ASP). The ability to nest universal and existential quantification makes QASP strictly more expressive than ASP. Indeed, we prove in the paper that QBF can be reduced naturally to QASP, thus any problem in the polynomial hierarchy can be also encoded in QASP. QASP combines the quantifiers of QBF with the non-monotonic reasoning features of ASP. 2
We start with recalling syntax and semantics of answer set programming. We concentrate on logic programs over a propositional signature S . A disjunctive rule r is of the form a1 _ _ al b1; :::; bm; not c1; :::; not cn; (1) where all ai, b j, and ck are atoms (from S ); l; m; n 0, and l + m + n > 0; not represents negation-as-failure. The set H(r) = fa1; :::; al g is the head of r, while B+(r) = fb1; :::; bmg and B (r) = fc1; : : : ; cng are the positive body and the negative body of r, respectively; the body of r is B(r) = B+(r) [ B (r). We denote by At(r) = H(r) [ B(r) the set of all atoms occurring in r. A rule r is a fact, if B(r) = 0/ (we then omit ); a constraint, if H(r) = 0/ ; normal, if jH(r)j 1 and positive, if B (r) = 0/ . A (disjunctive logic) program P is a finite set of disjunctive rules. P is called normal [resp. positive] if each r 2 P is normal [resp. positive]. We set At(P) = Sr2P At(r), that is the set of all atoms occurring in the program P.
Any subset I of S is an interpretation. An interpretation I is a model of a program
P (denoted I j= P) if and only if for each rule r 2 P, I \ H(r) 6= 0/ if B+(r) I and
B (r) \ I = 0/ (denoted I j= r). A model M of P is minimal, if and only if there is no
model M0 of P such that M0 M. We denote by MM(P) the set of all minimal models
of P. Given an interpretation I, let PI be the well-known Gelfond-Lifschitz reduct [
P = fa not b; b c; not d; c a; d not bg: For instance, a model of P is fb; dg. Moreover, the set of all minimal models of P is given by MM(P) = ffbg; fa; c; dgg. Now, let I = fa; c; dg. The Gelfond-Lifschitz reduct of P with respect to I is PI = fa; c a; dg. Thus, fa; c; dg is a minimal model of PI . Hence, it is an answer set of P. On the other hand, fbg is not an answer set of P. Indeed, Pfbg = fb c; c ag, but fbg is not a minimal model of Pfbg (as MM(Pfbg) = f0/ g). 3
In this section, we introduce the syntax and the semantics of Quantified Answer Set Programming (QASP). Intuitively, we consider a partition of the atoms of a logic program, identifying different levels and quantifications (existential or universal) for each atom. Then, we show that QASP semantics extends the standard ASP semantics. Finally, we note that modelling capabilities of QASP programs are beyond NP for normal QASP programs.
A QASP QP over a set of existential atoms E = fe1; : : : ; eng and a set of universal atoms U = fu1; : : : ; umg, is a structure of the form:
Q1V1 : : : QkVkP where P is a logic program such that At(P) = E [ U ; Qi 2 f9; 8g, for i = 1; : : : ; k; Vi E if Qi = 9, and Vi U if Qi = 8, for each i = 1; : : : ; k; and for each i 6= j 2 f1; : : : ; kg, Vi \Vj = 0/ , and Sik=1 Vi = E [U . In the following, without loss of generality, we assume that Qi 6= Qi+1, for each i = 1; : : : ; k 1, i.e. we consider an alternation of existential and universal quantifiers, and moreover we assume that V1 = 8 and Vk = 9. Note that to obtain a QASP program starting with an existential quantifier or ending with a universal quantifier, it is enough to set V1 = 0/ or Vk = 0/ , respectively. Therefore, we will consider QASP programs of the form 8U19E1 : : : 8Uh9EhP, where U1; : : : ;Uh U and E1; : : : ; Eh E. We say that QP is a normal QASP program if P is normal.
Let E0 E, U 0 U , and let I be a set of atoms. If I E0, then I is called partial existential interpretation w.r.t. E0, and if I U 0, then I is called partial universal interpretation w.r.t. U 0. A total interpretation M of a QASP program QP is a forest (i.e., a disjoint union of trees), M = hN; Ai, where each node n 2 N is a pair n = (I; J), where I is a partial universal interpretation w.r.t. Ui U , and J is a partial existential interpretation w.r.t. Ei E, for some i = 1; : : : ; h, that is called the level of the node n. At level 1 there exist exactly 2jU1j nodes n = (I; J) such that I varies over all subsets of U1. Moreover, for each node n = (I; J) at level i < h, there exist exactly 2jUi+1j edges (n; n0) such that n0 = (I0; J0) is a node at level i + 1, where I0 varies over all subsets of Ui+1.
A total interpretation M is a quantified answer set of a QASP program QP, if each path from a node at level 1 to a node at level h, that is a sequence of h nodes, (I1; J1); : : : ; (Ih; Jh), is such that I1 [J1 [ [ Ih [Jh is a minimal model of PI1[J1[ [Ih[Jh . We denote by QAS(QP) the set of all quantified answer sets of QP.
QP = 8U19E18U29E2P, over E = fe1; e2; e3g and U = fu1; u2g, where U1 = 0/ , E1 = fe1; e2g, U2 = fu1; u2g, E2 = fe3; e4g, and
P = 8> e3 _ u1 _ u2 e1; >< e1 not u1; e1 > e4 u1; not u2; e4 >: u1 not e3; not e4; u2 9 > not e3; >=. u2; not u1; > not e3; not e4 ;> Then, the graph reported in Figure 1 is a total interpretation of QP, where (0/ ; fe1g) is at level 1, and (0/ ; fe3g), (fu1g; fe4g), (fu2g; fe4g), and (fu1; u2g; 0/ ) are at level 2. Moreover, it is also a quantified answer set. Indeed, fe1; e3g is a minimal model of Pfe1;e3g = fe3 _ u1 _ u2 e1; e1; e4 u1; e4 u2g; fe1; u1; e4g is a minimal model of Pfe1;u1;e4g = fe3 _ u1 _ u2 e1; e1; e4 u1g; fe1; u2; e4g is a minimal model of Pfe1;u2;e4g = fe3 _ u1 _ u2 e1; e1; e4 u2g; and fe1; u1; u2g is a minimal model of Pfe1;u1;u2g = fe3 _ u1 _ u2 e1; e1; u1; u2g.
( 0/; fe1g) ( 0/; fe3g) (fu1g; fe4g) (fu2g; fe4g) (fu1; u2g; 0/)
Intuitively, the notion of quantified answer set can be considered as an extension of the notion of answer set. Indeed, quantified answer sets coincides with answer sets whenever the QASP program contains existential atoms only, as stated in the following theorem.
Theorem 1. Let P be a logic program, and let QP = 8U 9EP, where U = 0/ and E = At(P). Then, M 2 AS(P) if, and only if, (0/ ; M) 2 QAS(QP).
Given the possibility of alternating universal and existential quantifiers, it is easy to see that the problem of deciding the existence of a quantified answer set such as its modelling capability are beyond NP problems.
Theorem 2. To decide the existence of a quantified answer set for a QASP program is a PSPACE-complete problem, also for normal QASP program. 4
Let X = fx1; : : : ; xkg and Y = fy1; : : : ; yng be two sets of variables. A Quantified Boolean Formula (QBF) is of the form F = 9X8Yf (X ;Y ), where f (X ;Y ) is a disjunction of m clauses over variables in X and Y, i.e., f (X; Y) = C1 _ _ Cm, and each clause C j is the conjunction of three literals, i.e. C j = l1 j ^ l2 j ^ l3 j, for j = 1; : : : ; m, such that lk j 2 X [ f:x j x 2 Xg [ Y [ f:y j y 2 Yg.
We can model the QBF formula F by the QASP program QPF = 8U19E18U29E2P, where U1 = 0/ , E1 = X, U2 = Y, E2 = fg; nx1; : : : ; nxk; ny1; : : : ; nyng, and P is the set of the following rules x _ nx y _ ny g g s (l1 j) ^ s (l2 j) ^ s (l3 j) not g for each x 2 X; for each y 2 Y; for each j = 1; : : : ; m; where s (lk j) is equal to lk j, if lk j 2 X [ Y, is equal to nx, if lk j = :x for some x 2 X, and is equal to ny, if lk j = :y for some y 2 Y.
Theorem 3. Let F be a QBF formula. Then, F is valid if, and only if, QAS(QPF ) 6= 0/ . Proof. Let F be a valid QBF formula. Then, there is a truth assignment p of the variables in X such that for each truth assignment m of the variables in Y, at least one clause, say C j, is satisfied. Let M = p(X) [ m(Y) be the model satisfying C j. Hence, s (l1 j) ^ s (l2 j) ^ s (l3 j) is satisfied by s (M) = fs (l) j l 2 Mg. Therefore, M0 = s (M) [ fgg is a minimal model of PM0 . Thus, there exists a subset J1 of E1, namely J1 = p(X) \ X, such that for each subset I2 of U2, namely I2 = m(Y) \ Y, there is a subset J2 of E2, namely J2 = fgg [ s (p(X) \ f:x j x 2 Xg) [ s (m(Y) \ f:y j y 2 Yg) such that J1 [ I2 [ J2 is a minimal model of PJ1[I2[J2 . Therefore, QPF has a quantified answer set. Now assume that QAS(QPF ) 6= 0/ . Hence, it can be easily checked that a quantified answer set of QPF satisfies F . Indeed, each subset of U2 corresponds to an assignment of the universal variables of F , and each subset of E1 corresponds to an assignment of the existential variables of F . 5
Inspired by the way SAT is extended in QBF, in this paper we propose an extension
of ASP with quantifiers that is called QASP (Quantified ASP). At the moment this is a
proposal of extension that we would like to discuss at the workshop to get feedback from
the community. Mostly it will be the basis for future work. Where we will investigate the
possibility of extending QASP problems with variables, as it is done in ASP. Moreover
we will study the expressivity of the language by applying it to a number of problems,
and we will compare it with existing formalism in this respect. In particular, we will
assess the practical modeling advantages of QASP with respect to QBF and QCSP.
Finally, the implementation of the language in a solver is also subject of future work.
In particular, we will investigate how reasoning techniques and the various structural
properties useful for solving problems in QBF and QCSP (see, e.g. [