如何在 mzn2fzn 转换期间传播一组 int 域？

Question

我有以下 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 在 MiniZinc 模型中被声明为 set of 1..100，但是 mzn2fzn 正确地传播了数组 x 到 y，因此 FlatZinc 模型将 y 声明为 set 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;

我想知道是否有人知道将 x 的域传播到 y 的正确编码是什么。我设法为其他 element_T 约束做到了这一点，但我无法为 element_set 找到一个优雅的解决方案，因为我找不到合适的 builtins这样做。

换句话说，我想得到

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

而不是

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

我该怎么做？

Answer 1

虽然有点难找，索引的域实际上是在 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 分支中。更重要的问题是，为什么元素约束这么复杂。答案是和undefinedness有关。

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

现在，当我们回顾元素约束时，我们可以理解在根上下文中，就像在您的示例中一样，我们可以强制执行域并使用 "safe" 元素约束。类似地，如果索引的边界小于数组边界，我们可以使用 "safe" 元素约束，但如果边界更大，我们使用 "unsafe" 元素约束并确保 true仅在定义值时返回。

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

关于 MiniZinc 中未定义的更多信息可以在以下论文中找到：

Frisch, A. M., & Stuckey, P. J. (2009). The Proper Treatment of Undefinedness in Constraint Languages. CP, 5732, 367-382.

MiniZinc 使用关系语义。

Answer 2

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 谓词。

如何在 mzn2fzn 转换期间传播一组 int 域？

How to propagate set of int domains during mzn2fzn conversion?

minizinc

flatzinc