Boosting local consistency algorithms over oating-point numbers

Description

Solving constraints over oating-point numbers is a critical issue in numerous applications notably in program verication. Capa-bilities of ltering algorithms over the oating-point numbers (F) have been so far limited to 2b-consistency and its derivatives. Though safe, such ltering techniques suer from the well known pathological prob-lems of local consistencies, e.g., inability to eciently handle multiple occurrences of the variables. These limitations also have their origins 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, called FPLP, which relies on various relaxations over the real numbers of the problem over F. 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 promising and show that this approach can be eective for boosting local consistency algorithms over F.

Abstract

International audience

Additional details