Abstract Domains in Constraint Programming
Domaines abstraits en programmation par contraintes
Résumé
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 PhD dissertation, 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 our 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.
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’étudier 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 notre méthode générique 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.
Origine : Fichiers produits par l'(les) auteur(s)