The bit-vector Constraint

Some applications require to reason on particular bits of an integer value, and to express the fact that “the number X is encoded in binary by the vector of Boolean variables [x_n, …, x₀]”. The natural way to encode this is using a linear constraint. We show that bound propagation on this constraint has intriguing properties: it is complete in the sense that the bounds of the variable x_i (i in 0 .. n) are tightly reduced; on the other hand, the interval of values for X is in general not optimally reduced: it can be up to twice as large as the optimal. We show that a simple mechanism allows the reasoning to be complete on X.