Justification of Matching Outcomes Daniela Loustalot Knapp Abstract: This thesis is dedicated to the study of justifications of partial matching outcomes for one-to-one matching problems with two-sided preferences. Matching theory studies the problem of pairing agents from two groups while taking into account their preferences. The idea is to provide non-experts with a step-by-step explanation of why the computed assignment is a good compromise between all the agents’ preferences, grounded in a set of principles that are appealing to them. The contribution of this thesis is twofold. Firstly, we define a formal model for justifications. A justification consists of a normative basis together with a step-by-step explanation grounded in the basis and the agents’ preferences. Secondly, we show how to automate the search for justifications using SAT solvers. We formally define a procedure to find a justification for a specific problem whenever one exists. We transform the problem of finding a normative basis into a propositional satisfiability problem, so that it can be solved automatically by a SAT solver and we show how to extract an explanation from a minimal unsatisfiable subset. Finally, we present an implementation in Python and some examples of interesting executions.