Langues : English français
Accueil > Manifestations > Thèses et HDR > Thèses > Marie Pelleau

Marie Pelleau

Directeur de thèse

Frédéric Benhamou
Pascal van Hentenryck
Charlotte Truchet

Résumé

La programmation par contraintes permet de formaliser et résoudre des problèmes fortement combinatoires, dont le temps de calcul évolue en pratique exponentiellement. Les méthodes développées aujourd’hui résolvent efficacement de nombreux problèmes industriels de grande taille dans des solveurs génériques. Cependant, les solveurs restent dédiés à un seul type de variables : réelles ou entières, et résoudre des problèmes mixtes discrets-continus suppose des transformations ad hoc.

Dans un autre domaine, l’interprétation abstraite permet de prouver des propriétés sur des programmes, en étudiant une abstraction de leur sémantique concrète, constituée des traces des variables au cours d’une exécution. Plusieurs représentations de ces abstractions, appelées domaines abstraits, ont été proposées. Traitées de façon générique dans les analyseurs, elles peuvent mélanger les types entiers, réels et booléens, ou encore représenter des relations entre variables.

Dans cette thèse, nous définissons des domaines abstraits pour la programmation par contraintes, afin de construire une méthode de résolution traitant indifféremment les entiers et les réels. Cette généralisation permet d’intégrer à la programmation par contraintes des domaines relationnels, comme les octogones déjà utilisés en interprétation abstraite. En exploitant l’information spécifique aux octogones pour guider la recherche de solutions, nous obtenons de bonnes performances sur les problèmes continus. Dans un deuxième temps, nous définissons une méthode générique de résolution de contraintes, avec des outils d’interprétation abstraite, pour intégrer les domaines abstraits existants. Notre prototype, AbSolute, peut ainsi résoudre des problèmes mixtes et utiliser les domaines relationnels implémentés.

Mots-clés : Programmation par contraintes, Interprétation abstraite, Domaine abstrait, Octogone, Continu-discret.

Abstract

Abstract Domains in Constraint Programming

Constraint Programming aims at solving hard combinatorial problems, with a computation time increasing in practice exponentially. The methods are today efficient enough to solve large industrial problems, in a generic framework. However, solvers are dedicated to a single variable type : integer or real. Solving mixed problems relies on ad hoc transformations.

In another field, Abstract Interpretation offers tools to prove program properties, by studying an abstraction of their concrete semantics, that is, the set of possible values of the variables during an execution. Various representations for these abstractions have been proposed. They are called abstract domains. Abstract domains can mix any type of variables, and even represent relations between the variables.

In this Ph.D., we define abstract domains for Constraint Programming, so as to build a generic solving method, dealing with both integer and real variables. We can also study the octagons abstract domain, already defined in Abstract Interpretation. Guiding the search by the octagonal relations, we obtain good results on a continuous benchmark. In a second part, we define a solving method using Abstract Interpretation techniques, in order to include existing abstract domains. Our solver, AbSolute, is able to solve mixed problems and use relational domains.

Keywords : Constraint Programming, Abstract Interpretation, Abstract Domain, Octagon, Continuous-Discrete.

Composition du jury

  • Pedro Barahona, Professeur, Universidade Nova de Lisboa (rapporteur)
  • Xavier Rival, Chargé de recherche, INRIA - École Normale Supérieure (rapporteur)
  • Benoit Baudry, Chargé de recherche, INRIA - IRISA (examinateur)
  • Frédéric Benhamou, Professeur, Université de Nantes (directeur de thèse)
  • Pascal van Hentenryck, Professeur, University of Melbourne (co-directeur de thèse)
  • Charlotte Truchet, Maître de conférences, Université de Nantes (co-encadrante de thèse)

Dernière modification : lundi 7 janvier 2013