Minizinc: inconsistent constraint reformulation

Question

I'm developing a Minizinc model and I ran into this issue: given this model

enum req_type = {roads, rivers};
enum cities = {city1, city2, city3}


array[cities, cities] of var bool: are_connected; % true if cities are connected, false otherwise
array[cities, req_type] of var 0..1000: requests;
array[cities, req_type] of var 0..1000: approved_requests;

i want to model the following constraint: if two cities are connected by a road and they both make a request for roads, then the request is approved to only one of the two cities; otherwise, it is approved to both.

I've tried to model this constraint as follows:

constraint 
  forall(i,j in cities where i != j) (
    if are_connected[i,j] 
    then 
      approved_requests[i, roads] = requests[i, roads] /\ approved_requests[j, roads] = 0 \/ 
      approved_requests[j, roads] = requests[j, roads] /\ approved_requests[i, roads] = 0
    else
      approved_requests[i, roads] = requests[i, roads] /\ approved_requests[j, roads] = requests[j, roads]
    endif
  );

When i provide an are_connected which contains true values I get the following warning, and the model is unsatisfiable.

Warning: model inconsistency detected
...
  in call 'forall'
  in array comprehension expression
    with i = 2
    with j = 4
...
  in if-then-else expression
...
  in binary '\/' operator expression

=====UNSATISFIABLE=====
% time elapsed: 0.07 s

An example of are_connected that causes this problem is the following:

are_connected = [|
    false, false, false, false |
    false, false, false, true |
    false, false, false, false |
    false, true, false, false |
|];

How can I solve this issue or reformulate the constraint? Thank you!

EDIT: I noticed I was using OR but what I'm really trying to achieve is exclusive OR: only one OR the other request can be different than zero.

Answer 1

I figured it out. Let's take this adjacency matrix for the cities c1, c2, c3:

0 1 0
1 0 0
0 0 0

With the previous constraints, we would have the following combination of cities to be tested:

c1 c2; c1 c3;
c2 c1; c2 c3;
c3 c1; c3 c2;

In this case, since c1, c2 are connected, the solver might assign the value of request[c1, roads] to approved[c1, roads], and 0 to approved[c2, roads]. When evaluating the pair c2, c3, the else branch will try to set both approved[c1, roads], approved[c2, roads] values to the respective request value, but since we previously said that approved[c2, roads]= 0 we get the inconsistency.

The following constraints solve the issue:

% we guarantee that one at least one 'approved' of the two is 0
constraint
    forall(c1 in cities, c2 in cities where are_connected[c1, c2] = true /\ c1 < c2) (
        (approved[c1, strade] = requests[c1, strade] /\ approved[c2, strade] = 0) \/
        (approved[c1, strade] = 0 /\ approved[c2, strade] = requests[c2, strade])
    );

% we guarantee that if the value was not previously 0, then it is equal to the request
constraint
    forall(c1 in cities , c2 in cities where are_connected[c1, c2] = false /\ c1 < c2) (
      (not (approved[c1, strade] == 0) -> approved[c1, strade] = RICHIESTE[c1, strade]) /\
      (not (approved[c2, strade] == 0) -> approved[c2, strade] = RICHIESTE[c2, strade])
    );

I think these constraints can be simplified further but this change solved the issue.