Optimisation booléenne multiobjectif : complexité sous contraintes compilées et résolution via SAT
- Doctorant:
- Emmanuel Lonca
- Co-directeur(s) de thèse :
- Daniel Le Berre
- Pierre Marquis
- Co-encadrant(s) de thèse :
- Anne Parrain
- Financement : Artois
- Thèse soutenue le :
- 26 juin 2015
- •
- Salle des thèses
L’aide à la décision a pour but d’assister un opérateur humain dans ses choix. La nécessité d’employer de telles techniques s’est imposée avec la volonté de traiter des problèmes dépendant d’une quantité de données toujours plus importante.
L’intérêt de l’aide à la décision est encore plus manifeste lorsqu’on souhaite obtenir non pas une solution quelconque, mais une des meilleures solutions d’un problème combinatoire selon un critère donné. On passe alors d’un problème de décision (déterminer l’existence d’une solution) à un problème d’optimisation monocritère (déterminer une des meilleures solutions possibles selon un critère). Un décideur peut aussi souhaiter considérer plusieurs critères, et ainsi faire passer le problème de décision initial à un problème d’optimisation multicritère. La difficulté de ce type de problèmes provient du fait que les critères considérés sont généralement antagonistes, et qu’il n’existe donc pas de solution meilleure que les autres pour l’ensemble des critères. Dans ce cas, il s’agit plutôt de déterminer une solution qui offre un bon compromis entre les critères.
Dans cette thèse, nous étudions dans un premier temps la complexité théorique de tâches d’optimisation complexes sur les langages de la logique propositionnelle, puis nous étudions leur résolution pratique via le recours à des logiciels bâtis pour résoudre de manière efficace en pratique des problèmes de décision combinatoires, les prouveurs SAT.