Automated Justification of Collective Decisions via Constraint Solving

Given the preferences of several agents over a set of alternatives,there may be competing views on which of the alternatives would be the “best” compromise. We propose a formal model, grounded in social choice theory, for providing a justification for a given choice in the context of a given corpus of basic normative principles (so-called axioms) on which to base any possible step-by-step explanation for why a given target outcome has been or should be selected in a given situation. Thus, our notion of justification has both an explanatory and a normative component. We also develop an algorithm for computing such justifications that exploits the analogy between the notion of explanation and the concept of minimal unsatisfiable subset used in constraint programming. Finally,we report on an application of a proof-of-concept implementation of our approach to run an experimental study of the explanatory power of several axioms proposed in the social choice literature.