在 MiniZinc 中定义约束

Defining constraints in MiniZinc

我是约束编程和 MiniZinc 的新手 我想为以下问题定义约束。你能帮帮我吗

3 数组 F1,F2 和 F3 有子元素 (F1a,F1b) ; (F2a,F2b,F2c); (F3a,F3b,F3c,F3d) 分别。

我需要使用以下规则定义约束

*需要从每个族 F1 和 F3 中选择 1 个元素,F2b 包含在所有可能的解决方案中

我需要找到可能的解决方案

谢谢

我的实际问题有 650 个数组,如 F1、F2...,并且有 75000 个约束,如我所说。如果扩展下面由 Alex/Dekker 给出的相同逻辑,我会 运行 进入性能问题吗?解决如此严重问题的正确方法应该是什么 谢谢

这可以使用 sum 函数和用户定义的 predicate:

来表示
array[1..2] of var bool: F1;
array[1..3] of var bool: F2;
array[1..4] of var bool: F3;

%  assuming that exactly one has to be picked
constraint sum(F1) == 1;  %  same as (F1[1]+F1[2]) == 1
constraint sum(F2) == 1;
constraint sum(F3) == 1;

predicate coexist(array[int] of var bool: x ) =
  sum(x) > 1;
  
constraint not coexist([F1[1], F2[2]]);
constraint not coexist([F2[2], F3[2]]);
constraint not coexist([F1[1], F2[2], F3[1]]);

必须从元素数组中选取一定数量的元素的想法可以用许多不同的方式表示。如果我们被迫选择某个数字,那么使用 count 全局约束是最好的方法。 (但是,至少选择一个元素最好使用 exists 函数来完成,它表示逻辑或运算。)

元素的共存也是通过统计激活元素的数量来表示的。如果不允许共存,则一次只能激活 1 个。在我们只推理两个元素的情况下,有一个独特的场景,我们可以使用 /\ 运算符同时排除两个元素的使用。

您的模型因此可以变成:

array[1..2] of var bool: F1;
array[1..3] of var bool: F2;
array[1..4] of var bool: F3;
 
constraint count(F1) == 1; % Pick 1 element from F1
constraint count(F2) == 1; % Pick 1 element from F2
constraint count(F3) == 1; % Pick 1 element from F3
  
constraint not (F1[1] /\ F2[2]); % F2b and F1a cannot coexist in a solution
constraint not (F2[2] /\ F3[2]); % F2b and F3b cannot coexist in a solution
constraint count([F1[1], F2[2], F3[1]]) <= 1; % F1a F2b and F3a cannot coexist in a solution