为什么 MiniZinc 有时不使用求解器定义的正​​则约束？

编程问答 2022-06-01

问题描述

根据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,2,3,4,|
|];

constraint forall (i in 1..cnt) (
    regular(
        [tovalueAlphabet(paths[i,j]) | j in 1..tableRowSizes[i]] ++ [NULL],Q,ValueAlphabet,transitionTable,{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,3];
theTable = [|0,|0,|1,3|];

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

array [1..16] of int: X_INTRODUCED_30_ = [1,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_43_);
constraint array_int_element(X_INTRODUCED_47_,X_INTRODUCED_46_);
constraint array_int_element(X_INTRODUCED_50_,1);
constraint int_lin_eq([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_,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_,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_,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,[X_INTRODUCED_0_,X_INTRODUCED_42_],-5):: defines_var(X_INTRODUCED_42_):: domain;
constraint int_lin_eq([1,[X_INTRODUCED_1_,X_INTRODUCED_41_,X_INTRODUCED_45_],3):: defines_var(X_INTRODUCED_45_):: domain;
constraint int_lin_eq([1,[X_INTRODUCED_2_,X_INTRODUCED_43_,X_INTRODUCED_47_],3):: defines_var(X_INTRODUCED_47_):: domain;
constraint int_lin_eq([4,[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 "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,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,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