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 [xn,...,x0]”. 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 xi, i ∈ 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.