Un nouvel algorithme de consistance locale sur les nombres flottants

Mohammed Said Belaid 1 Claude Michel 1 Michel Rueher 1
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 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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-00829579
Contributor : Ist Inria Saclay <>
Submitted on : Monday, June 3, 2013 - 3:03:13 PM
Last modification on : Monday, November 5, 2018 - 3:48:02 PM
Document(s) archivé(s) le : Wednesday, September 4, 2013 - 4:13:48 AM

File

paper_32.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00829579, version 1

Collections

Citation

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. 2012, Actes des Huitièmes Journées Francophones de Programmation par Contraintes. 〈hal-00829579〉

Share

Metrics

Record views

169

Files downloads

234