Minizinc约束不一致问题：道路连接城市请求审批约束重构

问题背景 #

开发MiniZinc模型时，需实现以下道路请求批准规则：

• 若两个城市道路连通且双方均提交道路请求，仅批准其中一方的请求；
• 否则（不连通或至少一方未提交请求），双方请求均批准。

尝试的约束代码在are_connected包含true值时，触发模型不一致警告，最终返回不可满足（UNSATISFIABLE）。实际需实现异或逻辑：仅一方的批准请求非零。

模型定义 #

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

array[cities, cities] of var bool: are_connected; % 城市间是否连通
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
  );

报错信息 #

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

问题分析 #

1. 重复约束冲突：原约束遍历所有i≠j的城市对，导致同一对城市被双向约束（如i=city2,j=city4和i=city4,j=city2），两个约束逻辑重复但被视为独立条件，引发矛盾。
2. 逻辑不完整：原约束未判断双方是否均提交请求，只要连通就强制二选一，即使其中一方无请求，违反需求逻辑。

解决方案 #

重构思路 #

• 仅遍历唯一城市对（如i<j），避免重复约束；
• 仅当are_connected[i,j]为true且双方道路请求均非零时，触发异或批准逻辑；
• 其他情况直接批准双方请求。

重构后的约束代码 #

方式1：基于枚举顺序遍历唯一城市对

constraint 
  forall(i,j in cities where i < j) (
    if are_connected[i,j] /\ requests[i, roads] > 0 /\ requests[j, roads] > 0
    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
  );

方式2：用索引处理唯一城市对（兼容无法比较的枚举）

constraint 
  forall(i in index_set(cities), j in index_set(cities) where i < j) (
    let {
      city_i = cities[i],
      city_j = cities[j]
    } in
    if are_connected[city_i, city_j] /\ requests[city_i, roads] > 0 /\ requests[city_j, roads] > 0
    then 
      (approved_requests[city_i, roads] = requests[city_i, roads] /\ approved_requests[city_j, roads] = 0) \/ 
      (approved_requests[city_j, roads] = requests[city_j, roads] /\ approved_requests[city_i, roads] = 0)
    else
      approved_requests[city_i, roads] = requests[city_i, roads] /\ approved_requests[city_j, roads] = requests[city_j, roads]
    endif
  );

方式3：用异或运算符简化逻辑

constraint 
  forall(i,j in cities where i < j) (
    if are_connected[i,j] /\ requests[i, roads] > 0 /\ requests[j, roads] > 0
    then 
      (approved_requests[i, roads] = requests[i, roads]) xor (approved_requests[j, roads] = requests[j, roads])
      /\ approved_requests[i, roads] * approved_requests[j, roads] = 0 % 确保不同时非零
    else
      approved_requests[i, roads] = requests[i, roads] /\ approved_requests[j, roads] = requests[j, roads]
    endif
  );

内容的提问来源于stack exchange，提问作者Sassa