根据文档，“全局约束...可以专门用于特定求解器”。实际上，对于护士排班问题，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转换表中删除转换确实可以提高求解器的性能。
这种对求解器的选择性使用是否regular为MiniZinc编译器的预期行为提供了约束？我可以以某种方式要求编译器使用求解器提供的regular约束（例如在注释的帮助下）吗？
谓词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应该做的？我在文档中找不到它。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句