Flatzinc losing constraint information that leads to incorrect solutions

[lalithsuresh]

The following code should get x=1 as the only solution, but it instead gives -1, 0, and 1 as solutions (or -Int.Max to +Int.Max if I don't specify bounds for x).

var -1..1: x;
constraint sum([1 | i in 1..2 where i == x]) >= 0;

(The behavior is just as bad if I don't constraint i in the generator expression with 1..2. My original code was using another array 'z' instead of 1..2).

However, the following code does the right thing:

var -1..1: x;
var int: y = sum([1 | i in 1..2 where i == x]);
constraint y > 0;

[Dekker1]

Hi @lalithsuresh,

The two code samples are not equivalent. The first code sample allows for the sum to be 0, while the second sample doesn't. When the sum is zero, it does not constrain the variable x in any way. When changing the first sample the correct value for x is found:

var -1..1: x;
constraint sum([1 | i in 1..2 where i == x]) > 0;

[lalithsuresh]

Yikes, posted a wrong minimal test case. Sorry about that. Long day. :)

The way I got there was:

var -1..1: x;
constraint length([1 | i in 1..2 where i == x]) > 0;

The above code returns x=-1, 0, 1. I understand 'length' is not a function that I should use for this purpose, but in the absence of an error messsage, I was confused.

So when I tried this instead:

var -1..1: x;
var int: y = length([1 | i in 1..2 where i == x]);
constraint y > 0;

I get "MiniZinc: evaluation error: cannot evaluate expression 'x'".

Is this expected?

[guidotack]

There's a section in the manual that explains the behaviour of the length function in this case ("2.4.2 Hidden option types"). So the array you declare in the comprehension will always be of length 2, no matter what value x takes, because MiniZinc doesn't support variable-length arrays.

The error you get is indeed not expected, I will try to fix it for the next release.

[lalithsuresh]

Thanks @guidotack @Dekker1. I appreciate your quick responses!

[lalithsuresh]

@guidotack @Dekker1

Here's another variant of the problem I was encountering with opt variables.

array[1..2] of var 1..4 : x;
array[1..2] of int : y = [3, 4];

predicate exists_c(array[int] of var opt int: col1) = sum([1 | i in col1]) > 0;

constraint forall(i in 1..2)(
           exists_c([y[j] | j in 1..2 where y[j] == x[i]])
);

This returns every entry in the domain of x as valid solutions:

x = array1d(1..2, [1, 1]);
----------
x = array1d(1..2, [2, 1]);
----------
x = array1d(1..2, [3, 1]);
----------
x = array1d(1..2, [4, 1]);
----------
x = array1d(1..2, [1, 2]);
----------
x = array1d(1..2, [2, 2]);
----------
x = array1d(1..2, [3, 2]);
----------
x = array1d(1..2, [4, 2]);
----------
x = array1d(1..2, [1, 3]);
----------
x = array1d(1..2, [2, 3]);
----------
x = array1d(1..2, [3, 3]);
----------
x = array1d(1..2, [4, 3]);
----------
x = array1d(1..2, [1, 4]);
----------
x = array1d(1..2, [2, 4]);
----------
x = array1d(1..2, [3, 4]);
----------
x = array1d(1..2, [4, 4]);

Which is wrong, because if I assign some of those values to x directly like this:

array[1..2] of 1..4 : x = [1, 2];
array[1..2] of int : y = [3, 4];

predicate exists_c(array[int] of var opt int: col1) = sum([1 | i in col1]) > 0;

constraint forall(i in 1..2)(
           exists_c([y[j] | j in 1..2 where y[j] == x[i]])
);

... it correctly warns me that there's a model inconsistency and declares UNSAT.

Also related is if I treat x as a var like before, but do:

array[1..2] of var 1..4 : x;
array[1..2] of int : y = [3, 4];

predicate exists_c(array[int] of var opt int: col1) = sum([1 | i in col1]) > 0;

constraint x[1] = 1;
constraint x[2] = 2;
constraint forall(i in 1..2)(
           exists_c([y[j] | j in 1..2 where y[j] == x[i]])
);

It says x = array1d(1..2, [1, 2]); is a solution.

And lastly, if I write the predicate out directly inside the forall statement:

array[1..2] of var 1..4 : x;
array[1..2] of int : y = [3, 4];

constraint forall(i in 1..2)(
           sum([1 | k in [y[j] | j in 1..2 where y[j] == x[i]]]) > 0
);

I get "Cannot evaluate expression 'X_INTRODUCED_0_'".

[guidotack]

Sorry for the delayed reply, I hope it's still useful. We've been able to fix the issues that result in "cannot evaluate expression..." errors. For the unexpected behaviour (satisfiable vs. unsatisfiable), at least I can offer an explanation. The problem is the expression sum([1 | i in col1]). You expect this to iterate over the non-absent values in col1 (and that seems like the obvious semantics). However, what it does is to iterate over all values in col1 (and i has type var opt int). That's why exists_c is always true if the input array is not empty. When you fix the x, the compiler statically determines that the array is empty, so you get the correct behaviour.
To fix your code you can use sum([1 | i in col1 where occurs(i)]).