• Funding : Artois, Région HdF

In combinatorial problems, one can either look for a solution or a solution which optimize one or multiple criteria. In itinerary search for instance, one does not look for any itinerary between a source and a destination, but one minimizing the distance, the cost, or the number of direction changes for instance. In the first case, we talk about a satisfaction problem, while in the second case we talk about an optimization problem. When the variables have boolean domains, there are two main optimization problems: Pseudo-Boolean Optimization (PBO) and Maximum SATisfiability (MAXSAT). One of the consequences of the increase in automated decision making is the requirement to explain the decision taken. The aim of this thesis is to study explanation mechanisms for solutions given by boolean optimization engines, i.e. PBO and MAXSAT solvers. We especially care about the ability to explain on demand the solution provided by such solvers. Ideally, the explanation process should be as independent as possible from the solver, in the spirit of prior work on independent unsatisfiability checking.