当我知道有解决方案时，约束报告为“无法满足”（菜鸟错误？）

Question

作为 MiniZinc 的首次用户，我尝试用它来编写一个我已经知道解决方案的逻辑谜题。然而，当我尝试对所有谜题线索进行编码并运行代码时，它会报告回来=====UNSATISFIABLE=====。下面的代码运行，但如果两个注释掉的约束中的任何一个未注释，则找不到解决方案。

\n

我很可能在某个地方犯了错误，但我正在努力寻找它。非常感谢任何帮助！

\n

% Christmas Puzzle 2021\n\ninclude "alldifferent.mzn";\n\n% There are 9 reindeer numbered 1 to 9 and there are 9 different types of food.\n% The reindeer fly on three test flights and are fed one of the foods prior to\n% each test flight.\n\nset of int: REINDEER = 1..9;\nset of int: FOOD = 1..9;\nset of int: FLIGHT = 1..3;\n\n% Each reindeer has a favourite food\n\narray[REINDEER] of var FOOD: favourite;\narray[FLIGHT, REINDEER] of var FOOD: fed;\n\n%%% CLUES %%%\n\n% Reindeer 2\xe2\x80\x99s favourite food is 4\nconstraint favourite[2] == 4;\n\n% Before test \xef\xac\x82ight 1, reindeer 2 was given food 4\nconstraint fed[1, 4] == 4;\n\n% Before test \xef\xac\x82ight 2, reindeer 2 was given food 4\nconstraint fed[2, 4] == 4;\n\n% Before test \xef\xac\x82ight 3, reindeer 2 was given food 6\nconstraint fed[3, 4] == 6;\n\n% Before test \xef\xac\x82ight 3, a total of 4 reindeer were given the wrong food\nconstraint count([fed[3, r] - favourite[r] | r in REINDEER], 0, 5);\n\n% Reindeer 4\xe2\x80\x99s favourite food is a factor of 607\nconstraint favourite[4] == 1;\n\n% Reindeer 4 was given the same food before all three test \xef\xac\x82ights.\nconstraint fed[1, 4] == fed[2, 4];\n% =====UNSATISFIABLE===== \n%constraint fed[1, 4] == fed[3, 4];\n\n% Before test \xef\xac\x82ight 1, reindeer 8 was given food 3\nconstraint fed[1, 8] == 3;\n\n% Before test \xef\xac\x82ight 1, a total of 2 reindeer were given the wrong food.\nconstraint count([fed[1, r] - favourite[r] | r in REINDEER], 0, 7);\n\n% Before test \xef\xac\x82ight 1, reindeer 9 was given food 6\nconstraint fed[1, 9] == 6;\n\n% Before test \xef\xac\x82ight 2, reindeer 9 was given food 5\nconstraint fed[2, 9] == 5;\n\n% Before test \xef\xac\x82ight 3, reindeer 9 was given food 1\nconstraint fed[3, 9] == 1;\n\n% Before test \xef\xac\x82ight 2, reindeer 4 was not given food 9\nconstraint fed[2, 4] != 9;\n\n% Before test \xef\xac\x82ight 2, 2 reindeer were given the wrong food\n% =====UNSATISFIABLE===== \n%constraint count([fed[2, r] - favourite[r] | r in REINDEER], 0, 7);\n\n% Reindeer 1 was given food 1 before all three test \xef\xac\x82ights\nconstraint fed[1, 1] == 1;\nconstraint fed[2, 1] == 1;\nconstraint fed[3, 1] == 1;\n\n% Before test \xef\xac\x82ight 2, all the reindeer were given di\xef\xac\x80erent foods\nconstraint all_different([fed[2, r] | r in REINDEER]);\n\n% Before test \xef\xac\x82ight 1, reindeer 7 was not given food 7\nconstraint fed[1, 7] != 7;\n\n% Before test \xef\xac\x82ight 2, reindeer 8 was given food 2\nconstraint fed[2, 8] == 2;\n\n% Before test \xef\xac\x82ight 3, reindeer 5 was not given food 7\nconstraint fed[3, 5] !=7;\n\n% Before test \xef\xac\x82ight 3, 3 reindeer had the food equal to their number\nconstraint count([fed[3, r] - r | r in REINDEER], 0, 3);\n\n% Before test \xef\xac\x82ight 3, reindeer 7 was given food that is a factor of 148\nconstraint fed[3, 7] == 1 \\/ fed[3, 7] == 2 \\/ fed[3, 7] == 4;\n\n% Before test \xef\xac\x82ight 3, reindeer 7 was not given food 1\nconstraint fed[3, 7] != 1;\n\n% Before test \xef\xac\x82ight 3, no reindeer was given food 2\nconstraint forall([fed[3, r] != 2 | r in REINDEER]);\n\n% Before test \xef\xac\x82ight 1, reindeer 7 was not given food 9\nconstraint fed[1, 7] != 9;\n\nsolve satisfy;\n\noutput [\n  "Favourites    = ", show(favourite), "\\n",\n  "Test flight 1 = ", show([fed[1, r] | r in REINDEER]), "\\n",\n  "Test flight 2 = ", show([fed[2, r] | r in REINDEER]), "\\n",\n  "Test flight 3 = ", show([fed[3, r] | r in REINDEER]), "\\n"\n  ];\n

\n

请注意，以下结果应满足所有线索：

\n

Favourites    = [1, 4, 3, 1, 9, 6, 8, 3, 5]\nTest flight 1 = [1, 4, 3, 7, 9, 6, 8, 3, 6]\nTest flight 2 = [1, 4, 3, 7, 9, 6, 8, 2, 5]\nTest flight 3 = [1, 6, 3, 7, 9, 6, 4, 3, 1]\n

\n

我不知道是否有一种方法可以通过从该解决方案向后进行调试来查看哪些约束（如果有）未被满足。

\n

Answer 1

第一个约束中有一些拼写错误，可能是复制/粘贴问题。以下是变化：

% Before test flight 1, reindeer 2 was given food 4
% constraint fed[1, 4] == 4; % ORIG
constraint fed[1, 2] == 4; % hakank

% Before test flight 2, reindeer 2 was given food 4
% constraint fed[2, 4] == 4;  % ORIG
constraint fed[2, 2] == 4; % hakank

% Before test flight 3, reindeer 2 was given food 6
% constraint fed[3, 4] == 6; % ORIG
constraint fed[3, 2] == 6;  % hakank

现在模型输出唯一的解决方案：

Favourites    = [1, 4, 3, 1, 9, 6, 8, 3, 5]
Test flight 1 = [1, 4, 3, 7, 9, 6, 8, 3, 6]
Test flight 2 = [1, 4, 3, 7, 9, 6, 8, 2, 5]
Test flight 3 = [1, 6, 3, 7, 9, 6, 4, 3, 1]
----------
==========

有一种方法可以在 MiniZinc 中系统地调试 UNSAT 模型：使用 findMUS 求解器（MUS=最小不可满足子集）。它可能会显示冲突的地方。在此处查看有关 findMUS 的更多信息：https ://www.minizinc.org/doc-2.5.5/en/find_mus.html

我实际上首先尝试了 findMUS，但在这种情况下它没有多大帮助。相反，我查看了所有线索并与限制条件进行了比较。