Improve translation to clauses

[rkaminsk]

The current translation for sum constraints only makes sense with two variables. With more variables, auxiliary variables for intermediate results should be introduced.

I believe clingcon 3 had a similar translation.

Consider the constraint x+y+z <= 1 where all variables have domain [0,1]. The term x+y can take value 1 if x=0 and y=1 or x=1 and y=0. We get the clauses:

• x<=0 & y<=1 => z<=0, and
• x<=1 & y<=0 => z<=0.

We can avoid this by introducing an auxiliary variable for the prefix. It is probably best to detect such prefixes and introduce the required Boolean variables during the translation to clauses. It could also be done introducing auxiliary integer variables but this has the disadvantage that we would have to be very careful to stay within the bounds of the minimum/maximum integer.

[MaxOstrowski]

In old clingcon integer variables are introduced (constraints can be split into smaller ones). But for longer constraints a propagator is still more efficient.