Почему MiniZinc иногда не использует регулярные ограничения, определенные решателем?

Согласно документам, глобальные ограничения ... могут быть специализированы для конкретного решателя. Действительно, для проблемы составления списка медсестер модель 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|];

дает fzn-файл без упоминания предиката chuffed_regular:

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 (например, с помощью аннотации)?


minizinc
person Raman Chodźka    schedule 01.01.2021    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Предикат 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? Я не нашел в документации.

person Axel Kemper    schedule 01.01.2021
comment
Действительно, изменение include "globals.mzn"; на include "regular.mzn"; приводит к ошибке компиляции. Разве это не похоже на ошибку? Вероятно, должна быть ошибка компиляции независимо от включений. Также изменение regular(..., ..., ValueAlphabet, ..., ..., ... ) на regular(..., ..., card(ValueAlphabet), ..., ..., ... ) привело к модели FlatZinc с использованием chuffed_regular, что я и искал. - person Raman Chodźka; 01.01.2021
comment
Наконец, toValueAlphabet - это функция-конструктор перечисления: minizinc.org/doc-2.5.3/en/ В примере у них есть enum ChoreOrNothing = C(Chores) ++ { Nothing }; - person Raman Chodźka; 01.01.2021