为什么 MiniZinc 有时不使用求解器定义的常规约束？

Question

根据 the docs，“全局约束......可以专门用于特定的求解器”。实际上，对于 nurse rostering problem，FlatZinc 模型确实使用求解器定义的 regular 谓词（例如 chuffed_regular、ortools_regular）。

出于不明原因，MiniZinc 不使用此类求解器为以下模型提供的谓词：

include "globals.mzn";

int: cnt;
int: tableMaxRowSize;
array[1..cnt] of 0..tableMaxRowSize: tableRowSizes;
array[1..cnt, 1..tableMaxRowSize] of 0..cnt: theTable;

enum Value = {
    NONE,
    A,
    B
};
array[1..cnt] of var Value: values;
array[1..cnt, 1..tableMaxRowSize] of var Value: paths;


constraint forall (i in 1..cnt) (
    tableRowSizes[i] = 0
    \/
    forall (j in 1..tableRowSizes[i]) (
        paths[i, j] = values[theTable[i, j]]
    )
);

enum ValueAlphabet = {NULL} ++ toValueAlphabet(Value);
int: Q = 4; set of 1..Q: states = 1..Q;
array[states, ValueAlphabet] of int: transitionTable = [|
    1, 1, 1, 1, |
    1, 2, 3, 0, |
    1, 3, 0, 4, |
    1, 4, 0, 0, |
|];

constraint forall (i in 1..cnt) (
    regular(
        [toValueAlphabet(paths[i, j]) | j in 1..tableRowSizes[i]] ++ [NULL],
        Q,
        ValueAlphabet,
        transitionTable,
        2,
        {1}
    )
);

solve maximize sum (t in values) (t != NONE);

output [format(t) ++ "\n" | t in values];

用下面的数据编译上面的模型(minizinc --solver org.chuffed.chuffed -s model.mzn data.dzn -c)

cnt = 3;
tableMaxRowSize = 3;
tableRowSizes = [0,0,3];
theTable = [|0,0,0,|0,0,0,|1,2,3|];

生成一个没有提及 chuffed_regular 谓词的 fzn 文件：

array [1..16] of int: X_INTRODUCED_30_ = [1,1,1,1,1,2,3,0,1,3,0,4,1,4,0,0];
var 1..3: X_INTRODUCED_0_;
var 1..3: X_INTRODUCED_1_;
var 1..3: X_INTRODUCED_2_;
var 0..3: X_INTRODUCED_12_:: is_defined_var;
var bool: X_INTRODUCED_13_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_14_ ::var_is_introduced :: is_defined_var;
var bool: X_INTRODUCED_15_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_16_ ::var_is_introduced :: is_defined_var;
var bool: X_INTRODUCED_17_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_18_ ::var_is_introduced :: is_defined_var;
var 1..4: X_INTRODUCED_41_ ::var_is_introduced :: is_defined_var;
var 6..8: X_INTRODUCED_42_ ::var_is_introduced :: is_defined_var;
var 1..4: X_INTRODUCED_43_ ::var_is_introduced :: is_defined_var;
var 2..16: X_INTRODUCED_45_ ::var_is_introduced :: is_defined_var;
var 1..4: X_INTRODUCED_46_ ::var_is_introduced :: is_defined_var;
var 2..16: X_INTRODUCED_47_ ::var_is_introduced :: is_defined_var;
var 1..13: X_INTRODUCED_50_ ::var_is_introduced :: is_defined_var;
var 1..1: X_INTRODUCED_29_ ::var_is_introduced  = 1;
var 1..1: X_INTRODUCED_48_ ::var_is_introduced  = 1;
array [1..3] of var int: values:: output_array([1..3]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_];
constraint array_int_element(X_INTRODUCED_42_,X_INTRODUCED_30_,X_INTRODUCED_41_);
constraint array_int_element(X_INTRODUCED_45_,X_INTRODUCED_30_,X_INTRODUCED_43_);
constraint array_int_element(X_INTRODUCED_47_,X_INTRODUCED_30_,X_INTRODUCED_46_);
constraint array_int_element(X_INTRODUCED_50_,X_INTRODUCED_30_,1);
constraint int_lin_eq([1,1,1,-1],[X_INTRODUCED_14_,X_INTRODUCED_16_,X_INTRODUCED_18_,X_INTRODUCED_12_],0):: defines_var(X_INTRODUCED_12_);
constraint int_ne_reif(X_INTRODUCED_0_,1,X_INTRODUCED_13_):: defines_var(X_INTRODUCED_13_);
constraint bool2int(X_INTRODUCED_13_,X_INTRODUCED_14_):: defines_var(X_INTRODUCED_14_);
constraint int_ne_reif(X_INTRODUCED_1_,1,X_INTRODUCED_15_):: defines_var(X_INTRODUCED_15_);
constraint bool2int(X_INTRODUCED_15_,X_INTRODUCED_16_):: defines_var(X_INTRODUCED_16_);
constraint int_ne_reif(X_INTRODUCED_2_,1,X_INTRODUCED_17_):: defines_var(X_INTRODUCED_17_);
constraint bool2int(X_INTRODUCED_17_,X_INTRODUCED_18_):: defines_var(X_INTRODUCED_18_);
constraint int_lin_eq([1,-1],[X_INTRODUCED_0_,X_INTRODUCED_42_],-5):: defines_var(X_INTRODUCED_42_):: domain;
constraint int_lin_eq([1,4,-1],[X_INTRODUCED_1_,X_INTRODUCED_41_,X_INTRODUCED_45_],3):: defines_var(X_INTRODUCED_45_):: domain;
constraint int_lin_eq([1,4,-1],[X_INTRODUCED_2_,X_INTRODUCED_43_,X_INTRODUCED_47_],3):: defines_var(X_INTRODUCED_47_):: domain;
constraint int_lin_eq([4,-1],[X_INTRODUCED_46_,X_INTRODUCED_50_],3):: defines_var(X_INTRODUCED_50_):: domain;
solve  maximize X_INTRODUCED_12_;

以上模型是实际模型的简化版，Chuffed和OR-Tools都未能在合理的时间内解决。另外我确定求解器性能不佳的原因与 regular 约束有关，因为在实际模型中我消除了所有其他约束并且求解性能没有提高。另一方面，从 dfa 转换中移除转换 table 确实提高了求解器的性能。

求解器的这种选择性使用提供了 regular 约束是 MiniZinc 编译器的预期行为吗？我能否以某种方式要求编译器使用求解器提供的 regular 约束（例如在注释的帮助下）？

Answer 1

Predicate regular 以 set of ValueAlphabet 作为第三个参数调用。但它期望 int.

我修改了include语句为

include "regular.mzn";

这导致出现以下错误消息：

MiniZinc: type error: no function or predicate with this signature found: `regular(array[int] of var ValueAlphabet,int,set of ValueAlphabet,array[int,ValueAlphabet] of int,int,set of int)'
Cannot use the following functions or predicates with the same identifier:
predicate regular(array[int] of var int: x,int: Q,int: S,array[int,int] of int: d,int: q0,set of int: F);
    (argument 3 expects type int, but type set of ValueAlphabet given)

我不确定您模型中的以下行：

enum ValueAlphabet = {NULL} ++ toValueAlphabet(Value);

toValueAlphabet 应该做什么？我在文档中找不到它。

为什么 MiniZinc 有时不使用求解器定义的常规约束？

Why does MiniZinc sometimes not use regular constraint defined by a solver?

minizinc