有没有办法在 minizinc 谓词中提供搜索注释？答案

【问题标题】：is there a way to provide search annotation in minizinc predicate?有没有办法在 minizinc 谓词中提供搜索注释？
【发布时间】：2018-10-04 20:05:46
【问题描述】：

我想知道是否可以在 minizinc 谓词中提供搜索顺序。例如我有这样的代码

predicate numbers_falling_within_range (var int:a, var int:b)=
      let {
         var 213233..4535553: num;
       } in 
       (a+b<num*64+64) /\ (a+b>num*64);  %% pick a and b such that their sum fall within a range

这里我希望它在执行谓词时首先求解num，然后是a 或b。有没有办法做到这一点？我正在寻找类似于解决我们在模型末尾提供的订单注释的东西。

【问题讨论】：

标签： minizinc

【解决方案1】：

您可以设计搜索策略的唯一地方是解决项目，但您可能还会问：“我可以针对（到谓词）局部变量设计搜索策略吗？”

由于 MiniZinc 是一种范围语言，您无法真正访问谓词之外的这些变量，但您可以将它们提升到全局范围：

int num_num = ???;
array[1..num_num] of var 213233..4535553: nums;
predicate numbers_falling_within_range (var int: a, var int: b, var int: num) =
  (a+b<num*64+64) /\ (a+b>num*64);

% a call to the predicate
constraint numbers_falling_within_range(x, y, nums[1]);

solve ::int_search(nums, input_order, indomain_min) minimize cost;

请注意，这种方法只有在可以（高估）估计谓词调用次数并给每个调用一个不同的（现在是全局的）变量的情况下才有可能。除非您的谓词是递归的，否则这应该相对简单。

【讨论】：

我明白了。这种带出局部变量的想法很好。我会试试看。顺便问一下，从 minizinc 语言的角度来看，在谓词范围内提供这样的注释是否可行？某种“先解决”类型的提示？
由于声明性语言的性质，迭代构建事物的方法通常是不可能的。通常不难将这些方法改写为向全局状态添加东西的东西，这是可能的。因此，要直接在 MiniZinc 中回答您的问题，目前还没有像您描述的那样的功能。