MiniZinc
Flattening of count_{leq, lt, geq, gt} is broken
The flattening of count_{leq, lt, geq, gt} is broken. For example:
include "count.mzn";
array [1..3] of var 1..10: x;
var 1..10: y;
var 1..3: c;
constraint count(x, y) <= c;
gets compiled by MiniZinc 2.6.4 to
predicate int_lin_ne_imp(array [int] of int: as,array [int] of var int: bs,int: c,var bool: r);
array [1..2] of int: X_INTRODUCED_3_ = [1,-1];
array [1..4] of int: X_INTRODUCED_14_ = [-1,-1,-1,-1];
var 1..10: X_INTRODUCED_0_;
var 1..10: X_INTRODUCED_1_;
var 1..10: X_INTRODUCED_2_;
var 1..10: y:: output_var;
var 1..3: c:: output_var;
var bool: X_INTRODUCED_4_ ::var_is_introduced :: is_defined_var;
var bool: X_INTRODUCED_5_ ::var_is_introduced :: is_defined_var;
var bool: X_INTRODUCED_6_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_8_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_9_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_10_ ::var_is_introduced :: is_defined_var;
array [1..3] of var int: x:: output_array([1..3]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_];
constraint int_lin_le(X_INTRODUCED_14_,[X_INTRODUCED_8_,X_INTRODUCED_9_,X_INTRODUCED_10_,c],-3);
constraint int_lin_ne_imp(X_INTRODUCED_3_,[X_INTRODUCED_0_,y],0,X_INTRODUCED_4_):: defines_var(X_INTRODUCED_4_);
constraint int_lin_ne_imp(X_INTRODUCED_3_,[X_INTRODUCED_1_,y],0,X_INTRODUCED_5_):: defines_var(X_INTRODUCED_5_);
constraint int_lin_ne_imp(X_INTRODUCED_3_,[X_INTRODUCED_2_,y],0,X_INTRODUCED_6_):: defines_var(X_INTRODUCED_6_);
constraint bool2int(X_INTRODUCED_4_,X_INTRODUCED_8_):: defines_var(X_INTRODUCED_8_);
constraint bool2int(X_INTRODUCED_5_,X_INTRODUCED_9_):: defines_var(X_INTRODUCED_9_);
constraint bool2int(X_INTRODUCED_6_,X_INTRODUCED_10_):: defines_var(X_INTRODUCED_10_);
solve satisfy;
Expected output (produced by MiniZinc 2.5.5):
predicate fzn_count_eq(array [int] of var int: x,var int: y,var int: c);
array [1..2] of int: X_INTRODUCED_4_ = [1,-1];
var 1..10: X_INTRODUCED_0_;
var 1..10: X_INTRODUCED_1_;
var 1..10: X_INTRODUCED_2_;
var 1..10: y:: output_var;
var 1..3: c:: output_var;
var 0..3: X_INTRODUCED_3_ ::var_is_introduced :: is_defined_var;
array [1..3] of var int: x:: output_array([1..3]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_];
constraint fzn_count_eq(x,y,X_INTRODUCED_3_):: defines_var(X_INTRODUCED_3_);
constraint int_lin_le(X_INTRODUCED_4_,[X_INTRODUCED_3_,c],0);
solve satisfy;
I think the issue was introduced by this commit:
commit ce350a29a6208bfd22655ea3771a13abc1a84a73
Author: Jip J. Dekker <[email protected]>
Date: Thu Feb 18 14:38:22 2021 +1100
Add initial promised context annotations
diff --git a/share/minizinc/std/fzn_count_leq.mzn b/share/minizinc/std/fzn_count_leq.mzn
index b72b435f..1d06518c 100644
--- a/share/minizinc/std/fzn_count_leq.mzn
+++ b/share/minizinc/std/fzn_count_leq.mzn
@@ -1,7 +1,7 @@
include "count_fn.mzn";
predicate fzn_count_leq(array[int] of var int: x, var int: y, var int: c) =
- let { var int: z = count(x,y) } in z >= c;
+ let { var int: z ::promise_ctx_monotone = count(xi in x)(xi == y); } in z >= c;
% This needs to be written with a let rather than count(x,y) >= c
% so that the automatic rewriting of the latter doesn't kick in
Thanks for finding this. This might actually affect the outcome of this years competition...
Looking at the actual call trace it appear you have located the right commit, but the wrong predicate. fzn_count_leq seems to function fine.
It is fzn_count_geq that this model get rewritten to, and there we have made a more drastic change. Since the leq and geq versions of the count predicates never have to ensure an actual count, the fzn_count_geq was changed to push negations inward, to improve the number of positive context. It now thus counts how many values are not equal to y rather than the other way around:
% TODO: This is probably the better way to do this, but still always gives
% reifications (instead of half-reifications)
% let {
% var int: z ::promise_ctx_antitone = count(xi in x)(xi == y);
% } in z <= c;
let {
var int: z ::promise_ctx_monotone = count(xi in x)(xi != y);
} in z >= (length(x) - c);
Looking at my TODO this was always meant to be a temporary workaround, that wasn't expected to have any real negative impact (and a positive impact on all solvers supporting half-reified equality predicates). When a fzn_count_eq predicate is available, it does of course seem like a much better idea to ensure that they get used.
I will look into this issue further to try and find the best solution.
Ah, you are right, the comparison in my example translates to fzn_count_geq.
Still, the other variants of count are broken, too. For example,
include "count.mzn";
array [1..3] of var 1..10: x;
var 1..10: y;
var 1..3: c;
constraint count(x, y) >= c;
compiles to:
array [1..4] of int: X_INTRODUCED_11_ = [-1,-1,-1,1];
var 1..10: X_INTRODUCED_0_;
var 1..10: X_INTRODUCED_1_;
var 1..10: X_INTRODUCED_2_;
var 1..10: y:: output_var;
var 1..3: c:: output_var;
var bool: X_INTRODUCED_3_ ::var_is_introduced :: is_defined_var;
var bool: X_INTRODUCED_4_ ::var_is_introduced :: is_defined_var;
var bool: X_INTRODUCED_5_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_7_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_8_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_9_ ::var_is_introduced :: is_defined_var;
array [1..3] of var int: x:: output_array([1..3]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_];
constraint int_lin_le(X_INTRODUCED_11_,[X_INTRODUCED_7_,X_INTRODUCED_8_,X_INTRODUCED_9_,c],0);
constraint int_eq_reif(X_INTRODUCED_0_,y,X_INTRODUCED_3_):: defines_var(X_INTRODUCED_3_);
constraint int_eq_reif(X_INTRODUCED_1_,y,X_INTRODUCED_4_):: defines_var(X_INTRODUCED_4_);
constraint int_eq_reif(X_INTRODUCED_2_,y,X_INTRODUCED_5_):: defines_var(X_INTRODUCED_5_);
constraint bool2int(X_INTRODUCED_3_,X_INTRODUCED_7_):: defines_var(X_INTRODUCED_7_);
constraint bool2int(X_INTRODUCED_4_,X_INTRODUCED_8_):: defines_var(X_INTRODUCED_8_);
constraint bool2int(X_INTRODUCED_5_,X_INTRODUCED_9_):: defines_var(X_INTRODUCED_9_);
solve satisfy;
In 2.6.4, fzn_count_leq is defined as follows:
predicate fzn_count_leq(array[int] of var int: x, var int: y, var int: c) =
let { var int: z ::promise_ctx_monotone = count(xi in x)(xi == y); } in z >= c;
% This needs to be written with a let rather than count(x,y) >= c
% so that the automatic rewriting of the latter doesn't kick in
So it seems that the expected rewriting from var int: z ::promise_ctx_monotone = count(xi in x)(xi == y); to var int: z ::promise_ctx_monotone = count(x, y) (which should eventually lead to fzn_count_eq(x, y, z) :: defines_var(z)) does not work or, as the comments suggests, is not intended to happen.