Solving the Stable Roommates Problem using Incoherent Answer Set Programs Giovanni Amendola Department of Mathematics and Computer Science, University of Calabria, Italy amendola@mat.unical.it Abstract. Answer Set Programming (ASP) has become an established logic- based programming paradigm with successful applications. In this paper, through the study of a direct and natural modeling of the Stable Marriage Problem (SMP) via ASP, we apply the same approach to the Stable Roommates Problem (SRP). However, unlike the SMP, the modeling proposed may lead to lack of answer sets due to cyclic default negation occurring in the ASP program. Hence, the proposed modeling of the SRP can lead to a first benchmark in the ASP competions with consistent, but incoherent ASP programs. Keywords: Answer Set Programming · Paracoherent Resoning · Semi-Equilibrium Models · Stable Marriage Problem · Stable Roommates Problem. 1 Introduction Answer Set Programming (ASP) is a premier formalism for knowledge representation and non-monotonic reasoning. It is a declarative programming paradigm oriented to- wards difficult search problems. Indeed, ASP combines a comparatively high knowledge- modeling power [16, 2, 15] with a robust solving technology [17, 23–26, 33, 8, 12–14, 37, 36]. The idea of ASP is to represent a given computational problem by a logic pro- gram whose answer sets correspond to solutions, and then use a solver to find them. For these reasons ASP has become an established logic-based programming paradigm with successful applications to complex problems in several areas, such as Artificial Intelligence [29, 28, 7, 4], Bioinformatics [21], Databases [35], Game Theory [11], In- formation Extraction [1]. Recently, ASP programs have been used to encode a number of variations and gen- eralizations of the Stable Marriage Problem (SMP) [19]. The SMP requires to find a way to arrange the marriage for the men and women with respect to mutual prefer- ences [31]. Given a set of men M and a set of women W of the same size, and a set of preferences, a solution to SMP is a bijective function S from M to W such that there is no pair (m, w) ∈ M × W , where m prefers w to S(m), and w prefers m to S−1 (w). It is well-known that it is always possible to solve the SMP and make all marriages sta- ble [22]. The SMP has been addressed from an abstract argumentation perspective by Dung in its pioneering work [20]. In this paper, first we show that the modeling approach proposed by Dung can be ported to ASP, and it represents a direct and natural encoding of the SMP. The main 2 G. Amendola feature of this modeling is the absence of constraints in the logic program. Then, we consider a variation of the SMP, known as the Stable Roommates Problem (SRP). Given a set of 2n persons, each one ranks the others in strict order of preference. A solution to the SRP is a set of n disjoint pairs of persons so that there are no two persons p1 and p2 , each of whom prefers the other to their partner. As the SRP has a structure similar to the SMP, the modeling of the SMP via ASP remains a direct and natural encoding for the SRP. However, unlike the SMP, a solution to the SRP may fail to exist for certain sets of persons and their preferences, and so no answer set could exist. Since no constraint appears in the encoding, the lack of answer sets is due to the cyclic default negation. It is noteworthy to mention that in all the benchmarks appearing in the ASP competitions [26], the lack of answer sets is always due to the violation of some constraint. Hence, the proposed modeling of the SRP can lead to have a first benchmark with consistent, but incoherent ASP programs. 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 S all atoms occurring in the program P. Finally, the dependency graph of a program P is defined as follows. Its nodes are the atoms in At(P), and it contains a directed edge (a, b) if and only if there exists a rule r ∈ P such that a ∈ H(r) and b ∈ B(r). The edge is labelled positive if b ∈ B+ (r), and negative if b ∈ B(r). 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 [27] 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. Finally, we say that a program P is consistent, if it admits some model, otherwise it is inconsistent; whereas we say that it is coherent, if it admits some answer set (i.e., AS(P) 6= 0), / otherwise, it is incoherent [3, 10, 9]. Solving the SRP using Incoherent ASP Programs 3 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 Stable Marriage Problem: from Argumentation to ASP The Stable Marriage Problem (SMP) requires to find a way to arrange the marriage for the men and women with respect to mutual preferences [31]. Given a set M of n men, a set W of n women, and a set of preferences of the form m ∈ M prefers w1 ∈ W to w2 ∈ W or w ∈ W prefers m1 ∈ M to m2 ∈ M, a solution to SMP is a bijective function S from M to W such that there is no pair (m, w) ∈ M ×W , where m prefers w to S(m), and w prefers m to S−1 (w). Note that, it is implicitely assumed that M ∩W = 0. / It is well-known that it is always possible to solve the SMP and make all marriages stable [22]. The SMP has been addressed from an abstract argumentation perspective by Dung in its pioneering work [20]. An argumentation framework AF is defined as (Ar, att), where Ar is a set of arguments and att ⊆ Ar × Ar is a set of attacks. For instance, if AF = ({a, b, c}, {(a, b), (b, c)}), then argument a attacks argument b, and argument b attacks argument c. Dung introduced the so-called stable semantics for argumentation framework. A set of arguments A is a stable extension, if (1) each argument in A does not attack an argument in A; and (2) each argument outside A is attacked by some argument in A. For instance, if we consider the previous argumentation framework AF, we have that A = {a, c} is a stable extension. Indeed, (1) (a, c) and (c, a) do not belong to att; and (2) the argument b (not in A) is attacked by a ∈ A. In [20], Dung proposed a modeling of the SMP via abstract argumentation frame- work. Starting from M, W , and a set of preferences, defined as above, he constructs an argumentation framework AF = (Ar, att), where Ar = M × W , and a pair (m1 , w1 ) ∈ M ×W attacks (m2 , w2 ) ∈ M ×W if, and only if, (i) m1 = m2 and m1 prefers w1 to w2 ; or (ii) w1 = w2 and w1 prefers m1 to m2 . Then, he was able to prove that Theorem 1 (Theorem 39 in [20]). A set S ⊆ M ×W constitutes a solution to the SMP if, and only if, S is a stable extension of the corresponding argumentation framework. Example 2. Consider the following instance of the SMP: M = {m1 , m2 , m3 , m4 } and W = {w1 , w2 , w3 , w4 } with the basic prefence relations: m1 prefers w2 to w4 ; m1 prefers w4 to w1 ; m1 prefers w1 to w3 ; m2 prefers w3 to w1 ; m2 prefers w1 to w4 ; m2 prefers w4 to w2 ; m3 prefers w2 to w3 ; m3 prefers w3 to w1 ; m3 prefers w1 to w4 ; m4 prefers w4 to w1 ; m4 prefers w1 to w3 ; m4 prefers w3 to w2 ; w1 prefers m2 to m1 ; w1 prefers m1 to m4 ; w1 prefers m4 to m3 ; w2 prefers m4 to m3 ; w2 prefers m3 to m1 ; w2 prefers m1 to m2 ; 4 G. Amendola w3 prefers m1 to m4 ; w3 prefers m4 to m3 ; w3 prefers m3 to m2 ; w4 prefers m2 to m1 ; w4 prefers m1 to m4 ; w4 prefers m4 to m3 . We reported basic preference relations only. However, they imply others. For instance, from m1 prefers w2 to w4 and m1 prefers w4 to w1 , one can deduce that m1 prefers w2 to w1 . Hence, the corresponding argumentation framework is formed by Ar = M ×W and     ((m1 , w2 ), (m1 , w4 )), ((m1 , w4 ), (m1 , w1 )), ((m1 , w1 ), (m1 , w3 ))   ((m2 , w3 ), (m2 , w1 )), ((m2 , w1 ), (m2 , w4 )), ((m2 , w4 ), (m2 , w2 ))         ((m3 , w2 ), (m3 , w3 )), ((m3 , w3 ), (m3 , w1 )), ((m3 , w1 ), (m3 , w4 ))         ((m4 , w4 ), (m4 , w1 )), ((m4 , w1 ), (m4 , w3 )), ((m4 , w3 ), (m4 , w2 ))         ((m2 , w1 ), (m1 , w1 )), ((m1 , w1 ), (m4 , w1 )), ((m4 , w1 ), (m3 , w1 ))         ((m , w ), (m , w )), ((m , w ), (m , w )), ((m , w ), (m , w ))   4 2 3 2 3 2 1 2 1 2 2 2       ((m , w ), (m , w )), ((m , w ), (m , w )), ((m , w ), (m , w ))   1 3 4 3 4 3 3 3 3 3 2 3       ((m2 , w4 ), (m1 , w4 )), ((m1 , w4 ), (m4 , w4 )), ((m4 , w4 ), (m3 , w4 ))   att = .   ((m1 , w2 ), (m1 , w1 )), ((m1 , w2 ), (m1 , w3 )), ((m1 , w4 ), (m1 , w3 ))    ((m2 , w3 ), (m2 , w4 )), ((m2 , w3 ), (m2 , w2 )), ((m2 , w1 ), (m2 , w2 ))         ((m3 , w2 ), (m3 , w1 )), ((m3 , w2 ), (m3 , w4 )), ((m3 , w3 ), (m3 , w4 ))        ((m , w ), (m , w )), ((m , w ), (m , w )), ((m , w ), (m , w ))   4 4 4 3 4 4 4 2 4 1 4 2        ((m2 , w1 ), (m4 , w1 )), ((m2 , w1 ), (m3 , w1 )), ((m1 , w1 ), (m3 , w1 ))         ((m4 , w2 ), (m1 , w2 )), ((m4 , w2 ), (m2 , w2 )), ((m3 , w2 ), (m2 , w2 ))         ((m1 , w3 ), (m3 , w3 )), ((m1 , w3 ), (m2 , w3 )), ((m4 , w3 ), (m2 , w3 ))        ((m2 , w4 ), (m4 , w4 )), ((m2 , w4 ), (m3 , w4 )), ((m1 , w4 ), (m3 , w4 ))   It can be checked that there are exactly two solutions to the SMP instance: {(m1 , w4 ), (m2 , w3 ), (m3 , w2 ), (m4 , w1 )}, and {(m1 , w4 ), (m2 , w1 ), (m3 , w2 ), (m4 , w3 )}, which cor- respond to the stable extensions of the argumentation framework (Ar, att), according to the Theorem 1. Recently, relations between abstract argumentation semantics and logic program- ming semantics has been studied systematically in [18]. These can be highlighted by us- ing a well-known tool for translating argumentation frameworks to logic programs [39]. In particular, given an argumentation framework AF one can build an ASP program, PAF as follows. For each argument a in AF, if c1 , c2 , ..., cm is the set of its defeaters (i.e., the set of arguments that attack a), we construct the rule a ← not c1 , not c2 , . . . , not cm . Intuitively, each of these rules means that an argument is accepted (inferred as true) if, and only if, all of its defeaters are rejected (inferred as false). More formally, given an argumentation AF = (Ar, att). For each argument a ∈ Ar, we build a rule ra such that H(ra ) = {a}, B+ (ra ) = 0, / and B− (ra ) = {c ∈ Ar | (c, a) ∈ att}. Then, we define PAF as the set of all rules of the form ra , i.e., PAF = {ra | a ∈ Ar}. It is well-known that the answer sets of PAF correspond to the stable extensions of AF [20]. Therefore, the modeling offered by Dung of the SMP through abstract argumen- tation frameworks, leads to a natural and direct modeling of the SMP through ASP. Starting from M, W , and a set of preferences, defined as above, we constructs an ASP program P as follows. The set of atoms of P is At(P) = M × W . For each pair Solving the SRP using Incoherent ASP Programs 5 (m, w) ∈ M ×W , we build a rule r(m,w) such that H(r(m,w) ) = {(m, w)}, B+ (r(m,w) ) = 0, / and (m, w0 ) ∈ B− (r(m,w) ) if m prefers w0 to w; and (m0 , w) ∈ B− (r(m,w) ) if w prefers m0 to m. Hence, P is defined as the set {r(m,w) | (m, w) ∈ M ×W }. Therefore, it can be shown that Theorem 2. A set S ⊆ M ×W constitutes a solution to the SMP if, and only if, S is an answer set of the corresponding ASP program. Example 3. Consider again the SMP instance of the Example 2. Hence, the correspond- ing logic program P is given by the following set of rules: (m1 , w1 ) ← not(m1 , w4 ), not(m1 , w2 ), not(m2 , w1 ) (m1 , w2 ) ← not(m3 , w2 ), not(m4 , w2 ), (m1 , w3 ) ← not(m1 , w1 ), not(m1 , w4 ), not(m1 , w2 ) (m1 , w4 ) ← not(m1 , w2 ), not(m2 , w4 ) (m2 , w1 ) ← not(m2 , w3 ) (m2 , w2 ) ← not(m2 , w4 ), not(m2 , w1 ), not(m2 , w3 ), not(m1 , w2 ), not(m3 , w2 ), not(m4 , w2 ) (m2 , w3 ) ← not(m3 , w3 ), not(m4 , w3 ), not(m1 , w3 ) (m2 , w4 ) ← not(m2 , w1 ), not(m2 , w3 ), (m3 , w1 ) ← not(m3 , w3 ), not(m3 , w2 ), not(m4 , w1 ), not(m1 , w1 ), not(m1 , w2 ) (m3 , w2 ) ← not(m4 , w2 ) (m3 , w3 ) ← not(m3 , w2 ), not(m4 , w3 ), not(m1 , w3 ) (m3 , w4 ) ← not(m3 , w1 ), not(m3 , w3 ), not(m3 , w2 ), not(m4 , w4 ), not(m1 , w4 ), not(m2 , w4 ) (m4 , w1 ) ← not(m4 , w4 ), not(m1 , w1 ), not(m2 , w1 ) (m4 , w2 ) ← not(m4 , w3 ), not(m4 , w1 ), not(m4 , w4 ) (m4 , w3 ) ← not(m4 , w1 ), not(m4 , w4 ), not(m1 , w3 ) (m4 , w4 ) ← not(m1 , w4 ), not(m2 , w4 ) It can be checked that {(m1 , w4 ), (m2 , w3 ), (m3 , w2 ), (m4 , w1 )}, and {(m1 , w4 ), (m2 , w1 ), (m3 , w2 ), (m4 , w3 )} are the answer sets of P, according to the Theorem 2. We stress that the ASP modeling of the SMP introduced above is a direct and natural representation of the problem [20]. 4 Stable Roommates Problem via Incoherent ASP Programs In the literature, there exists several variants of the SMP [30, 32, 38, 34], those are also studied from a modeling perspective using ASP [19]. In the previous Section, we have pointed out that the sets M and W were disjoint. What happens if M ∩W 6= 0? / In partic- ular, we can assume that the two sets coincide, we call A this set, and each person in A ranks all the others persons in order of preferences. This variant of the SMP is known as the Stable Roommates Problem (SRP) [22]. Clearly, to have a stable roommates a necessary condition is that the cardinality of A is even, otherwise no stable matching could exist. 6 G. Amendola More formally, let A be a set of 2n persons. For each person p ∈ A, we consider a bijective map π p : A \ {p} → {1, 2, ..., 2n − 1} that assigns to each other person in A a number from 1 to 2n − 1, denoting the ranking. For instance, if n = 2, we have a set of 4 persons A = {p1 , p2 , p3 , p4 }. Assume that person p1 prefers person p2 to person p3 , and prefers person p3 to person p4 . Then, we will have that π p1 (p2 ) = 1, π p1 (p3 ) = 2, and π p1 (p4 ) = 3. The goal is to find a set S of n pairs, say A1 , A2 , ..., An that form a partition of A (i.e., A1 ∪ A2 ∪ . . . ∪ An = A, and Ai ∩ A j = 0, / for each i 6= j) such that no two persons who are not roommates both prefer each other to their actual partners. Now, the SRP has a structure similar to the SMP. Hence, the modeling of the SMP via ASP can be applied as it is to the SRP. There is no substantial motivation to change it. It remains a direct and a natural encoding also for the SRP. Theorem 3. A set S ⊆ A × A constitutes a solution to the SRP if, and only if, S is an answer set of the corresponding ASP program. Example 4. Consider the following instance of the SRP: A = {p1 , p2 , p3 , p4 }, and p1 prefers p2 to p4 ; p1 prefers p4 to p3 ; p2 prefers p3 to p1 ; p2 prefers p1 to p4 ; p3 prefers p1 to p4 ; p3 prefers p4 to p2 ; p4 prefers p3 to p2 ; p4 prefers p2 to p1 . So that, π p1 (p2 ) = 1, π p1 (p3 ) = 3, π p1 (p4 ) = 2, π p2 (p1 ) = 2, π p2 (p3 ) = 1, π p2 (p4 ) = 3, π p3 (p1 ) = 1, π p3 (p2 ) = 3, π p3 (p4 ) = 2, π p4 (p1 ) = 3, π p4 (p2 ) = 2, π p4 (p3 ) = 1. Therefore, the ASP program associated to this SRP instance is given by the following set of rules:     (p1 , p2 ) ← not(p2 , p3 )   (p , p ) ← not(p , p ), not(p , p )   1 3 1 4 1 2       (p1 , p4 ) ← not(p1 , p2 ), not(p2 , p4 ), not(p3 , p4 )   P= .   (p2 , p3 ) ← not(p3 , p4 ), not(p1 , p3 )   (p2 , p4 ) ← not(p1 , p2 ), not(p2 , p3 ), not(p3 , p4 )         (p3 , p4 ) ← not(p1 , p3 )   It can be checked that {(p1 , p2 ), (p3 , p4 )} is the unique solution to this SRP instance as well as the unique answer set of P, according to the Theorem 3. However, unlike the SMP, a stable matching for the SRP may fail to exist for certain sets of persons and their preferences. In this case no answer set of the modeling program exists. Example 5. Consider the following instance of the SRP: A = {p1 , p2 , p3 , p4 }, and p1 prefers p2 to p3 ; p1 prefers p3 to p4 ; p2 prefers p3 to p1 ; p2 prefers p1 to p4 ; p3 prefers p1 to p2 ; p3 prefers p2 to p4 ; p4 prefers p1 to p2 ; p4 prefers p2 to p3 . So that, π p1 (p2 ) = 1, π p1 (p3 ) = 2, π p1 (p4 ) = 3, π p2 (p1 ) = 2, π p2 (p3 ) = 1, π p2 (p4 ) = 3, π p3 (p1 ) = 1, π p3 (p2 ) = 2, π p3 (p4 ) = 3, π p4 (p1 ) = 1, π p4 (p2 ) = 2, π p4 (p3 ) = 3. Therefore, the ASP program associated to this SRP instance is given by the following set of rules: Solving the SRP using Incoherent ASP Programs 7 (p1 , p4 ) (p2 , p4 ) (p1 , p2 ) (p1 , p3 ) (p2 , p3 ) (p3 , p4 ) Fig. 1: Dependency graph of the program P of the Example 5.     (p1 , p2 ) ← not(p2 , p3 )   (p , p ) ← not(p , p )   1 3 1 2       (p1 , p4 ) ← not(p1 , p3 ), not(p1 , p2 )   P= .   (p2 , p3 ) ← not(p1 , p3 )   (p2 , p4 ) ← not(p1 , p2 ), not(p2 , p3 ), not(p1 , p4 )         (p3 , p4 ) ← not(p2 , p3 ), not(p1 , p3 ), not(p2 , p4 ), not(p1 , p4 )   To highlight the negative dependecies of each atom of the program, the dependency graph of P is reported in Figure 1. It can be checked that there is no solution to this SRP instance as well as no answer set of P exists, according to the Theorem 3. Note that the lack of answer sets is not due to the violation of some constraint. In- deed, no constraint appears in the encoding above. But, it is caused by cyclic default negation. We point out that the absence of answer sets is not due to a wrong modeling approach. It concerns the intrinsic characteristics of the notion of answer set. However, it is noteworthy that in literature and, in particular, in all the benchmarks appearing in the ASP competitions, the lack of answer sets is always due to the violation of some constraint [26, 5, 6]. 5 Conclusion In this paper, we investigated a modeling of the SMP via ASP, by showing its natural- ness through its relations with abstract argumentation modeling. However, the modeling proposed may lead to lack of answer sets due to cyclic default negation, when we move from the SMP to the SRP. Hence, this modeling approach to the SRP leads to have a first benchmark with consistent, but incoherent ASP programs. 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) 8 G. Amendola 2. Alviano, M., Amendola, G., Peñaloza, R.: Minimal undefinedness for fuzzy answer sets. In: AAAI. pp. 3694–3700. AAAI Press (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., Dodaro, C., Faber, W., Leone, N., Ricca, F.: On the computation of paraco- herent answer sets. In: AAAI. pp. 1034–1040. AAAI Press (2017) 6. 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) 7. 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) 8. 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) 9. 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) 10. 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) 11. 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) 12. Amendola, G., Ricca, F., Truszczynski, M.: Generating hard random boolean formulas and disjunctive logic programs. In: IJCAI. pp. 532–538. ijcai.org (2017) 13. Amendola, G., Ricca, F., Truszczynski, M.: A generator of hard 2qbf formulas and asp pro- grams. In: KR. AAAI Press (2018) 14. 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) 15. 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) 16. Brewka, G., Eiter, T., Truszczynski, M.: Answer set programming at a glance. Com. ACM 54(12), 92–103 (2011) 17. Calimeri, F., Gebser, M., Maratea, M., Ricca, F.: Design and results of the Fifth Answer Set Programming Competition. Artif. Intell. 231, 151–181 (2016) 18. Caminada, M., Sá, S., Alcântara, J., Dvorák, W.: On the equivalence between logic program- ming semantics and argumentation semantics. Int. J. Approx. Reasoning 58, 87–111 (2015) 19. Clercq, S.D., Schockaert, S., Cock, M.D., Nowé, A.: Solving stable matching problems using answer set programming. TPLP 16(3), 247–268 (2016) 20. Dung, P.M.: On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artif. Intell. 77(2), 321–358 (1995) 21. Erdem, E., Öztok, U.: Generating explanations for biomedical queries. TPLP 15(1), 35–78 (2015) 22. Gale, D., Shapley, L.S.: College admissions and the stability of marriage. The American Mathematical Monthly 69(1), 9–15 (1962), http://www.jstor.org/stable/2312726 23. 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) Solving the SRP using Incoherent ASP Programs 9 24. 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) 25. Gebser, M., Maratea, M., Ricca, F.: What’s hot in the answer set programming competition. In: AAAI. pp. 4327–4329. AAAI Press (2016) 26. Gebser, M., Maratea, M., Ricca, F.: The sixth answer set programming competition. Journal of Artificial Intelligence Research 60, 41–95 (2017) 27. Gelfond, M., Lifschitz, V.: Classical negation in logic programs and disjunctive databases. New Generation Comput. 9(3/4), 365–386 (1991) 28. 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) 29. 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) 30. Gusfield, D.: Three fast algorithms for four problems in stable marriage. SIAM J. Comput. 16(1), 111–128 (1987) 31. Gusfield, D., Irving, R.W.: The Stable marriage problem - structure and algorithms. Founda- tions of computing series, MIT Press (1989) 32. Irving, R.W., Leather, P., Gusfield, D.: An efficient algorithm for the ”optimal” stable mar- riage. J. ACM 34(3), 532–543 (1987) 33. Lierler, Y., Maratea, M., Ricca, F.: Systems, engineering environments, and competitions. AI Magazine 37(3), 45–52 (2016) 34. Manlove, D., Irving, R.W., Iwama, K., Miyazaki, S., Morita, Y.: Hard variants of stable marriage. Theor. Comput. Sci. 276(1-2), 261–279 (2002) 35. 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) 36. Maratea, M., Pulina, L., Ricca, F.: A multi-engine approach to answer-set programming. TPLP 14(6), 841–868 (2014) 37. 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) 38. McDermid, E., Irving, R.W.: Sex-equal stable matchings: Complexity and exact algorithms. Algorithmica 68(3), 545–570 (2014) 39. Wu, Y., Caminada, M., Gabbay, D.M.: Complete extensions in argumentation coincide with 3-valued stable models in logic programming. Studia Logica 93(2-3), 383–403 (2009)