Apportionment is the task of assigning resources to entities with different entitlements in a fair manner, and specifically a manner that is as proportional as possible. The best-known application is the assignment of parliamentary seats to political parties based on their share in the popular vote. Here we enrich the standard model of apportionment by associating each seat with a weight representing the (objective) value of that seat. A seat’s weight reflects the fact that different seats might come with different roles, such as chair or treasurer. We define several apportionment methods and natural fairness requirements for this new setting, and we study the extent to which our methods satisfy these requirements. Our findings show that full fairness is harder to achieve than in the standard apportionment setting. Yet, for several natural relaxations of those requirements we can achieve stronger results than in the more expressive model of fair division with entitlements, where the values of objects are subjective.

We initiate the study of voting rules for participatory budgeting using the so-called epistemic approach, where one interprets votes as noisy reflections of some ground truth regarding the objectively best set of projects to fund. Using this approach, we first show that both the most studied rules in the literature and the most widely used rule in practice cannot be justified on epistemic grounds: they cannot be interpreted as maximum likelihood estimators, whatever assumptions we make about the accuracy of voters. Focusing then on welfare-maximising rules, we obtain both positive and negative results regarding epistemic guarantees.

We consider scenarios where a group of agents wish to simplify a given abstract argumentation framework—specifying a set of arguments and the attacks between them—by eliminating cycles in the attack-relation on the basis of their preferences over arguments. They do so by first aggregating their individual preferences into a collective preference order and then removing any attacks involved in a cycle that go against that order. Our analysis integrates insights from formal argumentation and social choice theory. We obtain sweeping impossibility results for essentially all standard methods of preference aggregation, showing that no Condorcet method and no positional scoring rule can uphold the fundamental principle expressing that views held by every single member of the group must be respected. But we also find that so-called representative-agent rules do offer this guarantee.

International audience

In the context of social choice theory, we develop a tableau-based calculus for reasoning about voting rules. This calculus can be used to obtain structured explanations for why a given set of axioms justifies a given election outcome for a given profile of voter preferences. We then show how to operationalise this calculus, using a combination of SAT solving and answer set programming, to arrive at a flexible framework for presenting human-readable justifications to users.

We present an online demonstration tool illustrating a general approach to computing justifications for accepting a given decision when confronted with the preferences of several agents. Such a justification consists of a set of axioms providing a normative basis for the decision, together with a step-by-step explanation of how those axioms determine the decision. Our open-source implementation may also prove useful for realising other kinds of projects in computational social choice, particularly those requiring access to a SAT solver.

In the context of aggregating intervals reflecting the views of several agents into a single interval, we investigate the impact of the form of representation chosen for the intervals involved. Specifically, we ask whether there are natural rules we can define both as rules that aggregate separately the left and right endpoints of intervals and as rules that aggregate separately the left endpoints and the interval widths. We show that on discrete scales it is essentially impossible to do so, while on continuous scales we can characterise the rules meeting these requirements as those that compute a weighted average of the endpoints of the individual intervals.

We introduce an end-to-end model for participatory budgeting grounded in social choice theory. Our model accounts for the interplay between the two stages commonly encountered in real-life partici- patory budgeting. In the first stage participants pro- pose projects to be shortlisted, while in the second stage they vote on which of the shortlisted projects should be funded. Prior work of a formal nature has focused on analysing the second stage only. We in- troduce several shortlisting rules for the first stage and analyse them in both normative and algorith- mic terms. Our main focus is on the incentives of participants to engage in strategic behaviour during the first stage, in which they need to reason about how their proposals will impact the range of strate- gies available to everyone in the second stage.

We develop a powerful approach that makes modern SAT solving techniques available as a tool to support the axiomatic analysis of economic matching mechanisms. Our central result is a preservation theorem, establishing sufficient conditions under which the possibility of designing a matching mechanism meeting certain axiomatic requirements for a given number of agents carries over to all scenarios with strictly fewer agents. This allows us to obtain general results about matching by verifying claims for specific instances using a SAT solver. We use our approach to automatically derive elementary proofs for two new impossibility theorems: (i) a strong form of Roth's classical result regarding the impossibility of designing mechanisms that are both stable and strategyproof and (ii) a result establishing the impossibility of guaranteeing stability while also respecting a basic notion of cross-group fairness (so-called gender-indifference).

Suppose you want to design a voting rule that can be used to elect a committee or parliament by asking each voter to approve of a subset of the candidates standing.There are several properties you may want that rule to satisfy.First, voters should enjoy some form of proportional representation.Second, voters should not have an incentive to misrepresent their preferences.Third, outcomes should be Pareto efficient.We show that it is impossible to design a voting rule that satisfies all three properties.We also explore what possibilities there are when we weaken our requirements.Of special interest is the methodology we use, as a significant part of the proof is outsourced to a SAT solver.While prior work has considered similar questions for the special case of resolute voting rules, which do not allow for ties between outcomes, we focus on the fact that, in practice, most voting rules allow for the possibility of such ties.

We introduce a new approach for designing rules for participatory budgeting, the problem of deciding on the use of public funds based directly on the views expressed by the citizens concerned. The core idea is to embed instances of the participatory budgeting problem into judgment aggregation, a powerful general-purpose framework for modelling collective decision making. Taking advantage of the possibilities offered by judgment aggregation, we enrich the familiar setting of participatory budgeting with additional constraints, namely dependencies between projects and quotas regarding different types of projects. We analyse the rules obtained both in algorithmic and in axiomatic terms.

We provide a comprehensive analysis of the computational complexity of the outcome determination problem for the most important aggregation rules proposed in the literature on logic-based judgment aggregation. Judgment aggregation is a powerful and flexible framework for studying problems of collective decision making that has attracted interest in a range of disciplines, including Legal Theory, Philosophy, Economics, Political Science, and Artificial Intelligence. The problem of computing the outcome for a given list of individual judgments to be aggregated into a single collective judgment is the most fundamental algorithmic challenge arising in this context. Our analysis applies to several different variants of the basic framework of judgment aggregation that have been discussed in the literature, as well as to a new framework that encompasses all existing such frameworks in terms of expressive power and representational succinctness.

We develop a model for the aggregation of preferences that do not need to be either complete or transitive. Our focus is on the normative characterisation of aggregation rules under which each agent has a weight that depends only on the size of her ballot, i.e., on the number of pairs of alternatives for which she chooses to report a relative ranking. We show that for rules that satisfy a restricted form of majoritarianism these weights in fact must be constant, while for rules that are invariant under agents with compatible preferences forming pre-election pacts it must be the case that an agent's weight is inversely proportional to the size of her ballot.

We introduce a formal model of iterative judgment aggregation, enabling the analysis of scenarios in which agents repeatedly update their individual positions on a set of issues, before a final decision is made by applying an aggregation rule to these individual positions. Focusing on two popular aggregation rules, the premise-based rule and the plurality rule, we study under what circumstances convergence to an equilibrium can be guaranteed. We also analyse the quality, in social terms, of the final decisions obtained. Our results not only shed light on the parameters that determine whether iteration converges and is socially beneficial, but they also clarify important differences between iterative judgment aggregation and the related framework of iterative voting.

When confronted with the same abstract argumentation framework, specifying a set of arguments and an attack-relation between them, different agents may disagree on which arguments to accept, i.e., they may choose different extensions. In the context of designing systems to support collective argumentation, we may then wish to aggregate such alternative extensions into a single extension that appropriately reflects the views of the group as a whole. Focusing on a conceptually and computationally simple family of aggregation rules, the quota rules, we analyse under what circumstances relevant properties of extensions shared by all extensions reported by the individual agents will be preserved under aggregation. The properties we consider are the classical properties of argumentation semantics, such as being a conflict-free, a complete, or a preferred extension. We show that, while for some properties there are quota rules that guarantee their preservation, for the more demanding properties it is impossible to do so in general.

We review a recently introduced model in which each of a number of agents is endowed with an abstract argumentation framework reflecting her individual views regarding a given set of arguments. A question arising in this context is whether the diversity of views observed in such a situation is consistent with the assumption that every individual argumentation framework is induced by a combination of, first, some basic factual information and, second, the personal preferences of the agent concerned. We treat this question of rationalisability of a profile as an algorithmic problem and identify tractable and intractable cases. This is useful for understanding what types of profiles can reasonably be expected to occur in a multiagent system.

Different agents may have different points of view. Following a popular approach in the artificial intelligence literature, this can be modeled by means of different abstract argumentation frameworks, each consisting of a set of arguments the agent is contemplating and a binary attack-relation between them. A question arising in this context is whether the diversity of views observed in such a profile of argumentation frameworks is consistent with the assumption that every individual argumentation framework is induced by a combination of, first, some basic factual attack-relation between the arguments and, second, the personal preferences of the agent concerned regarding the moral or social values the arguments under scrutiny relate to. We treat this question of rationalisability of a profile as an algorithmic problem and identify tractable and intractable cases. In doing so, we distinguish different constraints on admissible rationalisations, e.g., concerning the types of preferences used or the number of distinct values involved. We also distinguish two different semantics for rationalisability, which differ in the assumptions made on how agents treat attacks between arguments they do not report. This research agenda, bringing together ideas from abstract argumentation and social choice, is useful for understanding what types of profiles can reasonably be expected to occur in a multiagent system.

We introduce a new family of judgment aggregation rules, called the binomial rules, designed to account for hidden dependencies between some of the issues being judged. To place them within the landscape of judgment aggregation rules, we analyse both their axiomatic properties and their computational complexity, and we show that they contain both the well-known distance-based rule and the basic rule returning the most frequent overall judgment as special cases. To evaluate the performance of our rules empirically, we apply them to a dataset of crowdsourced judgments regarding the quality of hotels extracted from the travel website TripAdvisor. In our experiments we distinguish between the full dataset and a subset of highly polarised judgments, and we develop a new notion of polarisation for profiles of judgments for this purpose, which may also be of independent interest.

Combinatorial auctions are mechanisms for allocating bundles of goods to agents who each have preferences over these goods. Finding an economically efficient allocation, the so-called winner determination problem, is computationally intractable in the general case, which is why it is important to identify special cases that are tractable but also sufficiently expressive for applications. We introduce a family of auction problems in which the goods on auction can be rearranged into a sequence, and each bid submitted concerns a bundle of goods corresponding to an interval on this sequence, possibly with multiple gaps of bounded length. We investigate the computational complexity of the winner determination problem for such auctions and explore the frontier between tractability and intractability in detail, identifying tractable, intractable, and fixed-parameter tractable cases.

A number of seminal results in the field of social choice theory demonstrate the difficulties of aggregating the preferences of several individual agents for the purpose of making a decision together. We show how to formalise three of the most important impossibility results of this kind—Arrow’s Theorem, Sen’s Theorem, and the Muller–Satterthwaite Theorem—by using a modal logic of social choice functions. We also provide syntactic proofs of these theorems in the same logic. While prior work has been successful in applying tools from logic and automated reasoning to social choice theory, this is the first human-readable formalisation of the Arrovian framework allowing for a direct derivation of the main impossibility theorems of social choice theory. This is useful for gaining a deeper understanding of the foundations of collective decision making, both in human society and in groups of autonomous software agents.

In binary aggregation, each member of a group expresses yes/no choices regarding several correlated issues and we need to decide on a collective choice that accurately reflects the views of the group. A good collective choice will minimise the distance to each of the individual choices, but using such a distance-based aggregation rule is computationally intractable. Instead, we explore a class of low-complexity aggregation rules that select the most representative voter in any given situation and return that voter's choice as the outcome.

We address the problem of specifying a voting rule by means of a series of examples. Each example consists of the answer to a simple question: how should the rule rank two alternatives, given the positions at which each voter ranks the two alternatives? To be able to formalise this elicitation problem, we develop a novel variant of classical social choice theory in terms of associations of alternatives with vectors of ranks rather than the common associations of voters with preference orders. We then define and study a class of voting rules suited for elicitation using such answers. Finally, we propose and experimentally evaluate several elicitation strategies for arriving at a good approximation of the target rule with a reasonable number of queries.

Suppose a number of agents each provide us with a directed graph over a common set of vertices. Graph aggregation is the problem of computing a single “collective” graph that best represents the information inherent in this profile of individual graphs. We consider this aggregation problem from the point of view of social choice theory and ask what properties shared by the individual graphs will transfer to the graph computed by a given aggregation procedure. Our main result is a general impossibility theorem that applies to a wide range of graph properties.

We introduce a general framework for measuring the degree of diversity in the preferences held by the members of a group. We formalise and investigate three specific approaches within that framework: diversity as the range of distinct views held, diversity as aggregate distance between individual views, and diversity as distance of the group's views to a single compromise view. While similarly attractive from an intuitive point of view, the three approaches display significant differences when analysed using both the axiomatic method and empirical studies.

The problem of merging several ontologies has important applications in the Semantic Web, medical ontology engineering and other domains where information from several distinct sources needs to be integrated in a coherent manner. We propose to view ontology merging as a problem of social choice, i.e. as a problem of aggregating the input of a set of individuals into an adequate collective decision. That is, we propose to view ontology merging as ontology aggregation. As a first step in this direction, we formulate several desirable properties for ontology aggregators, we identify the incompatibility of some of these properties, and we define and analyse several simple aggregation procedures. Our approach is closely related to work in judgment aggregation, but with the crucial difference that we adopt an open world assumption, by distinguishing between facts not included in an agent's ontology and facts explicitly negated in an agent's ontology.

We analyse the computational complexity of three problems in judgment aggregation: (1) computing a collective judgment from a profile of individual judgments (the winner determination problem); (2) deciding whether a given agent can influence the outcome of a judgment aggregation procedure in her favour by reporting insincere judgments (the strategic manipulation problem); and (3) deciding whether a given judgment aggregation scenario is guaranteed to result in a logically consistent outcome, independently from what the judgments supplied by the individuals are (the problem of the safety of the agenda). We provide results both for specific aggregation procedures (the quota rules, the premise-based procedure, and a distance-based procedure) and for classes of aggregation procedures characterised in terms of fundamental axioms.

Many collective decision making problems have a combinatorial structure: the agents involved must decide on multiple issues and their preferences over one issue may depend on the choices adopted for some of the others. Voting is an attractive method for making collective decisions, but conducting a multi-issue election is challenging. On the one hand, requiring agents to vote by expressing their preferences over all combinations of issues is computationally infeasible; on the other, decomposing the problem into several elections on smaller sets of issues can lead to paradoxical outcomes. Any pragmatic method for running a multi-issue election will have to balance these two concerns. We identify and analyse the problem of generating an agenda for a given election, specifying which issues to vote on together in local elections and in which order to schedule those local elections.

We investigate the problem of influencing the preferences of players within a Boolean game so that, if all players act rationally, certain desirable outcomes will result. The way in which we influence preferences is by overlaying games with taxation schemes. In a Boolean game, each player has unique control of a set of Boolean variables, and the choices available to the player correspond to the possible assignments that may be made to these variables. Each player also has a goal, represented by a Boolean formula, that they desire to see satisfied. Whether or not a player’s goal is satisfied will depend both on their own choices and on the choices of others, which gives Boolean games their strategic character. We extend this basic framework by introducing an external principal who is able to levy a taxation scheme on the game, which imposes a cost on every possible action that a player can choose. By designing a taxation scheme appropriately, it is possible to perturb the preferences of the players, so that they are incentivised to choose some equilibrium that would not otherwise be chosen. After motivating and formally presenting our model, we explore some issues surrounding it, including the complexity of finding a taxation scheme that implements some socially desirable outcome, and then discuss desirable properties of taxation schemes.

Binary aggregation studies problems in which individuals express yes/no choices over a number of possibly correlated issues, and these individual choices need to be aggregated into a collective choice. We show how several classical frameworks of Social Choice Theory, particularly preference and judgment aggregation, can be viewed as binary aggregation problems by designing an appropriate set of integrity constraints for each specific setting. We explore the generality of this framework, showing that it makes available useful techniques both to prove theoretical results, such as a new impossibility theorem in preference aggregation, and to analyse practical problems, such as the characterisation of safe agendas in judgment aggregation in a syntactic way. The framework also allows us to formulate a general definition of paradox that is independent of the domain under consideration, which gives rise to the study of the class of aggregation procedures of generalised dictatorships.

We present a method for using standard techniques from satisfiability checking to automatically verify and discover theorems in an area of economic theory known as ranking sets of objects. The key question in this area, which has important applications in social choice theory and decision making under uncertainty, is how to extend an agent's preferences over a number of objects to a preference relation over nonempty sets of such objects. Certain combinations of seemingly natural principles for this kind of preference extension can result in logical inconsistencies, which has led to a number of important impossibility theorems. We first prove a general result that shows that for a wide range of such principles, characterised by their syntactic form when expressed in a many-sorted first-order logic, any impossibility exhibited at a fixed (small) domain size will necessarily extend to the general case. We then show how to formulate candidates for impossibility theorems at a fixed domain size in propositional logic, which in turn enables us to automatically search for (general) impossibility theorems using a SAT solver. When applied to a space of 20 principles for preference extension familiar from the literature, this method yields a total of 84 impossibility theorems, including both known and nontrivial new results.

We consider problems where several individuals each need to make a yes/no choice regarding a number of issues and these choices then need to be aggregated into a collective choice. Depending on the application at hand, different combinations of yes/no may be considered rational. We can describe such rationality assumptions in terms of a propositional formula. The question then arises whether or not a given aggregation procedure will lift the rationality assumptions from the individual to the collective level, i.e., whether the collective choice will be rational whenever all individual choices are. To address this question, for each of a number of simple fragments of the language of propositional logic, we provide an axiomatic characterisation of the class of aggregation procedures that will lift all rationality assumptions expressible in that fragment.

We study the problem of fairly dividing a set of goods amongst a group of agents, when those agents have preferences that are ordinal relations over alternative bundles of goods (rather than utility functions) and when our knowledge of those preferences is incomplete. The incompleteness of the preferences stems from the fact that each agent reports their preferences by means of an expression of bounded size in a compact preference representation language. Specifically, we assume that each agent only provides a ranking of individual goods (rather than of bundles). In this context, we consider the algorithmic problem of deciding whether there exists an allocation that is possibly (or necessarily) envy-free, given the incomplete preference information available, if in addition some mild economic efficiency criteria need to be satisfied. We provide simple characterisations, giving rise to simple algorithms, for some instances of the problem, and computational complexity results, establishing the intractability of the problem, for others.

We show how to embed a framework for multilateral negotiation, in which a group of agents implement a sequence of deals concerning the exchange of a number of resources, into linear logic. In this model, multisets of goods, allocations of resources, preferences of agents, and deals are all modelled as formulas of linear logic. Whether or not a proposed deal is rational, given the preferences of the agents concerned, reduces to a question of provability, as does the question of whether there exists a sequence of deals leading to an allocation with certain desirable properties, such as maximising social welfare. Thus, linear logic provides a formal basis for modelling convergence properties in distributed resource allocation.

We investigate the properties of an abstract negotiation framework where agents autonomously negotiate over allocations of indivisible resources. In this framework, reaching an allocation that is optimal may require very complex multilateral deals. Therefore, we are interested in identifying classes of valuation functions such that any negotiation conducted by means of deals involving only a single resource at a time is bound to converge to an optimal allocation whenever all agents model their preferences using these functions. In the case of negotiation with monetary side payments amongst self-interested but myopic agents, the class of modular valuation functions turns out to be such a class. That is, modularity is a sufficient condition for convergence in this framework. We also show that modularity is not a necessary condition. Indeed, there can be no condition on individual valuation functions that would be both necessary and sufficient in this sense. Evaluating conditions formulated with respect to the whole profile of valuation functions used by the agents in the system would be possible in theory, but turns out to be computationally intractable in practice. Our main result shows that the class of modular functions is maximal in the sense that no strictly larger class of valuation functions would still guarantee an optimal outcome of negotiation, even when we permit more general bilateral deals. We also establish similar results in the context of negotiation without side payments.

Abstract We present the CIFF proof procedure for abductive logic programming with constraints, and we prove its correctness. CIFF is an extension of the IFF proof procedure for abductive logic programming, relaxing the original restrictions over variable quantification (allowedness conditions) and incorporating a constraint solver to deal with numerical constraints as in constraint logic programming. Finally, we describe the CIFF system, comparing it with state-of-the-art abductive systems and answer set solvers and showing how to use it to program some applications.

A classical result in voting theory, the Gibbard-Satterthwaite Theorem, states that for any non-dictatorial voting rule for choosing between three or more candidates, there will be situations that give voters an incentive to manipulate by not reporting their true preferences. However, this theorem does not immediately apply to all voting rules that are used in practice. For instance, it makes the implicit assumption that there is a unique way of casting a sincere vote, for any given preference ordering over candidates. Approval voting is an important voting rule that does not satisfy this condition. In approval voting, a ballot consists of the names of any subset of the set of candidates standing; these are the candidates the voter approves of. The candidate receiving the most approvals wins. A ballot is considered sincere if the voter prefers any of the approved candidates over any of the disapproved candidates. In this paper, we explore to what extent the presence of multiple sincere ballots allows us to circumvent the Gibbard-Satterthwaite Theorem. Our results show that there are several interesting settings in which no voter will have an incentive not to vote by means of some sincere ballot. 1

A multiagent system may be thought of as an artificial society of autonomous software agents and we can apply concepts borrowed from welfare economics and social choice theory to assess the social welfare of such an agent society. In this paper, we study an abstract negotiation framework where agents can agree on multilateral deals to exchange bundles of indivisible resources. We then analyse how these deals affect social welfare for different instances of the basic framework and different interpretations of the concept of social welfare itself. In particular, we show how certain classes of deals are both sufficient and necessary to guarantee that a socially optimal allocation of resources will be reached eventually.