时间戳

首页 > 解决方案 > 检查 MiniZinc 数组中的项目

minizinc - 检查 MiniZinc 数组中的项目

问题描述

我想在 MiniZinc 中创建两个具有相同项目的数组，不一定要以相同的顺序。在这里，每个项目A0也应该在A1：

array[1..3] of var int:A0;
array[1..3] of var int:A1;

constraint forall(A2 in A0)(
  (A2 in A1) /\ A2 < 5
 );

但是在这里，似乎有一个类型错误：

MiniZinc: type error: type error in operator application for `'in''. No matching operator found with left-hand side type `var int' and right-hand side type `array[int] of var int'

如何检查一个数组是否包含另一个数组中的相同项？

标签： minizinc

解决方案

编辑：文件中有一个array2set，builtins.mzn但它没有记录在https://www.minizinc.org/doc-2.4.2/中。

以下模型适用于大多数 FlatZinc 求解器，例如 Gecode、Google-OR-tools、Choco、PicatSAT 和 JaCoP，但不适用于 Chuffed（见下文）。请注意“nosets.mzn”的包含，以便对集合变量没有先天支持的求解器可以运行模型。此外，我添加了一个较小的域，A0以便A1于测试。

include "nosets.mzn"; % Support for set variables for all solvers
array[1..3] of var 0..10: A0;
array[1..3] of var 0..10: A1;

constraint
   forall(A2 in A0)( 
     A2 in array2set(A1) /\ A2 < 5
   )
   /\
   forall(A2 in A1)(
     A2 in array2set(A0) /\ A2 < 5
   );

   solve satisfy;

   output [ "A0: \(A0) A1: \(A1)\n" ];

但是，一些求解器不喜欢这样：

  • Chuffed：抛出“错误：注册表：在第 101 行中找不到约束 bool_lin_eq”

甚至稍后注意：如果域是var int（而不是 my var 0..10），那么 MiniZinc 会发出一个奇怪（而且很长）的错误：

...
in array comprehension expression
  comprehension iterates over an infinite set

所以array2set似乎要求变量域必须是有界的。

这是第一个答案 这是一种似乎可行的方法，即使用exists并检查元素是否相等：

constraint forall(A2 in A0)(
              exists(i in 1..3) ( A2 = A1[i] /\ A2 < 5)
);

注意：此约束仅确保 A0 中的元素在 A1 中。因此，A1 中可能存在不在 A0 中的元素。例如

A0：[1,1,4]

A1：[1,4,3]

我猜你也想要反过来，即 A1 中的所有元素也都在 A0 中：

constraint forall(A2 in A1) (
   exists(i in 1..3) ( A2 = A0[i] /\ A2 < 5)
);

注意：以下内容不起作用，但很高兴拥有。两者都产生错误MiniZinc: internal error: var set comprehensions not supported yet。

% idea 1
constraint forall(A2 in A0)(
   A2 in {A1[i] | i in 1..3} /\ A2 < 5
);

% idea 2
constraint forall(A2 in A0) (
     A2 in {a | a in A1} /\ A2 < 5         
);

推荐阅读