У меня есть следующая модель minizinc:
include "globals.mzn";
var 0..9: A_1_1;
var 0..9: A_2_1;
var 0..9: A_3_1;
constraint (A_3_1+A_2_1+A_1_1) = A_1_1;
solve satisfy;
Модель должна иметь тривиальное решение 0=A
include "globals.mzn";
var 0..9: A_1_1;
var 0..9: A_2_1;
var 0..9: A_3_1;
constraint (A_3_1+A_2_1+A_1_1) = A_1_1;
solve satisfy;
Что я упускаю из виду?
Кажется, это ошибка в MiniZinc, когда он переводит модель в формат FlatZinc. Данное сообщение от MiniZinc:
WARNING: model inconsistency detected
test66.mzn:6:
in binary '=' operator expression
Сгенерированный файл FlatZinc содержит только это:
constraint bool_eq(false,true);
solve satisfy;
и именно поэтому решатели FlatZinc дают НЕУДОВЛЕТВОРИТЕЛЬНО.
Интересно, что следующая модель работает с использованием временной переменной решения T:
var 0..9: A_1_1;
var 0..9: A_2_1;
var 0..9: A_3_1;
var 0..9: T;
constraint
T = A_3_1 + A_2_1 + A_1_1 /\
T = A_1_1
;
solve satisfy;
Затем модель выдает все 10 решений, где A_1_1 присваиваются значения от 0 до 9, A_2_1 = A_3_1 = 0, а T присваивается то же значение, что и A_1_1.
Однако, если T инициализируется с помощью A_1_1, то снова выдается UNSAT:
переменная 0..9: T = A
WARNING: model inconsistency detected
test66.mzn:6:
in binary '=' operator expression
Обновление: можно заметить, что работает следующее ограничение, то есть 2 * A_1_1 справа:
constraint A_3_1 + A_2_1 + A_1_1 = 2 * A_1_1;
Похоже, ваше ограничение пытается использовать оператор присваивания, но операция может быть недействительной. Вы можете попробовать a = b+ c, но b+c=a может быть не разрешено. В качестве альтернативы вы можете попробовать использовать оператор равенства ==, чтобы определить ваше ограничение, которое должно работать. У меня нет установленной программы для проверки, но я надеюсь, что она даст вам немного больше информации о проблеме. Я не удивлюсь, если там тоже есть ошибка, мне было бы интересно узнать.
