• PhD Student:
  • Anthony Blomme
  • Funding : Artois, Région HdF
  • PhD defended on :
  • Dec 18, 2023

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.

Some references

[1] Raymond Reiter, Johan de Kleer: Foundations of Assumption-based Truth Maintenance Systems: Preliminary Report. AAAI 1987: 183-189

[2] Narendra Jussien. e-constraints: explanation-based constraint programming. In CP01 Workshop on User-Interaction in Constraint Satisfaction, Paphos, Cyprus, 1 December 2001.

[3] Didier Dubois, Daniel Le Berre, Henri Prade, Régis Sabbadin: Using Possibilistic Logic for Modeling Qualitative Decision: ATMS-based Algorithms. Fundam. Inform. 37(1-2): 1-30 (1999)

[4] Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler: Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Softw. Test., Verif. Reliab. 24(8): 593-607 (2014)