Un nouvel algorithme de consistance locale sur les nombres flottants - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

Un nouvel algorithme de consistance locale sur les nombres flottants

Résumé

Solving constraints over oating-point numbers is a critical issue in numerous applications notably in program veri cation. Capabilities of ltering algorithms over the oating-point numbers have been so far limited to 2b-consistency and its derivatives. Though safe, such ltering techniques su er from the well known pathological problems of local consistencies, e.g., inability to e ciently handle multiple occurrences of the variables. These limitations also take roots in the strongly restricted oating-point arithmetic. To circumvent the poor properties of oating-point arithmetic, we propose in this paper a new ltering algorithm which relies on various relaxations over the reals of the problem over the oats. Safe bounds of the domains are computed with a mixed integer linear programming solver (MILP) on safe linearizations of these relaxations. Preliminary experiments on a relevant set of benchmarks are very promising and show that this approach can be very effective for boosting local consistency algorithms over the floats.
La résolution de contraintes sur les nombres a virgule flottante soulève des problèmes critiques dans de nombreuses applications, notamment en vérification de programmes. Jusqu'à maintenant, les algorithmes de filtrage sur les nombres à virgule flottante ont été limités a la 2B{consistance et ses dérivées. Bien que ces filtrages soient conservatifs des solutions, ils souffrent des problèmes bien connus des consistances locales, e.g., leur incapacité à traiter efficacement les occurrences multiples de variables. Leurs limitations proviennent aussi de la pauvret e des propriétés de l'arithmétique des nombres à virgule flottante. Afin de pallier à ces limitations, nous proposons dans cet article un nouvel algorithme de filtrage de contraintes sur les flottants qui repose sur des relaxations successives sur les réels du problème initial sur les flottants. Des bornes conservatives des domaines sont obtenues à l'aide d'un solveur de programme linéaire mixte (MILP) appliquées à des linéarisations conservatives de ces relaxations. Les résultats préliminaires sont prometteurs et montrent que cette approche peut effectivement accélérer les filtrages par consistances locales.
Fichier principal
Vignette du fichier
paper_32.pdf (182.51 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00829579 , version 1 (03-06-2013)

Identifiants

  • HAL Id : hal-00829579 , version 1

Citer

Mohammed Said Belaid, Claude Michel, Michel Rueher. Un nouvel algorithme de consistance locale sur les nombres flottants. Huitièmes Journées Francophones de Programmation par Contraintes - JFPC 2012, May 2012, Toulouse, France. ⟨hal-00829579⟩
106 Consultations
146 Téléchargements

Partager

Gmail Facebook X LinkedIn More