A redundant constraint makes explicit a property that satisfies a solution implicitly. In fact, in some disciplines, redundant constraints are known as implicit constraints for that reason. Such a constraint should not change the nature of the solution, but its propagation should delimit the general shape of the solution more quickly.

Of course, there is no need to express grossly obvious redundancy since the highly optimized algorithms that Solver uses to insure arc consistency already work well enough. For example, if we are given this system of equations:

x = y + z

z = a + b

we gain no efficiency whatsoever by adding this constraint:

x = y + a + b

However, in any case where an implicit property makes good sense, or derives from experience, or satisfies formal computations, its explicit implementation as a redundant constraint can be beneficial.