1

我有以下MiniZinc代码示例：

include "globals.mzn";

var int: i;
array[-3..3] of var set of 1..10: x;
var set of 1..100: y;

constraint element(i, x, y);

solve satisfy;

output [
    show(i), "\n",
    show(x), "\n",
    show(y), "\n",
];

mzn2fzn使用标准库执行的命令输出以下FlatZinc代码：

var set of 1..10: X_INTRODUCED_0_;
var set of 1..10: X_INTRODUCED_1_;
var set of 1..10: X_INTRODUCED_2_;
var set of 1..10: X_INTRODUCED_3_;
var set of 1..10: X_INTRODUCED_4_;
var set of 1..10: X_INTRODUCED_5_;
var set of 1..10: X_INTRODUCED_6_;
var -3..3: i:: output_var;
var set of 1..10: y:: output_var;
var 1..7: X_INTRODUCED_9_ ::var_is_introduced :: is_defined_var;
array [1..7] of var set of int: x:: output_array([-3..3]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_,X_INTRODUCED_3_,X_INTRODUCED_4_,X_INTRODUCED_5_,X_INTRODUCED_6_];
constraint array_var_set_element(X_INTRODUCED_9_,[X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_,X_INTRODUCED_3_,X_INTRODUCED_4_,X_INTRODUCED_5_,X_INTRODUCED_6_],y):: defines_var(y);
constraint int_lin_eq([1,-1],[i,X_INTRODUCED_9_],-4):: defines_var(X_INTRODUCED_9_):: domain;
solve  satisfy;

在这里，请注意最初在模型中y被声明为 a ，但正确地将数组元素的边界传播到 上，因此模型声明为 a 。set of 1..100MiniZincmzn2fznxyFlatZincyset of 1..10

现在，我想自定义 的内容，element_set.mzn以便在使用时调用我自己的谓词element_set，所以我将其更改为如下：

predicate element_set(var int: i, array[int] of var set of int: x,
        var set of int: y) =
    min(index_set(x)) <= i /\ i <= max(index_set(x)) /\
    optimathsat_element_set(i, x, y, index_set(x));

predicate optimathsat_element_set(var int: i,
                                  array[int] of var set of int: x,
                                  var set of int: y,
                                  set of int: xdom);

但是，此代码不会将数组元素的边界传播x到 上y，因此生成的FlatZinc文件y仍然声明为set of 1..100：

predicate optimathsat_element_set(var int: i,array [int] of var set of int: x,var set of int: y,set of int: xdom);
var set of 1..10: X_INTRODUCED_0_;
var set of 1..10: X_INTRODUCED_1_;
var set of 1..10: X_INTRODUCED_2_;
var set of 1..10: X_INTRODUCED_3_;
var set of 1..10: X_INTRODUCED_4_;
var set of 1..10: X_INTRODUCED_5_;
var set of 1..10: X_INTRODUCED_6_;
var -3..3: i:: output_var;
var set of 1..100: y:: output_var; %%% OFFENSIVE LINE %%%
array [1..7] of var set of int: x:: output_array([-3..3]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_,X_INTRODUCED_3_,X_INTRODUCED_4_,X_INTRODUCED_5_,X_INTRODUCED_6_];
constraint optimathsat_element_set(i,x,y,-3..3);
solve  satisfy;

我想知道是否有人知道传播xover域的正确编码是什么y。我设法为其他element_T约束做到了这一点，但我无法找到一个优雅的解决方案element_set，因为我找不到合适的内置函数来执行此操作。

换句话说，我想得到

var set of 1..10: y:: output_var;

代替

var set of 1..100: y:: output_var;

我该怎么做？

4

2 回答 2

2

虽然有点难找，但索引的域实际上是在element函数的 MiniZinc 定义中传播的。定义见builtins.mzn，如下：

function var set of int: element(var int: idx, array[int] of var set of int: x) =
  if mzn_in_root_context(idx) then let {
    constraint idx in index_set(x)
  } in element_t(idx,x)
  elseif (has_bounds(idx) /\ lb(idx) >= min(index_set(x)) /\ ub(idx) <= max(index_set(x))) then
    element_t(idx,x)
  else let {
    constraint idx in index_set(x)
  } in element_mt(idx,x)
  endif;

您可以看到您的元素约束被评估为在第一个 if-then 分支中。更重要的问题是，为什么元素约束如此复杂。答案是它与不确定性有关。

假设我们有一个array[1..3] of int: a，那么a[4]评估是什么？将这样的事情设为非法似乎很容易，但表达式a[i] > 5 \/ i > 10. 这可能是一个经过深思熟虑的模型，应该可以满足i = 11. 在 MiniZinc 中，这些非法值被称为 undefined 并冒泡到最接近的布尔表达式 be false。

现在，当我们回顾元素约束时，我们可以理解在根上下文中，就像在您的示例中一样，我们可以只强制域并使用“安全”元素约束。同样，如果索引的边界小于数组边界，我们可以使用“安全”元素约束，但如果边界更大，我们使用“不安全”元素约束，并确保true仅在定义值时返回。

我建议您使用类似的方法或重新定义后期谓词。（可以改为重新定义array_var_set_element）

有关 MiniZinc 中不确定性的更多信息，请参阅以下论文：

弗里施，上午和斯塔基，PJ（2009 年）。约束语言中未定义的正确处理。CP, 5732, 367-382。

MiniZinc 使用关系语义。

于 2017-11-09T00:01:00.457 回答
0

element/谓词族element_T在内部映射到element/element_T函数族。

在MiniZinc版本2.0.2及更高版本中，这些函数映射到以下谓词：

% This file contains redefinitions of standard builtins for version 2.0.2
% that can be overridden by solvers.

...    

predicate array_var_bool_element_nonshifted(var int: idx, array[int] of var bool: x, var bool: c) =
  array_var_bool_element((idx-(min(index_set(x))-1))::domain,array1d(x),c);

predicate array_var_int_element_nonshifted(var int: idx, array[int] of var int: x, var int: c) =
  array_var_int_element((idx-(min(index_set(x))-1))::domain,array1d(x),c);

predicate array_var_float_element_nonshifted(var int: idx, array[int] of var float: x, var float: c) =
  array_var_float_element((idx-(min(index_set(x))-1))::domain,array1d(x),c);

predicate array_var_set_element_nonshifted(var int: idx, array[int] of var set of int: x, var set of int: c) =
  array_var_set_element((idx-(min(index_set(x))-1))::domain,array1d(x),c);

最好的解决方案是覆盖这些谓词而不是弄乱element/ element_T。

于 2017-11-11T08:29:51.337 回答