array_var_bool_element allows inconsistent index values

[GustavBjordal]

Running the following model on Gecode 6.3.0 under MiniZinc 2.5.5

array[1..10] of var bool: x;
var 20..30: i;
var bool: y;
constraint y = x[i];

give the following solution when it should actually give UNSAT:

x = array1d(1..10, [false, false, false, false, false, false, false, false, false, false]);
i = 20;
y = false;
----------

My best guess is that array_var_bool_element is compiled in a reified context due to some bug somewhere. If one compiles the following model (note the changed domain of i) then one gets the then following FlatZinc:

array[1..10] of var bool: x;
var 1..30: i;
var bool: y;
constraint y = x[i];

predicate int_eq_imp(var int: a,var int: b,var bool: r);
predicate gecode_bool_element(var int: idx,int: idxoffset,array [int] of var bool: x,var bool: c);
var bool: X_INTRODUCED_0_;
...
var bool: X_INTRODUCED_9_;
var 1..30: i:: output_var;
var bool: y:: is_defined_var:: output_var;
var bool: X_INTRODUCED_10_ ::var_is_introduced :: is_defined_var;
var bool: X_INTRODUCED_11_ ::var_is_introduced :: is_defined_var;
var 1..10: X_INTRODUCED_12_ ::var_is_introduced ;
var bool: X_INTRODUCED_15_ ::var_is_introduced :: is_defined_var;
array [1..10] of var bool: x:: output_array([1..10]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_,X_INTRODUCED_3_,X_INTRODUCED_4_,X_INTRODUCED_5_,X_INTRODUCED_6_,X_INTRODUCED_7_,X_INTRODUCED_8_,X_INTRODUCED_9_];
constraint array_bool_or([X_INTRODUCED_10_,X_INTRODUCED_15_],true);
constraint gecode_bool_element(X_INTRODUCED_12_,1,x,X_INTRODUCED_11_):: defines_var(X_INTRODUCED_11_);
constraint int_eq_imp(X_INTRODUCED_12_,i,X_INTRODUCED_10_);
constraint array_bool_and([X_INTRODUCED_10_,X_INTRODUCED_11_],y):: defines_var(y);
constraint set_in_reif(i,1..10,X_INTRODUCED_10_):: defines_var(X_INTRODUCED_10_);
constraint int_eq_imp(X_INTRODUCED_12_,1,X_INTRODUCED_15_):: defines_var(X_INTRODUCED_15_);
solve  satisfy;

This looks pretty reified to me...

[Dekker1]

Hi Gustav,

This is part of relational semantics. Whenever you use a partial function (such as the element function) and the result is undefined, it makes the closest Boolean context false. In this case, the closest Boolean context is the result of the element function itself. This means the RHS of the equality constraint is set to false, not the full constraint.

So although I see how this can be confusing, it is at least intended behaviour.

[GustavBjordal]

I see what you mean, this is very interesting and makes sense I guess. But what is then the semantics of the FlatZinc array_bool_element? The documentation states as [ b ] = c, but as you just pointed out, this should allow b to take a value outside the index set of as. But, why does the compiler then introduce the extra constraints for dealing with the index out of bounds case? It seems like the semantics of array_bool_element on the FlatZinc level behave as I first expected, while at the MiniZinc level the semantics is as you just explained (which I agree is technically correct). But this then creates a point of friction in the documentation and it is not clear which semantics a solver should implement.

However, is this design actually good from a language point of view? It feels like it is setting people up for failure, as this is a rather obscure fact about the element constraint on boolean variables that easily leads to unintentional bugs in both models and solvers. Note for example that this means that the following two models are not equivalent even though I'd claim that most people (and even solvers) would treat them as such:

array[1..10] of var bool: x;
var 1..30: i;
var bool: y;
constraint y = x[i];

array[1..10] of var 0..1: x;
var 1..30: i;
var 0..1: y;
constraint y = x[i];

It seems to me like there should be two versions of the element constraint on boolean variables, one array_bool_element(as, b, c) that requires that the index is within the index set, and one called something like array_bool_element_open(as, b, c) that does not. I would then argue that y = x[i] should be treated as array_bool_element(x, i, y), and that the open version either does not have a functional version or is written as y <-> x[i]. This would at least preserve semantics when going between a boolean model and a 01 model, and the y <-> x[i] would not directly translate, which is a good thing! Note that the current semantics of Minizinc is basically y <-> y = x[i], which while correct seems like semantics that should be opt-in rather than opt-out.

ps. Note that based on what you just pointed out, the element constraint on boolean variables is actually a total function! So at least it is a bug that the compiler seems to treat it as a partial function and generates constraint for when the index is out of bounds.

[Dekker1]

I think there are a few parts to the your comments:

First, the semantics of the FlatZinc level element predicate array_bool_element. It is a design decision that in the transformation from MiniZinc to FlatZinc all partial functions are transformed, such that they do not contain (or at least depend) on the semantics for partiality of the solvers. This is partially a reaction to the different ways in which solvers handle these cases. The semantics for array_bool_element in the solver can thus assume that the index out of bounds is not allowed and remove any value from the domain that are. Note that it might be possible to change the handling of this in the solver's MiniZinc library, but at the moment this is tricky to say the least.

Second, I agree that the model you show is particularly tricky, but I do not agree with you assertion that the modeller can expect that it works a certain way. In any programming language, be it C++, Java, or MiniZinc, using undefined behaviour/partial functions should be something you have to be wary off, and when you do, you have to be especially careful. MiniZinc has chosen a clear semantic, and tries to warn the user (the warning would show up if the accessor was a parameter, but maybe this should be extended to also check variable domains). The point of action here is probably that we should have better documentation on the semantics of MiniZinc. This is indeed a big difference in MiniZinc between using 0..1 variables and Boolean variables.

Then, I believe that changing the semantics based on an operator would only make this more complex. I think your point is might be more related about what a solver might expect, and I think that is something that we could look into. If the solver can ensure that partiality is handled correctly and more efficiently, we should be promoting that! However, I think when it comes to modelling I think that it is a lot more clear to explicitly add the i in index_set(x) constraint, rather than choosing between two operators, which are intended to be equivalent. (This would introduce a similar issues as with the different of using 0..1 and Boolean variables).

Finally, element is not a total function in MiniZinc. Relational semantics merely make it look like one. Under relational semantics when the function is undefined, the closest Boolean context becomes false. In MiniZinc this means that for example the constraint

constraint y = x[j];

where y and x are of integer type, would be compiled as:

constraint j in index_set(x) /\ y = element_t(j, x);

where element_t is element function that can only be used when it is guaranteed to be total. It is only allowed to be used because the constraint is in root context (and force to take a value in the index set).

When using Boolean types the only change is that the closest Boolean context is not the equivalence, but the result of the element itself. It is thus compiled as:

constraint  y = (j in index_set(x) /\ element_mt(j, x));

Notice, however, that the element is no longer in root context, instead it is in a positive context. We use the element_mt (make total) function instead to wrap around element_t that uses a variable that is equivalent to j when it is within the index set and a dummy value otherwise.

[guidotack]

Just a tiny correction to Jip’s comment: Gustav is correct that element on a var bool array is a total function (because all functions that return var bool are by definition total). But the FlatZinc solver built-in has a different semantics (the one that fails when the index is out of range), and that’s why MiniZinc has to translate the total call to the element function using reification. It would actually be better to have the solver do this instead. So we should introduce a new builtin array_bool_element_total, which by default would be decomposed into the current element constraint and reification.

[GustavBjordal]

Thanks for the replies, I have a few more thoughts. I apologise that there are basically four things discussed here: the syntax for element on var bool, 01 models vs. bool models, the FlatZinc semantics of element, and the documentation. I'll try to keep things separated.

For the syntax of element, I agree that giving a special meaning to y <-> x[i] adds complexity and might even be a terrible idea. But, I think it is worth considering, and one can make roughly the same argument of "using undefined behaviour/partial functions should be something you have to be wary off, and when you do, you have to be especially careful": with two versions of element you get the option to carefully consider which version you should use and it makes you aware of the oddity. I find it telling that the documentation for the FlatZinc solver built-in is defined simply as "Constrains as[b] = c" without any other mention of the semantics, but this is meant to be interpreted as b must be in the index set of as. Also I have always found it a bit funny (and redundant) that =, ==, and<-> are synonyms, so I wouldn't find it too strange if <-> conveyed some different meaning. Anyway, for this post I will use y <-> x[i] to mean the current version and y = x[i] to mean the version that requires i to be in the index set of x.

Next, I think the topic of 01 models vs. bool models is interesting. Clearly, one cannot replace each var bool by var 0..1 and expect the model to even compile, as boolean operators such as /\ are not defined for integers. However, as far as I can tell, it is perfectly fine to do a naive find&replace for each var 0..1 by var bool, and still get a semantically equivalent model that will compile and run, with the (only?) exception being the element constraint. That is, if it wasn't for the current semantics of element on boolean variables, then any 01 model can be trivially transformed into a bool model. Maybe there is some other exception that I am not aware of, please let me know if that's the case. For this reason, I think that it could make some sense for y <-> x[i] to have a different semantic from y = x[i] as that would exemplify why you cannot directly go from bool to 01, while you can (or should be able to) go directly from 01 to bool.

As for the FlatZinc semantics, it would be nice if, as Guido suggests, both versions where available to the solver. Since y <-> x[i] is a total function, one can deal with it significantly better internally in a local search solver compared to what can be done with the current flattening. In fact, implementing y <-> x[i] would have no overhead compared to y = x[i] in fzn-oscar-cbls, as one has to worry about i taking a value outside the index set either way in a LS solver.

Finally, all of this should at the very least be clarified in the documentation. The current "Constrains as[b] = c" is clearly not correct when writing as[b] = c in MiniZinc would give a different semantic. Same also applies to the nonshifted and element2d versions of course. And again, if there are any other examples like this then that would be interesting to know!

By the way, note that, except for updating the documentation, I do not have any strong opinion here: I just find the current state of things a bit counter-intuitive and would just like to hear your thoughts here.