Boosting domain filtering over floating-point numbers with safe linear approximations

Mohammed Said Belaid 1 Claude Michel 1 Michel Rueher 1, *
* Auteur correspondant
1 Laboratoire d'Informatique, Signaux, et Systèmes de Sophia-Antipolis (I3S) / Equipe CEP
Laboratoire I3S - MDSC - Modèles Discrets pour les Systèmes Complexes
Abstract : Solving constraints over floating-point numbers is a critical issue in numerous applications notably in program verification. Capabilities of filtering algorithms for constraints over the floating-point numbers have been so far limited to 2b-consistency and its derivatives. Though safe, such filtering techniques suffer from the well known pathological problems of local consistencies, e.g., inability to efficiently handle mul- tiple occurrences of the variables. These limitations also take roots in the strongly restricted floating-point arithmetic. To circumvent the poor properties of floating-point arithmetic, we propose in this paper to build various relaxations over the reals of the problem over the floats. We show that using linear programming (LP) to shrink the domains with safe linearisations of such relaxations can be very effective for boosting filtering techniques for constraints over the floats. Preliminary experiments on a limited but relevant set of benchmarks are very promising.
Type de document :
Pré-publication, Document de travail
2011
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00653659
Contributeur : Michel Rueher <>
Soumis le : lundi 19 décembre 2011 - 22:45:12
Dernière modification le : lundi 5 novembre 2018 - 15:48:02
Document(s) archivé(s) le : vendredi 16 novembre 2012 - 16:05:27

Fichier

cpaior2012.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00653659, version 1

Collections

Citation

Mohammed Said Belaid, Claude Michel, Michel Rueher. Boosting domain filtering over floating-point numbers with safe linear approximations. 2011. 〈hal-00653659〉

Partager

Métriques

Consultations de la notice

219

Téléchargements de fichiers

150