如何在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;

我想知道是否有人知道在y上传播y域的正确编码是什么。对于其他element_T约束，我设法做到了这一点，但是我无法为element_set找到一个优雅的解决方案，因为我找不到合适的内置来完成这个任务。

换句话说，我想

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

而不是

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

我该怎么做？

Answer 1

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

Answer 2

虽然很难找到索引，但是索引的域实际上是在MiniZinc函数的element定义中传播的。该定义在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-然后分支中。更重要的问题是，为什么元素约束如此复杂。答案是，这与不确定性有关。

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

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

我建议您要么使用类似的方法，要么重新定义后期谓词。(可以重新定义array_var_set_element )

有关MiniZinc中不确定性的更多信息可以在以下文章中找到：

Frisch，A.M.，& Stuckey，P.J. (2009)。约束语言中不确定性的正确处理。CP，5732,367-382。

MiniZinc使用关系语义。