Minizinc：使用\/（或）的不一致约束

Question

我正在开发 Minizinc 模型，我遇到了这个问题：给定这个模型

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;

我想对以下约束进行建模：如果两个城市由一条道路连接，并且它们都提出道路请求，则该请求仅批准给这两个城市之一；否则，双方都批准。

我尝试按如下方式对这个约束进行建模：

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
  );

当我提供包含真实值的

are_connected

时，我收到以下警告，并且模型无法满足。

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

导致此问题的

are_connected

示例如下：

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

如何解决这个问题或重新制定约束？谢谢！

编辑：我注意到我正在使用 OR，但我真正想要实现的是独占 OR：只有一个或另一个请求可以不同于零。

Answer 1

我想通了。让我们采用城市的邻接矩阵

c1, c2, c3

:

0 1 0
1 0 0
0 0 0

根据之前的限制，我们将有以下要测试的城市组合：

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

在这种情况下，由于

c1, c2

已连接，求解器可能会将

request[c1, roads]

的值分配给

approved[c1, roads]

，将 0 分配给

approved[c2, roads]

。当评估

c2, c3

对时，

else

分支将尝试将两个

approved[c1, roads], approved[c2, roads]

值设置为各自的

request

值，但由于我们之前说过

approved[c2, roads]= 0

，我们会得到不一致的结果。

以下约束解决了该问题：

% 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])
    );

我认为这些约束可以进一步简化，但这一更改解决了问题。