Unsatisfiable solution with `constraint forall(i in x)( x[i] <= x[i+1] );`

Question

I'm working on a toy problem to learn minizinc. Take an array (hardcoded to size 3 for now) of values between 0 and 9 and find the combinations where the sum is equal to the product.

par int: n = 3; % hardcode for now 

array[1..n] of var 0..9: x;

constraint sum(x) != 0;
constraint sum(x) == product(x);

output["\(x)"];

Outputs

[2, 3, 1]
----------

This works as expected, however, next I try to constrain so that the values must increase in order.

First I tried this:

constraint forall(i in x)( 
   x[i] <= x[i+1]
);

This was UNSATISFIABLE. I was thinking this could be due to the i+1 index being greater than the size of the array for the last item. So I added a condition to the forall to prevent the index of the last item being out of bounds:

constraint forall(i in x)( 
   i < n /\ x[i] <= x[i+1]
);

However, this was also UNSATISFIABLE.

Something is amiss with my conceptual understanding. What is wrong with my approach?

Answer 1

PROBLEM(s).

In general, the constraint is fine. In the context of this example, however, it is inconsistent. Let's see why this is the case.

We know that the solution must include 1, 2, 3, thus, we can infer that the constraint

constraint forall (i in x) (
    x[i] <= x[i+1]
);

is "equivalent" to

constraint x[1] <= x[2];
constraint x[2] <= x[3];
constraint x[3] <= x[4];

for which mzn2fzn reports the following issue:

  WARNING: undefined result becomes false in Boolean context
  (array access out of bounds)
  ./t.mzn:12:
  in binary '<=' operator expression
  in array access

When the same constraint is written without hard-encoded index values, the mzn2fzn compiler is unable to detect the inconsistency before the solver is invoked. However, the semantics of the access out of bounds is still the same (i.e. false) at run-time, so the formula becomes unsatisfiable.

The constraint

constraint forall(i in x)( 
   i < n /\ x[i] <= x[i+1]
);

augments the previous constraint with the requirement that i must be smaller than n. This is clearly false for i = 3, so there is one more inconsistency in the model. The constraint would be correct if you used the implication symbol -> instead of the (logical) and symbol /\.

---

SOLUTION(s).

First, let me set aside a possible misunderstanding of the language. The comprehension i in x, which you used in your model, refers to the elements inside the array x, and not to the index set of x. In this particular case the solution and the index set of x contain the same values, so it does not cause an inconsistency. However, this is not true in general, so it's better to use the function index_set() as follows:

constraint forall(i, j in index_set(x) where i < j)(
   x[i] <= x[j]
);

example:

par int: n = 3; % hardcode for now 

array[1..n] of var 0..9: x;

constraint sum(x) != 0;
constraint sum(x) == product(x);

constraint forall(i, j in index_set(x) where i < j)(
   x[i] <= x[j]
);

solve satisfy;

output["\(x)"];

yields

~$ mzn2fzn test.mzn 
~$ optimathsat -input=fzn < test.fzn 
x = array1d(1..3, [1, 2, 3]);
----------

---

A more elegant solution is to use the following global constraint, which is mentioned in the documentation (v. 2.2.3) of MiniZinc:

predicate increasing(array [int] of var bool: x)
predicate increasing(array [int] of var int: x)
predicate increasing(array [int] of var float: x)

The predicate admits duplicate values in the array, that is, it enforces a non-strict increasing order (if that is needed, combine increasing with distinct).

The predicate is contained in the file increasing.mzn. However, people normally include the file globals.mzn instead, so as to have access to all predicates at once.

example:

include "globals.mzn";

par int: n = 3; % hardcode for now 

array[1..n] of var 0..9: x;

constraint sum(x) != 0;
constraint sum(x) == product(x);

constraint increasing(x);

solve satisfy;

output["\(x)"];

yields

~$ mzn2fzn t.mzn 
~$ optimathsat -input=fzn < t.fzn 
x = array1d(1..3, [1, 2, 3]);
----------