Linear aggregation can make propagation less effective

[matsc-at-sics-se]

Consider this silly model:

include "globals.mzn";

array[1..8] of var 1..8: x;

var int: sum1 = sum(x[1..4]);
var int: rawsum2 = sum(x[5..8]);
% var int: sum2 = min(10,rawsum2); % failures=88 with this line; rawsum2 in .fzn
var int: sum2 = rawsum2;       % failures=293 with this line; no rawsum2 in .fzn

constraint rawsum2 <= 10;

constraint alldifferent(x);

solve maximize sum1 + sum2;

If I run it with minizinc -s silly.mzn, it runs with 293 failures. If I uncomment the first sum2 line and comment the second one, it runs with 88 failures. The failures occur during proof of optimality. The difference is unexpected, because how can rawsum2 be any different from min(10,rawsum2) in the context of rawsum2 <= 10?

If I look into the .fzn, I see a variable rawsum2 in the 88 failures version, but no such variable in the 293 failures version.

Second-guessing what the flattener does in the 293 failures version: I guess it eliminates rawsum2 and replaces its occurrences by sum(x[5..8]). But that makes the constraint rawsum2 <= 10 less effective, because it no longer prunes a single variable.

I observed this phenomenon in a larger model and came up with a similar work-around. The reduction in number of failures was quite dramatic. Perhaps you want to want to perform variable elimination (if that is what you do) more selectively.

[Dekker1]

Generally the MiniZinc compiler will try to aggregate linear expressions. When you write sum(x) <= 10 the compiler will create a single int_lin_le constraint instead of a sum/int_lin_eq constraint and an int_le constraint. The idea of this is that the solver can then choose it's best approach to handle the constraint (and we avoid creating the sum variable in general). In Gecode, this constraint is handled directly.

In the case of min(10, sum(x), the compiler knows that the value sum(x) is used both in the min constraint and in a linear constraint and it does not aggregate the sum into a single linear expression.

You are probably more of an expert in explaining why having the sum variable helps the propagation of the problem, but it could be caused by the sum occurring in both the constraint and the objective function and it seems that this is not shared when both are aggregated.

The decision of when to aggregate linear expressions is a hard one, since for mathematical solvers its crucial, but it can hurt in some scenarios for CP solvers (although not aggregating at all also seems a bad idea). Solvers that do better without the aggregation can always redefine int_lin_eq and int_lin_le.

Currently the best option is to optimise the aggregation behaviour yourself when it is known to benefit from (partial) sum variables. I believe we had a general rule that when a variable is named it would stop aggregation, but that does not seem the case here. Maybe Guido can shine more light on the exact rules for aggregation.

[matsc-at-sics-se]

I wrote the issue from the perspective not of a solver implementor, but of a CP modeller. From the modeller's perspective, I find the behavior unexpected and nontrivial to work around. I guess this phenomenon can surface in minimization problems in cases where you want to provide good lower bounds on the objective or its subterms.

Mats Carlsson, Ph.D.

Associate Professor

Digital Systems

Department Computer Science

Unit Computer Systems

D: +46 10 228 43 16 |  M: +46 70 264 71 80

[email protected]mailto:[email protected]

RISE Research Institutes of Sweden | ri.sehttp://ri.se

 |

---

Från: Jip J. Dekker [email protected] Skickat: den 21 juli 2020 15:24 Till: MiniZinc/libminizinc [email protected] Kopia: Mats Carlsson [email protected]; Author [email protected] Ämne: Re: [MiniZinc/libminizinc] variable elimination can make propagation less effective (#400)

Generally the MiniZinc compiler will try to aggregate linear expressions. When you write sum(x) <= 10 the compiler will create a single int_lin_le constraint instead of a sum/int_lin_eq constraint and an int_le constraint. The idea of this is that the solver can then choose it's best approach to handle the constraint (and we avoid creating the sum variable in general). In Gecode, this constraint is handled directly.

In the case of min(10, sum(x), the compiler knows that the value sum(x) is used both in the min constraint and in a linear constraint and it does not aggregate the sum into a single linear expression.

You are probably more of an expert in explaining why having the sum variable helps the propagation of the problem, but it could be caused by the sum occurring in both the constraint and the objective function and it seems that this is not shared when both are aggregated.

The decision of when to aggregate linear expressions is a hard one, since for mathematical solvers its crucial, but it can hurt in some scenarios for CP solvers (although not aggregating at all also seems a bad idea). Solvers that do better without the aggregation can always redefine int_lin_eq and int_lin_le.

Currently the best option is to optimise the aggregation behaviour yourself when it is known to benefit from (partial) sum variables. I believe we had a general rule that when a variable is named it would stop aggregation, but that does not seem the case here. Maybe Guido can shine more light on the exact rules for aggregation.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHubhttps://github.com/MiniZinc/libminizinc/issues/400#issuecomment-661859284, or unsubscribehttps://github.com/notifications/unsubscribe-auth/ACTJ26TBSQHMGD5RXUVUUL3R4WJJJANCNFSM4PDSDGHA.