Un solveur de contraintes basé sur les domaines abstraits

Autor: Pelleau, Marie, Miné, Antoine, Truchet, Charlotte, Benhamou, Frédéric
Přispěvatelé: Theory, Algorithms and Systems for Constraints (TASC), Laboratoire d'Informatique de Nantes Atlantique (LINA), Mines Nantes (Mines Nantes)-Université de Nantes (UN)-Centre National de la Recherche Scientifique (CNRS)-Mines Nantes (Mines Nantes)-Université de Nantes (UN)-Centre National de la Recherche Scientifique (CNRS)-Département informatique - EMN, Mines Nantes (Mines Nantes)-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire d'informatique de l'école normale supérieure (LIENS), École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS), Abstract Interpretation and Static Analysis (ABSTRACTION), Département d'informatique de l'École normale supérieure (DI-ENS), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Mines Nantes (Mines Nantes)-Université de Nantes (UN)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS)-Mines Nantes (Mines Nantes)-Université de Nantes (UN)-Centre National de la Recherche Scientifique (CNRS)-Mines Nantes (Mines Nantes)-Université de Nantes (UN)-Département informatique - EMN, Département d'informatique - ENS Paris (DI-ENS), Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Inria Paris-Rocquencourt, Centre National de la Recherche Scientifique (CNRS)-Mines Nantes (Mines Nantes)-Université de Nantes (UN), École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)
Jazyk: francouzština
Rok vydání: 2013
Předmět:
Zdroj: 9èmes Journées Francophones de Programmation par Contraintes
9èmes Journées Francophones de Programmation par Contraintes, Jun 2013, Aix-en-Provence, France. pp.259-268
Popis: International audience; Dans cet article, nous utilisons des techniques de l'interpréation abstraite (une théorie d'approximation des sémantiques) dans le cadre de la programmation par contraintes (basée sur la logique du premier ordre qui permet de résoudre des problèmes combinatoires). Nous mettons en évidence certains liens et différences entre ces domaines de recherches : tous deux calculent itérativement des points fixes mais emploient des extrapolations et stratégies de raffinement différentes. De plus, nous pouvons mettre en correspondance les consistances en programmation par contraintes et les domaines abstraits non relationnels. Nous utilisons ensuite ces correspondances pour construire un solveur de contraintes abstrait qui s'appuie sur des techniques d'interprétation abstraite (comme les domaines relationnels) pour aller au-delà des solveurs classiques. Les résultats expérimentaux obtenus avec notre prototype sont encourageants.
Databáze: OpenAIRE
Externí odkaz: