=Paper=
{{Paper
|id=Vol-2271/invited2
|storemode=property
|title=Towards Quantified Answer Set Programming
|pdfUrl=https://ceur-ws.org/Vol-2271/invited2.pdf
|volume=Vol-2271
|authors=Giovanni Amendola
|dblpUrl=https://dblp.org/rec/conf/rcra/Amendola18
}}
==Towards Quantified Answer Set Programming==
https://ceur-ws.org/Vol-2271/invited2.pdf
Towards Quantified Answer Set Programming
Giovanni Amendola
Department of Mathematics and Computer Science, University of Calabria, Italy
amendola@mat.unical.it
Abstract. This paper proposes an extension of Answer Set Programming (ASP)
with quantifiers called Quantified ASP (QASP). This proposal is somehow in-
spired to the extension of SAT formulas in Quantified Boolean Formulas (QBF).
The resulting language is more expressive than plain ASP (which remains a sub-
class of QASP), and allows modeling problems belonging to any level of the
polynomial hierarchy.
Keywords: Logic Programming · Answer Set Programming · Quantified Boolean
Formulas.
1 Introduction
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 [34, 30]. The ability to nest universal and existential quantifi-
cation makes QBF very expressive (any problem in the polynomial hierarchy can be
encoded in QBF), and strictly more expressive than SAT which is bounded to NP com-
plete problems. Solving QBF formulas has become an attractive and important research
area over the last years. Indeed, many important artificial intelligence (AI) problems,
such as planning, non monotonic reasoning, scheduling, model checking and verifica-
tion formal verification, can be reduced to QBF [20, 41, 37]. So that, several solvers for
QBF formulas have been proposed [31, 9, 42, 36].
Answer Set Programming (ASP) [18, 23, 16] is a well-established formalism for
nonmonotonic reasoning, and combines a comparatively high knowledge-modeling power
[18, 2] with a robust solving technology [19, 24–27, 35, 9, 13–15, 40, 39], that can also
be responsive in case of incoherent logic programs [3, 11, 10, 6, 7]. For these reasons
ASP has become an established logic-based programming paradigm with successful ap-
plications to complex problems in Artificial Intelligence [33, 32, 8, 5, 4], Databases [38],
Game Theory [12], Information Extraction [1], and many other fields of knowledge.
ASP is very related to SAT [29]. Indeed, non-disjunctive ASP can model in a natural
declarative way NP-hard combinatorial problems by encoding them as a logic program
and computing its answer sets, which encode the problem solutions. Once disjunctive
rules are admitted in an ASP programs, ASP can be used to model (often in a rather
difficult and unnatural way) problems belonging to the second level of the polynomial
hierarchy at most [21, 22].
Inspired by the way SAT is extended in QBF, in this paper we propose an exten-
sion of ASP with quantifiers that is called QASP (Quantified ASP). The ability to nest
2 G. Amendola
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 Preliminaries
We start with recalling syntax and semantics of answer set programming. We concen-
trate on logic programs over a propositional signature Σ . 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 Σ ); l, m, n ≥ 0, and l + m + n > 0; not repre-
sents negation-as-failure. The set H(r) = {a1 , ..., al } is the head of r, while B+ (r) =
{b1 , ..., bm } and B− (r) = {c1 , . . . , cn } 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 |H(r)| ≤ 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 ∈ P is normal [resp. positive]. We set At(P) = r∈P At(r), that is the set of all
S
atoms occurring in the program P.
Any subset I of Σ is an interpretation. An interpretation I is a model of a program
P (denoted I |= P) if and only if for each rule r ∈ P, I ∩ H(r) 6= 0/ if B+ (r) ⊆ I and
B− (r) ∩ I = 0/ (denoted I |= r). A model M of P is minimal, if and only if there is no
model M 0 of P such that M 0 ⊂ 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 [28]
of P with respect to I, i.e., the set of rules a1 ∨ ... ∨ al ← b1 , ..., bm , obtained from rules
r ∈ P of form (1), such that B− (r) ∩ I = 0. / An interpretation I is an answer set of P if
I ∈ MM(PI ). We denote by AS(P) the set of all answer sets (called also stable models)
of P.
Example 1. Consider the following logic program
P = {a ← not b; b ← c, not d; c ← a; d ← not b}.
For instance, a model of P is {b, d}. Moreover, the set of all minimal models of P is
given by MM(P) = {{b}, {a, c, d}}. Now, let I = {a, c, d}. The Gelfond-Lifschitz reduct
of P with respect to I is PI = {a; c ← a; d}. Thus, {a, c, d} is a minimal model of PI .
Hence, it is an answer set of P. On the other hand, {b} is not an answer set of P. Indeed,
P{b} = {b ← c; c ← a}, but {b} is not a minimal model of P{b} (as MM(P{b} ) = {0}). /
3 Quantified Answer Set Programming
In this section, we introduce the syntax and the semantics of Quantified Answer Set Pro-
gramming (QASP). Intuitively, we consider a partition of the atoms of a logic program,
identifying different levels and quantifications (existential or universal) for each atom.
Towards Quantified Answer Set Programming 3
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 = {e1 , . . . , en } and a set of universal
atoms U = {u1 , . . . , um }, is a structure of the form:
Q1V1 . . . QkVk P
where P is a logic program such that At(P) = E ∪ U; Qi ∈ {∃, ∀}, for i = 1, . . . , k;
Vi ⊆ E if Qi = ∃, and Vi ⊆ U if Qi = ∀, for each i = 1, . . . , k; and for each i 6= j ∈
{1, . . . , k}, Vi ∩V j = 0, / and ki=1 Vi = E ∪U. In the following, without loss of generality,
S
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 = ∀ and Vk = ∃.
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 ∀U1 ∃E1 . . . ∀Uh ∃Eh P, where U1 , . . . ,Uh ⊆
U and E1 , . . . , Eh ⊆ E. We say that QP is a normal QASP program if P is normal.
Let E 0 ⊆ E, U 0 ⊆ U, and let I be a set of atoms. If I ⊆ E 0 , then I is called partial
existential interpretation w.r.t. E 0 , and if I ⊆ U 0 , then I is called partial universal inter-
pretation 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 ∈ 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 inter-
pretation 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 2|U1 | 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 2|Ui+1 | edges (n, n0 )
such that n0 = (I 0 , J 0 ) is a node at level i + 1, where I 0 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.
Example 2. Consider the following QASP program:
QP = ∀U1 ∃E1 ∀U2 ∃E2 P,
over E = {e1 , e2 , e3 } and U = {u1 , u2 }, where U1 = 0, / E1 = {e1 , e2 }, U2 = {u1 , u2 },
E2 = {e3 , e4 }, and
e3 ∨ u1 ∨ u2 ← e1 ;
e1 ← not u1 ; e1 ← not e3 ;
P= .
e4 ← u1 , not u2 ; e4 ← u2 , not u1 ;
u1 ← not e3 , not e4 ; u2 ← not e3 , not e4
Then, the graph reported in Figure 1 is a total interpretation of QP, where (0, / {e1 })
is at level 1, and (0, / {e3 }), ({u1 }, {e4 }), ({u2 }, {e4 }), and ({u1 , u2 }, 0)
/ are at level 2.
Moreover, it is also a quantified answer set. Indeed, {e1 , e3 } is a minimal model of
P{e1 ,e3 } = {e3 ∨ u1 ∨ u2 ← e1 ; e1 ; e4 ← u1 ; e4 ← u2 }; {e1 , u1 , e4 } is a minimal model
of P{e1 ,u1 ,e4 } = {e3 ∨ u1 ∨ u2 ← e1 ; e1 ; e4 ← u1 }; {e1 , u2 , e4 } is a minimal model of
P{e1 ,u2 ,e4 } = {e3 ∨ u1 ∨ u2 ← e1 ; e1 ; e4 ← u2 }; and {e1 , u1 , u2 } is a minimal model of
P{e1 ,u1 ,u2 } = {e3 ∨ u1 ∨ u2 ← e1 ; e1 ; u1 ; u2 }.
4 G. Amendola
/ {e1 })
(0,
/ {e3 })
(0, ({u1 }, {e4 }) ({u2 }, {e4 }) ({u1 , u2 }, 0)
/
Fig. 1: Total interpretation of the program of the Example 2.
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 = ∀U∃EP, where U = 0/ and E =
At(P). Then, M ∈ AS(P) if, and only if, (0,
/ M) ∈ 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 Modeling Quantified Boolean Formulas in QASP
Let X = {x1 , . . . , xk } and Y = {y1 , . . . , yn } be two sets of variables. A Quantified Boolean
Formula (QBF) is of the form Φ = ∃X∀Yφ (X,Y ), where φ (X,Y ) is a disjunction of m
clauses over variables in X and Y, i.e., φ (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 ∈ X ∪ {¬x | x ∈ X} ∪ Y ∪ {¬y | y ∈ Y}.
We can model the QBF formula Φ by the QASP program QPΦ = ∀U1 ∃E1 ∀U2 ∃E2 P,
where U1 = 0, / E1 = X, U2 = Y, E2 = {g, nx1 , . . . , nxk , ny1 , . . . , nyn }, and P is the set of
the following rules
x ∨ nx for each x ∈ X;
y ∨ ny for each y ∈ Y;
g ← σ (l1 j ) ∧ σ (l2 j ) ∧ σ (l3 j ) for each j = 1, . . . , m;
g ← not g
where σ (lk j ) is equal to lk j , if lk j ∈ X ∪ Y, is equal to nx, if lk j = ¬x for some x ∈ X,
and is equal to ny, if lk j = ¬y for some y ∈ Y.
Theorem 3. Let Φ be a QBF formula. Then, Φ is valid if, and only if, QAS(QPΦ ) 6= 0.
/
Proof. Let Φ be a valid QBF formula. Then, there is a truth assignment π of the
variables in X such that for each truth assignment µ of the variables in Y, at least
Towards Quantified Answer Set Programming 5
one clause, say C j , is satisfied. Let M = π(X) ∪ µ(Y) be the model satisfying C j .
Hence, σ (l1 j ) ∧ σ (l2 j ) ∧ σ (l3 j ) is satisfied by σ (M) = {σ (l) | l ∈ M}. Therefore, M 0 =
0
σ (M) ∪ {g} is a minimal model of PM . Thus, there exists a subset J1 of E1 , namely
J1 = π(X) ∩ X, such that for each subset I2 of U2 , namely I2 = µ(Y) ∩ Y, there is a
subset J2 of E2 , namely J2 = {g} ∪ σ (π(X) ∩ {¬x | x ∈ X}) ∪ σ (µ(Y) ∩ {¬y | y ∈ Y})
such that J1 ∪ I2 ∪ J2 is a minimal model of PJ1 ∪I2 ∪J2 . Therefore, QPΦ has a quantified
answer set. Now assume that QAS(QPΦ ) 6= 0. / Hence, it can be easily checked that a
quantified answer set of QPΦ satisfies Φ. Indeed, each subset of U2 corresponds to an
assignment of the universal variables of Φ, and each subset of E1 corresponds to an
assignment of the existential variables of Φ.
5 Future work
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. [17]) can be adapted
to build efficient QASP solvers.
References
1. Adrian, W.T., Manna, M., Leone, N., Amendola, G., Adrian, M.: Entity set expansion from
the web via ASP. In: ICLP (Technical Communications). OASICS, vol. 58, pp. 1:1–1:5.
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)
2. Alviano, M., Amendola, G., Peñaloza, R.: Minimal undefinedness for fuzzy answer sets. In:
AAAI 2017. pp. 3694–3700 (2017)
3. Amendola, G.: Dealing with incoherence in ASP: split semi-equilibrium semantics. In:
DWAI@AI*IA. CEUR Workshop Proceedings, vol. 1334, pp. 23–32. CEUR-WS.org (2014)
4. Amendola, G.: Preliminary results on modeling interdependent scheduling games via answer
set programming. In: RCRA@AI*IA. p. to appear. CEUR Workshop Proceedings, CEUR-
WS.org (2018)
5. Amendola, G.: Solving the stable roommates problem using incoherent answer set programs.
In: RCRA@AI*IA. p. to appear. CEUR Workshop Proceedings, CEUR-WS.org (2018)
6. Amendola, G., Dodaro, C., Faber, W., Leone, N., Ricca, F.: On the computation of para-
coherent answer sets. In: Proceedings of the Thirty-First AAAI Conference on Artificial
Intelligence, February 4-9, 2017, San Francisco, California, USA. pp. 1034–1040 (2017)
7. Amendola, G., Dodaro, C., Faber, W., Ricca, F.: Externally supported models for efficient
computation of paracoherent answer sets. In: Proceedings of the Thirty-Second AAAI Con-
ference on Artificial Intelligence, February 2-7, 2018, New Orleans, Louisiana, USA. pp.
1034–1040 (2018)
6 G. Amendola
8. Amendola, G., Dodaro, C., Leone, N., Ricca, F.: On the application of answer set program-
ming to the conference paper assignment problem. In: AI*IA. Lecture Notes in Computer
Science, vol. 10037, pp. 164–178. Springer (2016)
9. Amendola, G., Dodaro, C., Ricca, F.: ASPQ: an asp-based 2qbf solver. In: QBF@SAT.
CEUR Workshop Proceedings, vol. 1719, pp. 49–54. CEUR-WS.org (2016)
10. Amendola, G., Eiter, T., Fink, M., Leone, N., Moura, J.: Semi-equilibrium models for para-
coherent answer set programs. Artif. Intell. 234, 219–271 (2016)
11. Amendola, G., Eiter, T., Leone, N.: Modular paracoherent answer sets. In: Logics in Ar-
tificial Intelligence - 14th European Conference, JELIA2014, Funchal, Madeira, Portugal,
September 24-26, 2014. Proceedings. pp. 457–471 (2014)
12. Amendola, G., Greco, G., Leone, N., Veltri, P.: Modeling and reasoning about NTU games
via answer set programming. In: IJCAI 2016. pp. 38–45 (2016)
13. Amendola, G., Ricca, F., Truszczynski, M.: Generating hard random boolean formulas and
disjunctive logic programs. In: IJCAI. pp. 532–538. ijcai.org (2017)
14. Amendola, G., Ricca, F., Truszczynski, M.: A generator of hard 2qbf formulas and asp pro-
grams. In: KR. AAAI Press (2018)
15. Amendola, G., Ricca, F., Truszczynski, M.: Random models of very hard 2qbf and dis-
junctive programs: An overview. In: ICTCS. CEUR Workshop Proceedings, CEUR-WS.org
(2018)
16. Bonatti, P.A., Calimeri, F., Leone, N., Ricca, F.: Answer set programming. In: 25 Years
GULP. Lecture Notes in Computer Science, vol. 6125, pp. 159–182. Springer (2010)
17. Bordeaux, L., Cadoli, M., Mancini, T.: Generalizing consistency and other constraint prop-
erties to quantified constraints. ACM Trans. Comput. Log. 10(3), 17:1–17:25 (2009)
18. Brewka, G., Eiter, T., Truszczynski, M.: Answer set programming at a glance. Com. ACM
54(12), 92–103 (2011)
19. Calimeri, F., Gebser, M., Maratea, M., Ricca, F.: Design and results of the Fifth Answer Set
Programming Competition. Artif. Intell. 231, 151–181 (2016)
20. Cashmore, M., Fox, M., Giunchiglia, E.: Planning as quantified boolean formula. In: ECAI.
Frontiers in Artificial Intelligence and Applications, vol. 242, pp. 217–222. IOS Press (2012)
21. Eiter, T., Gottlob, G.: On the computational cost of disjunctive logic programming: Proposi-
tional case. Ann. Math. Artif. Intell. 15(3-4), 289–323 (1995)
22. Eiter, T., Gottlob, G., Mannila, H.: Disjunctive datalog. ACM Trans. Database Syst. 22(3),
364–418 (1997)
23. Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Answer Set Solving in Practice. Mor-
gan & Claypool Publishers (2012)
24. Gebser, M., Leone, N., Maratea, M., Perri, S., Ricca, F., Schaub, T.: Evaluation techniques
and systems for answer set programming: a survey. In: IJCAI 2018. pp. 5450–5456 (2018)
25. Gebser, M., Maratea, M., Ricca, F.: The Design of the Sixth Answer Set Programming Com-
petition. In: LPNMR. LNCS, vol. 9345, pp. 531–544. Springer (2015)
26. Gebser, M., Maratea, M., Ricca, F.: What’s hot in the answer set programming competition.
In: AAAI. pp. 4327–4329. AAAI Press (2016)
27. Gebser, M., Maratea, M., Ricca, F.: The sixth answer set programming competition. Journal
of Artificial Intelligence Research 60, 41–95 (2017)
28. Gelfond, M., Lifschitz, V.: Classical negation in logic programs and disjunctive databases.
New Generation Comput. 9(3/4), 365–386 (1991). https://doi.org/10.1007/BF03037169,
http://dx.doi.org/10.1007/BF03037169
29. Giunchiglia, E., Lierler, Y., Maratea, M.: Sat-based answer set programming. In: AAAI. pp.
61–66. AAAI Press / The MIT Press (2004)
30. Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with quantified boolean formulas. In:
Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp.
761–780. IOS Press (2009)
Towards Quantified Answer Set Programming 7
31. Giunchiglia, E., Narizzano, M., Tacchella, A.: QUBE: A system for deciding quantified
boolean formulas satisfiability. In: IJCAR. Lecture Notes in Computer Science, vol. 2083,
pp. 364–369. Springer (2001)
32. Grasso, G., Iiritano, S., Leone, N., Lio, V., Ricca, F., Scalise, F.: An asp-based system for
team-building in the gioia-tauro seaport. In: PADL. Lecture Notes in Computer Science,
vol. 5937, pp. 40–42. Springer (2010)
33. Grasso, G., Iiritano, S., Leone, N., Ricca, F.: Some DLV applications for knowledge man-
agement. In: LPNMR. Lecture Notes in Computer Science, vol. 5753, pp. 591–597. Springer
(2009)
34. Kleine Büning, H., Bubeck, U.: Theory of quantified boolean formulas. In: Handbook of
Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 735–760.
IOS Press (2009)
35. Lierler, Y., Maratea, M., Ricca, F.: Systems, engineering environments, and competitions. AI
Magazine 37(3), 45–52 (2016)
36. Lonsing, F., Egly, U.: Depqbf 6.0: A search-based QBF solver beyond traditional QCDCL.
In: CADE. Lecture Notes in Computer Science, vol. 10395, pp. 371–384. Springer (2017)
37. Mangassarian, H., Veneris, A.G., Benedetti, M.: Robust QBF encodings for sequential cir-
cuits with applications to verification, debug, and test. IEEE Trans. Computers 59(7), 981–
994 (2010)
38. Manna, M., Ricca, F., Terracina, G.: Taming primary key violations to query large inconsis-
tent data via ASP. TPLP 15(4-5), 696–710 (2015)
39. Maratea, M., Pulina, L., Ricca, F.: A multi-engine approach to answer-set programming.
TPLP 14(6), 841–868 (2014)
40. Maratea, M., Ricca, F., Faber, W., Leone, N.: Look-back techniques and heuristics in DLV:
implementation, evaluation, and comparison to QBF solvers. J. Algorithms 63(1-3), 70–89
(2008)
41. Marin, P., Narizzano, M., Pulina, L., Tacchella, A., Giunchiglia, E.: Twelve years of QBF
evaluations: QSAT is pspace-hard and it shows. Fundam. Inform. 149(1-2), 133–158 (2016)
42. Rabe, M.N., Tentrup, L.: CAQE: A certifying QBF solver. In: FMCAD. pp. 136–143. IEEE
(2015)