Modeling and Reasoning about NTU Games via Answer Set Programming

1 Introduction

Coalitional games are mathematical models which have been proposed to study payoff distribution problems among cooperative agents [von Neumann and Morgenstern, 1944]. In the classical setting where utility can be freely transferred among agents, a game can be defined as a pair hN↪ vi, where N is a finite set of agents and where v is a function associating each coalition S ✓ N with the worth v(S) 2 R that agents in S can get by collaborating with each other. A fundamental problem over hN↪ vi is then to single out the most desirable distributions of the total worth v(N), called solution concepts, which can be perceived as fair and stable (see, e.g., [Osborne and Rubinstein, 1994]).

Since the nineties, coalitional games gained popularity in the artificial intelligence community where solution concepts have been reconsidered from the computational viewpoint (cf. [Deng and Papadimitriou, 1994]). In particular, moving from the observation that explicitly listing all coalitions with their worths is unfeasible over games involving many agents, significant efforts have been spent to study compact representations for coalitional games (see, e.g., [Chalkiadakis et al., 2011; Greco et al., 2011]). In a compact representation, a game hN↪ vi is defined via an encoding, such as a combinatorial structure, a graphical structure, or a logical theory; and, for each coalition S ✓ N, the worth v(S) is computed via an algorithm taking as input that structure and the coalition S.

Example 1. The graph on the left of Figure 1 can be a compact representation for a game over the set N = ¶1↪ 2↪ 3↪ 4♦ of agents one-to-one corresponding with its nodes. For instance, for each coalition S ✓ N, we might define v(S) as the number of edges in the subgraph induced over the nodes in S. E.g., we have v(¶1↪ 2↪ 3♦) = 2 and v(¶1↪ 2↪ 3↪ 4♦) = 3. In general, as every graph on ♣N♣ nodes has O(♣N♣2 ) edges, the encoding is exponentially more succinct than explicitly listing the worths associated with all 2♣N♣ coalitions. C

Whenever utility cannot be freely transferred, the classical model for coalitional games can be generalized by associating each coalition S ✓ N with all the possible payoff distributions that are allowed to the agents in S, rather than with just one value v(S). Games of this kind have been firstly studied by Aumann and Peleg [1960] and they are called coalitional games with non-transferable utility (short: NTU games).

Formally, for any coalition S ✓ N, let RS be the ♣S♣- dimensional real coordinate space, whose coordinates are labeled with the members of S; in particular, given a payoff vector x 2 RS , xi denotes the component associated with the agent i 2 S. Then, an NTU game is a pair hN↪ V i, where N is a finite set of agents and V is a function associating each coalition S ✓ N with a set of payoff vectors V (S) ✓ RS , which are also called consequences.

Applications of NTU games include frameworks for distributing invisible goods, for service composition, for task assignment, for coordination in wireless networks, and more generally all frameworks where incentives to cooperation are provided via payments taking values from discrete domains (see, e.g., [Greco et al., 2010] and the references therein).

When looking at the specification of NTU games from the computer science perspective, however, we might note that there is no clear way to adapt over them existing encodings defined for games with transferable utility (short: TU games). In fact, for each given coalition S ✓ N, V (S) is not a single real number which can be computed on top of the encoding, but it is actually a set of different alternatives that are available to the agents in S. Accordingly, compact representations for NTU games must provide not only a mechanism to reason about exponentially many coalitions (as with TU games), but also a mechanism that, for each given coalition S ✓ N, allows to succinctly encode the consequences in V (S).

As a matter of fact, very few efforts have been spent in the literature to define compact encodings for NTU games, and a representation that naturally provides the support discussed above was missing, so far. The goal of the paper is to fill this gap, by proposing a representation for NTU games founding on answer set programming [Gelfond and Lifschitz, 1991].

Indeed, answer set programming is a declarative programming paradigm where problems are specified in terms of logic programs, and its key feature is that the semantics of each program P is given in terms of a set AS(P) of answer sets, each one describing a possible alterative model for P . Hence, compact representations for NTU games can be naturally based on encoding their alternatives/consequences in terms of answer sets of suitably associated programs.

In the paper, we formalize this observation and we show that every NTU game with a finite set of consequences can be represented as an answer set game. Then, we embark on the study of the computational complexity of such games, by considering stratified and normal programs and by focusing on the core as a reference solution concept [Edgeworth, 1881]. For instance, we consider the problems of checking whether a given distribution is in the core and whether the core of a game is empty. Finally, we report results of experimental activity conducted over a system prototype we have implemented to support the above reasoning tasks. Notably, no reasoner for arbitrary NTU games was available, so far.

2 Preliminaries

Answer Set Programming. Let Γ be a set of atoms. A rule r on Γ is an expression having the form

The head of r is the set H(r) = ¶a♦, and the positive (resp., negative) body of r is the set B+(r) = ¶b1↪ ▷▷▷↪ bm♦ (resp., B-(r) = ¶c1↪ ▷▷▷↪ cn♦). If B-(r) = B+(r) = ;, then the arrow " " will be omitted in the notation.

A (normal) program P is a finite set of rules. An interpretation of P is any set I ✓ Γ of atoms. We say that I satisfies a rule r if B+(r) ✓ I and B-(r)\I = ; implies I\H(r) 6= ;. If I satisfies every rule r 2 P, then I is a model of P. The reduct of P w.r.t. an interpretation I is the program P I such that: (i) for each rule r 2 P with B-(r) \ I = ;, P I contains the rule r0 with H(r0 ) = H(r), B+(r0 ) = B+(r), and B-(r0 ) = ;; (ii) no further rule is in P I . An interpretation I is an answer set of P if it is a subset-minimal model of P I . The set of all answer sets of P is denoted by AS(P).

A normal program P is stratified if the atoms can be partitioned into pairwise disjoint sets S1↪ ▷▷▷↪ Sn such that, for each a 2 Si and b 2 Sj, if there is a rule r 2 P with a 2 H(r) and b 2 B+(r) (resp., b 2 B-(r)), then i ≥ j (resp., i > j).

Theorem 1. The following computational properties are known to hold (see, e.g., [Dantsin et al., 2001]):

1. Every stratified program has a unique answer set that, moreover, can be computed in polynomial time.
2. For normal programs P, checking whether an interpretation M belongs to AS(P) is feasible in polynomial time, while deciding whether AS(P) 6= ; is NPcomplete.

Imputations and Cores. Let G = hN↪ V i be an NTU game. A consequence x 2 V (N) is an imputation of G if the following two properties hold (see, e.g., [Peleg, 1963]):

• ÷ Efficiency: for each y 2 V (N), there is an agent i 2 N such that xi ≥ yi; and
• ÷ Individual Rationality: for each agent i 2 N, xi ≥ max¶yi ♣ yi 2 V (¶i♦)♦.

Intuitively, the former condition restricts imputations to those consequences where it is impossible to make any agent better off without making at least another agent worse off. Instead, the latter condition filters out all consequences where an agent receives less than it could obtain on its own, i.e., without cooperating with anyone else. In the following, the set of all imputations of G is denoted by I(G).

Solutions concepts are defined in the literature as imputations enjoying additional desirable properties. In the paper, we focus on the core of G, denoted by C(G), which is the set of all imputations x for which there is no objection, i.e., pair (y↪ S) such that y 2 V (S) and yk > xk, for each k 2 S [Aumann, 1961]. Therefore, this outcome represents a kind of agreement amongst players, in that it is "stable" with respect to the possibility that subsets of players get an incentive to deviate from it, by forming coalitions on their own.

Fact 1. If G=hN↪ V i is such that ♣N♣  2, then I(G) = C(G).

3 Formal Framework

In this section, we introduce answer set games and specialize over them the basic concepts about coalitional games.

3.1 Answer Set Games

Let N be a set of agents. An environment for N is a tuple ⌦ = hN↪ P↪ !i, where P is a vector of logic programs on a set Γ of atoms and ! is a vector of weight functions mapping interpretations to real numbers. In particular, the components of P and ! are labeled with the members of N.

We assume that Γ ◆ N, that is, agents are transparently viewed as atoms. Moreover, for each agent i 2 N and rule r 2 Pi, we require that H(r) \ N = ;, that is, atoms in N occur only in rule bodies. Finally, for each i 2 N, we require that !i is polynomial-time computable. In the following, whenever !i(I) = Pa2I !i(¶a♦) holds, for each interpretation I, we shall say that !i is additively separable.

Hereinafter, for each S ✓ N, we define a logic program PS = Si2S (Pi [ ¶i▷♦) based on the logic programs Pi associated with the agents i 2 S. In particular, when i is included in S, we add to PS the program Pi as well as the information that i occurs in S (that is, the fact "i▷"). This information can be used by other agents to reason about members of S. For instance, the logic program of another agent j 6= i can be defined to model scenarios where j can perform some task only in coalitions where i occurs.

The notions introduced above are now exemplified over an environment where logic programs play the role of modeling matchings over an underlying graph-recall that a matching is a set of pairwise non-adjacent edges; thats is, there is no pair of edges sharing some node. The rationale for the chosen exemplification is that matching games constitute one of the most studied class of coalitional games, with applications in matching markets (see, e.g., [Roth and Oliveira Sotomayor, 1990; Shapley and Shubik, 1971]).

Example 2. Consider again the graph shown in Figure 1, and let us define ⌦ = hN↪ P↪ !i, with N = ¶1↪ 2↪ 3↪ 4♦, as follows. Each agent i 2 N is equipped with a program Pi prescribing that at most one of its incident edges can be "selected". The intuition is that, for each S ✓ N, answer sets of PS will correspond to the matchings over the subgraph induced on S. Formally, we use atoms a, b, and c to identify the edges selected in the matching, and ¯a, ¯b, and ¯ c to mean that the corresponding edges are not selected. Then, we define:

Finally, for each agent/node i 2 N, !i is the additively separable function mapping each atom to 0, but the edges incident to i, which are mapped to 1. Hence, for the answer set M, we have !i(M) = 1, for each i 2 ¶1↪ 2↪ 3↪ 4♦. C

Note that the interpretation M = ¶1↪ 2↪ 3↪ 4↪ a↪ ¯b↪ c♦ belongs to AS(PN) = AS(Si2¶1↪2↪3↪4♦ (Pi [ ¶i▷♦)), and it encodes a maximal matching over the graph-see Figure 1.

Environments are now used to induce, in a natural way, an NTU game over the agents in N. Formally, the answer set game associated with ⌦ is the game G⌦ = hN↪ V⌦i where, for each S ✓ N, the set V⌦(S) is defined as follows:

Example 3. In Example 2, consider the coalition S = ¶2↪ 4♦. We have V⌦(S) = ¶↵↪ β♦ with ↵2 = ↵4 = 1 (corresponding to the matching where the edge c is selected) and β2 = β4 = 0 (corresponding to the case where no edge is selected). C

It is easy to see that any finite NTU game hN↪ V i, i.e., such that V (S) is a finite set of outcomes, for each S ✓ N, can be defined by using a suitable environment. 1

Theorem 2. For each finite NTU game hN↪ V i, there is an environment ⌦ over N such that V⌦(S) = V (S), 8S ✓ N.

1 See http://ntu2dlv.altervista.org/, for details and missing proofs.

In fact, the environments in the above result founds on programs whose rules are associated with all possible coalitions S ✓ N and with all possible outcomes in V (S). But, more succinct encodings can be obtained in some cases. For instance, by generalizing Example 2 to arbitrary graphs, it is easily seen that all (possibly exponentially-many) matchings can be encoded via programs with polynomially-many rules, only. For instance, for a clique over N, the number of maximal matching is exponential w.r.t. ♣N♣, but the number of rules in each program Pi is linearly bounded by the number of such nodes. For a further example of a succinct encoding, we can consider an environment where, for each i 2 N, we have Pi = ¶ai i↪ not ¯ai▷♦ [ ¶¯ai i↪ not ai▷♦ and !i(¶ai♦) = 1, with all other atoms mapped to 0. Then, we can check that ♣AS(PN)♣ = ♣V⌦(N)♣ = 2♣N♣ holds.

More importantly, the modeling capabilities of answer set programming make the setting expressive enough to deal with a number of real-world applications, for instance, to encode games defined over combinatorial structures [Bilbao, 2012]. Indeed, for each i 2 N, Pi might encode different combinatorial problems, ranging from scheduling, to routing and planning, just to name a few (see, e.g., [Grasso et al., 2013]).

Example 4. Consider a setting where, in order to perform a task t, a set S of skills are required, and where each agent i 2 N has some skills s1↪ ▷▷▷↪ shi taken from S. Consider a stratified logic program P modeling the conditions under which t is executed. In particular, if T ✓ S is a set of available skills, then the unique answer set M of P [ Ss2T ¶s▷♦ is such that: t 2 M, if and only if, T = S. Note that further specific application-oriented constraints can be defined in P .

Now, for each agent i 2 N, consider the program Pi = P [ ¶s1▷♦ [ · · · [ ¶shi ▷♦ and the weight function !i such that !i(M) = 1 (resp., !i(M) = 1) if t 2 M (resp., t 62 M). Then, the game G⌦ = hN↪ V⌦i is such that, for each S ✓ N, V⌦(S) = ¶x♦ where each component of x is 1 (resp., 0) if agents in S have (resp., do not have) the skills to perform t.

Simple extensions of the exemplification include the execution of more than one task, and the definition of a monetary reward that is specific for each task being executed and for the specific skills provided by each agent. C

3.2 Solution Concepts

Answer sets games G⌦ are standard NTU games and, therefore, we can apply on them well-known notions and solution concepts from coalitional game theory. In fact, such notions and concepts can be recast in terms of the underlying vector of logic programs P , as we discuss below.

Note first that, if x is an imputation in I(G⌦), then x 2 V⌦(N) holds and, by definition of of V⌦, there is an answer set M 2 AS(PN) such that xi = !i(M), for each i 2 N. This is called an imputation answer set of PN w.r.t. G⌦, and a useful characterization for it is next provided.

Fact 2. An interpretation M 2 AS(PN) is an imputation answer set if, and only if, the following properties hold:

• ÷ "Efficiency": for eachM 0 2 AS(PN), there is an agent i 2 N such that !i(M) ≥ !i(M 0 ); and
• ÷ "Individual Rationality": for each agent i 2 N, !i(M) ≥ max¶!i(M 0 ) ♣ M 0 2 AS(P¶i♦)♦.

Example 5. Recall from Example 2 that M = ¶1↪ 2↪ 3↪ 4↪ a↪ ¯b↪ c♦ 2 AS(PN) and !1(M) = 1. This is the best possible value for !1; hence, M is efficient. Moreover, !i(M) = 1 ≥ max¶!i(M 0 ) ♣ M 0 2 AS(P¶i♦)♦, for each i 2 N. Indeed, P¶i♦ has one answer set ¶i▷♦ and !i(¶i▷♦) = 0. So, M is also individually rational. Thus, it is an imputation answer set. C

Let IAS(P↪ G⌦) denote the set of all imputation answer sets. An interesting property is that, as far as the non-emptiness of IAS(P↪ G⌦) is concerned, efficiency in Fact 2 is immaterial.

Theorem 3. If there is an answer set of PN that satisfies the individual rationality property, then IAS(P↪ G⌦) 6= ;.

In addition to the elements in IAS(P↪ G⌦), the paper will also study core answer sets. Formally, an interpretation M 2 AS(PN) is a core answer set of PN w.r.t. G⌦ if !(M) 2 C(G⌦). Let CAS(P↪ G⌦) be the set of all core answer sets. In order to characterize these elements, given an interpretation M and a coalition S ✓ N, we say that M is S-feasible if M 2 AS(PS). Then, the following can be derived.

• ÷ M is an imputation answer set (i.e., M 2 IAS(P↪ G⌦));

Fact 3. An interpretation M 2 AS(PN) is a core answer set of PN w.r.t. G⌦ if, and only if, the following properties hold:

• ÷ "Absence of Objections": there is no S-feasible interpretation M 0 such that !k(M 0 ) > !k(M), 8k 2 S.

Instead, the set ¶1↪ 2↪ 3↪ 4↪ a↪¯b↪ ¯ c♦ 2 IAS(P↪ G⌦) is not a core answer set. Indeed, by Example 3, we know that coalition ¶2↪ 4♦ can object. In fact, for the interpretation ¶2↪ 4↪ ¯b↪ c♦2AS(P¶2↪4♦), we can derive that !2(¶2↪ 4↪ ¯b↪ c♦) = !4(¶2↪ 4↪ ¯b↪ c♦) = 1, while we have !2(¶1↪ 2↪ 3↪ 4↪ a↪ ¯b↪ ¯ c♦) = !4(¶1↪ 2↪ 3↪ 4↪ a↪ ¯b↪ ¯ c♦) = 0.

Example 6. In our example, M 2 AS(PN) is a core answer set. This is witnessed by Fact 3 and by observing that, for each coalition S ✓ N and for each M 0 2 AS(PS), there is always some agent k 2 S such that !k(M 0 )  !k(M).

More generally, it can be checked that an answer set in AS(PN) is a core answer set if, and only if, it corresponds to a maximal matching over the underlying graph. C

4 Computational Complexity Aspects

In this section, we study the computational complexity of the following reasoning tasks, all of them receiving as input an environment ⌦ and being defined over the game G⌦:

C-NONEMPTY: Does C(G⌦) 6= ; hold?

I-CHECK: Given a vector x, is x 2 I(G⌦)?

I-NONEMPTY: Does I(G⌦) 6= ; hold?

C-CHECK: Given a vector x, is x 2 C(G⌦) hold?

In addition, we study the following problems 2 where solution concepts for G⌦ are recast in terms of answer sets:

IAS-NONEMPTY: Does IAS(P↪ G⌦) 6= ; hold?

IAS-CHECK: Given an interpretationM, is M2IAS(P↪ G⌦)? CAS-CHECK: Given an interpretationM, isM2CAS(P↪ G⌦)?

CAS-NONEMPTY: Does CAS(P↪ G⌦) 6= ; hold?

2 Note that IAS-NONEMPTY and CAS-NONEMPTY are equivalent to I-NONEMPTY and C-NONEMPTY. Indeed, I(G⌦) 6= ; (resp., C(G⌦) 6= ;) iff IAS(P↪ G⌦) 6= ; (resp., CAS(P↪ G⌦) 6= ;).

A summary of our results is reported in Table 1, by distinguishing normal and stratified environments ⌦ = hN↪ P↪ !i, that is, when PN (hence, each program PS with S ✓ N) is normal and stratified, respectively. Note that, for each problem, say P, we report the complexity when the input is restricted over environments such that ♣N♣ = h, where h 2 N is a given fixed natural number, by denoting the problem as P[h]. For notational uniformity, the original problem P, without any bound on N, is also denoted as P[1].

4.1 Overview of the Proofs

We now discuss some representative proofs for the results reported in Table 1. In particular, we focus on intractability results only, and we start with stratified environments.

Theorem 4. CAS-CHECK[1] is coNP-complete on stratified environments.

Proof sketch. Membership is routine. For the hardness, let Φ = c1 ^ ▷▷▷ ^ cm be a Boolean formula in conjunctive normal form over the variables in ¶X1↪ ▷▷▷↪Xn♦. For a literal Xi (resp., ≻Xi) in a clause cj, let ⇡(Xi) = Xi (resp., ⇡(≻Xi) = not Xi). Deciding the satisfiability of such formulas is a well-known NP-hard problem.

Based on Φ, we build in polynomial time an environment ⌦ = hN↪ P↪ !i such that N = ¶1↪ ▷▷▷↪ n♦, Pi = ¶Xi i▷♦ [ Q, for each i 2 N, where

and where, for each i 2 N, !i(I) = 1 (resp., !i(I) = 0) if sat 2 I (resp., sat 62 I). W.l.o.g., assume that the truth assignment ¯σ where all variables evaluate true is not satisfying, and consider the answer set M = ¶satj ♣ cj evaluates true in ¯σ♦ [ Si2N ¶i▷♦ of PN. Note that M is the unique answer set of PN, as the program is stratified. The result then follows by checking that M 62 CAS(P↪ G⌦) if, and only if, Φ is satisfiable.

Considering normal environments, completeness results for the polynomial-time closure of NP emerge.

Theorem 5. 8h 2 N ∩ ¶1♦ [ ¶1♦, IAS-NONEMPTY[h] is ∆p2 -complete on normal environments.

Proof Sketch. For the membership part, by Theorem 3, we have to check whether there exists an answer set satisfying the individual rationality property. To check this property, we can first compute, for each i 2 N, the value mi = max¶!i(M 0 ) ♣ M 0 2 AS(P¶i♦)♦. This can be done by means of a binary search within the range for the possible values for mi. At each step, we just ask whether there is an answer set M 0 2 AS(P¶i♦) with !i(M 0 ) exceeding the current given threshold. Each step is hence feasible in NP, so mi can be computed in ∆p2 . Eventually, we can guess an interpretation M by then checking that M 2 AS(PN) and that, for each i 2 N, !i(M) ≥ mi. The whole computation is in ∆p2 .

For the hardness, we exhibit a reduction from the ∆p2 - complete OddLexMaxSAT problem [Wagner, 1987]. We are given a Boolean formula Φ = c1 ^ ▷▷▷ ^ cm in conjunctive normal form over the variables in ¶X1↪ ▷▷▷↪Xn♦. Such variables are lexicographically ordered (X1 < · · · < Xn), and we ask whether X1 evaluates true in the lexicographically maximum satisfying assignment-w.l.o.g., Φ is satisfiable by a satisfying assignment where X1 evaluates true. In the following, for a literal Xi (resp., ≻Xi), let ⇡(Xi) = Xi (resp., ⇡(≻Xi) = not Xi). Based on Φ, we build in polynomial time an environment ⌦ = hN↪ P↪ !i over two agents, i.e., N = ¶1↪ 2♦, and where P1 = P2 consists of the following rules:

Finally, we consider two additively separable weight functions, !1 and !2, given by

We claim that Φ is a "yes" instance of OddLexMaxSAT if, and only if, IAS(P↪ G⌦) 6= ;-the reduction can be extended to the case where ♣N♣ > 2, by setting !i(I) = 0, for each agent i 2 N ∩ ¶1↪ 2♦ and interpretation I. In the following, for each assignment σ, let Mσ be the (univocally determined) answer set of PN with Mσ ◆ ¶Xi ♣ Xi evaluates true in σ♦.

Assume that X1 evaluates false in the lexicographically maximum satisfying assignment σ. Recall that Φ is satisfiable by a satisfying assignment, say ˆσ, where X1 evaluates true. Consider the interpretation Mˆσ. Assume, for the sake of contradiction, that M is an answer set in IAS(P↪ G⌦). Note that !2(M) ≥ !2(Mˆσ) = 1 must hold, since M is individually rational. That is, X1 must occur in M. Consider then the assignment ¯σ such that Xi evaluates true if, and only if, Xi 2 M. Note that M = M¯σ. However, !1(M¯σ) < !1(Mσ), because σ is the lexicographically maximum satisfying assignment and ¯σ 6= σ, as X1 evaluates true

(resp., false) in ¯σ (resp., σ). So, M is not individually rational. This leads to a contradiction.

Eventually, assume that X1 is true in the lexicographically maximum satisfying assignment σ⇤ . Note that Mσ⇤ ◆ ¶X1♦, !1(Mσ⇤) = PXi♣Xi evaluates true in σ⇤2i and !2(Mσ⇤) = 1. Therefore, it can be checked that Mσ⇤ is efficient and individually rational.

We leave the section by exhibiting a completeness result for the second level of the polynomial hierarchy.

Theorem 6. 8h 2 N∩¶1↪ 2♦[¶1♦, CAS-NONEMPTY[h] is ⌃p2 -complete on normal environments.

Proof Sketch. In order to solve CAS-NONEMPTY, we can start by guessing an interpretation M. This task is clearly feasible in NP. Subsequently, we have to check whether M is a core answer set, which is feasible in coNP. Therefore, CAS-NONEMPTY is in ⌃p2 . For the hardness, we exhibit a reduction from the prototypical ⌃p2 -complete problem of deciding the validity of a quantified Boolean formula having the form 9X1↪ ▷▷▷↪Xn8Y1↪ ▷▷▷↪ YmΦ. Without loss of generality, we assume that Φ is in disjunctive normal form, that is, Φ = D1 _ ▷▷▷ _ Dr where, for each k 2 ¶1↪ ▷▷▷↪ r♦, Dk = lk1 ^ lk2 ^ lk3 is a conjunction of literals.

Consider the following normal program:

Let C = ¶c12↪ c13↪ c23↪ c123♦. Moreover, consider the following normal logic program

First, we define N = ¶1↪ 2↪ 3♦. Then, we let P1 = P2 = P3 = PΦ [ Q. And, finally, the weight functions are the additively separable functions given by

Now, based on and given P and C, we build the answer set game G⌦, where ⌦ = hN↪ P↪ !i is defined as follows.

Let M be an answer set in AS(PN) and observe that M ◆ ¶1↪ 2↪ 3↪ c123♦. Therefore, we have:

Eventually, it can be checked that is valid if, and only if, there is a core answer set.

• ÷ !1(M) = 2n+1 + PXi2M 2i + 1 - !3(M); ÷ !2(M) = 2n+1 + P ¯Xi2M 2i + 1 - !3(M).

(only-if part) Assume that σX is a truth assignment over the variables in ¶X1↪ ▷▷▷↪Xn♦ witnessing the validity of . Let σ be a truth assignment for Φ whose restriction on ¶X1↪ ▷▷▷↪ Xn♦ coincides with σX, and note that σ is satisfying. Consider the answer set Mσ 2 AS(PN) such that Mσ ◆ ¶Xi ♣ Xi evaluates true in σ♦. Note that Mσ is univocally defined and sat 2 Mσ. Now, we show that M is individually rational. Indeed, consider an answer set M1 2 AS(P¶1♦), hence, such that C \M1 = ;. Then, !1(M1)  2n+1  !1(Mσ). Similarly, for any answer set M2 2 AS(P¶2♦), we have !2(M2)  2n+1  !2(Mσ). Eventually, for any answer set M3 2 AS(P¶3♦), we have !3(M3)  1 = !3(Mσ). By similar arguments, we can show that Mσ is efficient and satisfies the objection property.

(if part) Assume that is not valid, and let M 2 AS(PN). In the case where sat 2 M, we can consider any answer set M 0 of P¶1↪2♦, such that M 0 \ ¶X1↪ ▷▷▷↪Xn♦ = M \ ¶X1↪ ▷▷▷↪Xn♦, and ¯ sat 2 M 0 . As is not valid, one answer set of this kind clearly exists. Moreover, we can note that !1(M 0 ) = !1(M) + 1 and !2(M 0 ) = !2(M) + 1. Therefore, M 0 is ¶1↪ 2♦-feasible and such that !k(M 0 ) > !k(M), for each k 2 ¶1↪ 2♦. Hence, M is not a core answer set. Consider, then, the case where ¯ sat 2 M. W.l.o.g., assume there is an answer set M 0 of P¶2↪3♦ such that M 0 \¶X1↪ ▷▷▷↪ Xn♦ = M \ ¶X1↪ ▷▷▷↪Xn♦ and sat 2 M 0 . Then, !3(M 0 ) = 1 > !3(M) = 0 and !2(M 0 ) = !2(M) + 1. Again, this shows that M is not a core answer set.

5 Implementation and Experiments

To support the reasoning tasks discussed in the paper, a system prototype, named ntu2DLV, has been implemented on top of the well-known answer set programming DLV reasoner [Leone et al., 2006]. In the following, we discuss the architecture of the system and results of some experimental activities we have conducted on it.

5.1 SystemArchitecture

Let ⌦ = hN↪ P↪ !i be a given environment. In order to use ntu2DLV, each program Pi 2 P has to be stored in a file named "agent[i].dl". Analogously, each weight function !i 2 ! has to be stored in a file named "weight[i].txt". We support additively separable functions, so that each line of the file consists of a pattern "[a] ! [v]", where v is the value associated to the atom a. All files have to be stored in a folder and the system can be then invoked as: ./ntu2DLV folderName -reasoning=[imputations♣core], where the option selects the desired reasoning task, that is, computing imputations or core answer sets, respectively. 3

3 The system prototype and further notes on its usage are also available at http://ntu2dlv.altervista.org/.

The system has been implemented in Java. Upon startup, it analyzes the input folder, by parsing the files and creating the associated data structures encoding G⌦. These structures are taken as input by a reasoning module, which interacts with the DLV system via the DLVWrapper library [Ricca, 2003]:

"-reasoning=imputations": When the focus is on imputation answer sets, DLV is invoked to compute AS(P¶i♦), for each i 2 N, and to compute AS(PN). The system then calculates the values max¶!i(M 0 ) ♣ M 0 2 AS(P¶i♦)♦ to discard the elements of AS(PN) that are not individually rational. For each remaining answer set M, the system checks whether there is an agent i such that !i(M) = max¶!i(M) ♣ M 2 AS(PN)♦. In the affirmative case, M is an imputation answer set and is returned as output.

"-reasoning=core": Whenever the system is asked to return core answer sets, DLV is additionally invoked to compute AS(PS), for each coalition S ⇢ N with ♣S♣ > 1. For each M 2 AS(PS), the elements I 2 IAS(P↪ G⌦) such that !i(M) > !i(I), for each i 2 S, are discarded. The imputation answer sets that survive to the filtering process are promoted to core answer sets and returned as output by the system.

5.2 Experiments and Results

Experimental activity has been conducted to assess the efficiency and the effectiveness of ntu2DLV. Tests have been carried out on an Intel Core i7-4710HQ, 2.50 GHz, with 16 Gb Ram, running Linux Operating System; for each test we allowed a maximum running time of 1800 seconds.

In a first series of experiments, we considered the setting discussed in Example 2, where a graph G is given and where ⌦ encodes a matching game. The system has been tested on different data sets of randomly-generated graphs, for normal, uniform and power-law distributions of node degrees. 4 For each given distribution and desired number of nodes, 3 graphs have been generated and average times are discussed. In particular, Table 2 reports the time taken by ntu2DLV to compute an imputation answer set at the growing of the number of the nodes. Note that with the power law distribution, the scaling of the system is quite effective. Indeed, for imputation answer sets, the number of invocations to DLV is always linear w.r.t. the number of agents. However, the number of rules of each program Pi is determined by the number of neighbors of agent i (see Example 2) so that, with the power-law distribution where most agents have only a few neighbors, reasoning on their associated programs is easier-DLV reasoning time tend to be exponential w.r.t. the size of the program.

4 The data generator along with a user guide can be downloaded from the system web-site.

Table 3 reports the (average) time taken by ntu2DLV to compute a core answer set, by focusing on normal edge distributions. In this case, DLV has to be invoked 2♣N♣ times in order to check whether there is some coalition that can object. Therefore, the exponential dependency w.r.t. the number of nodes is unavoidable, and the system does not scale to large scenarios. Pragmatically, as often done in these contexts, one might want to focus on certain coalitions only, as to restrict the search space. For instance, the table reports execution times when coalitions of size 2, 3, and 4 are considered.

For a further series of experiments, we focused on the flexibility of answer set systems to define and solve combinatorial problems (in their turn, inducing NTU games). In particular, we considered the same scenario as in Example 2, but defining programs PS whose answer sets correspond to independent sets over the subgraph induced on S-the encoding is standard and is omitted. In this case, on the specific family of graphs we have considered, it emerged that fewer answer sets are generated compared to matching games. Accordingly, it comes with no surprise that DLV reasoning times are better than those discussed so far. Details are reported in Table 4.

6 Discussion and Conclusion

A compact representation for non-transferable utility games has been proposed which founds on the use of answer set programming. The computational complexity of the framework has been studied, and a system supporting the basic reasoning tasks arising therein has been made available.

Our contribution fills a gap in the literature, where no general mechanism to compactly specify NTU games was proposed, so far. An avenue of research that is related to our work defines NTU games by equipping underlying TU games with some application-oriented constraints on the possible worth distributions-see, e.g., [Aumann and Dreze, 1974; Byford, 2007; Jiang and Baras, 2007] and the general framework of Greco et al. [2010]. Actually, in that framework, constraints are used to define the set V (N), only. For instance, to induce an NTU game where V (¶1↪ 2↪ 3♦) = ¶(1↪ 1↪ 1)♦, we have to specify that x1, x2, and x3 are positive integers, and that x1 + x2 + x3 = 3. Then, for each coalition S, consequences in V (S) are implicitly induced in [Greco et al., 2010] by projecting V (N) over S. For instance, we have V (¶1↪ 2♦) = ¶(1↪ 1)♦ and we have no flexibility to define, e.g., V (¶1↪ 2♦) = ¶(1↪ 1)↪ (2↪ 0)♦. By moving from numerical constraints to logical theories, answer set games are more flexible (in fact, fully expressive). Indeed, the input programs Pi, for each i 2 N, can be defined in a way that the program PS associated with coalition S encodes any desired set V (S).

Natural avenues of further research include the study of other solution concepts over answer set games, for instance taking into account scenarios with restricted agent interactions (see, e.g., [Chalkiadakis et al., 2016]), and the definition of optimization strategies for the system prototype.

Acknowledgments

The authors are supported by the Italian Ministry of University and Research under PON project "Ba2Know (Business Analytics to Know) Service Innovation - LAB", No. PON03PE 00001 1. Gianluigi Greco's work was also supported by a Kurt G¨odel Research Fellowship, awarded by the Kurt G¨odel Society.