当我知道有解决方案时，约束报告为不满足（菜鸟错误？）
Constraints reported as UNSATISFIABLE when I know there is a solution (rookie error?)
作为第一次使用 MiniZinc 的用户，我曾尝试用它编写一个我已经知道解决方案的逻辑难题。但是，当我尝试编写所有拼图线索和 运行 代码时，它会报告 =====UNSATISFIABLE=====。下面的代码 运行s 但如果两个注释掉的约束中的任何一个未被注释，则找不到解决方案。
很可能是我在某处犯了错误，但我正在努力寻找它。非常感谢任何帮助！
% Christmas Puzzle 2021
include "alldifferent.mzn";
% There are 9 reindeer numbered 1 to 9 and there are 9 different types of food.
% The reindeer fly on three test flights and are fed one of the foods prior to
% each test flight.
set of int: REINDEER = 1..9;
set of int: FOOD = 1..9;
set of int: FLIGHT = 1..3;
% Each reindeer has a favourite food
array[REINDEER] of var FOOD: favourite;
array[FLIGHT, REINDEER] of var FOOD: fed;
%%% CLUES %%%
% Reindeer 2’s favourite food is 4
constraint favourite[2] == 4;
% Before test flight 1, reindeer 2 was given food 4
constraint fed[1, 4] == 4;
% Before test flight 2, reindeer 2 was given food 4
constraint fed[2, 4] == 4;
% Before test flight 3, reindeer 2 was given food 6
constraint fed[3, 4] == 6;
% Before test flight 3, a total of 4 reindeer were given the wrong food
constraint count([fed[3, r] - favourite[r] | r in REINDEER], 0, 5);
% Reindeer 4’s favourite food is a factor of 607
constraint favourite[4] == 1;
% Reindeer 4 was given the same food before all three test flights.
constraint fed[1, 4] == fed[2, 4];
% =====UNSATISFIABLE=====
%constraint fed[1, 4] == fed[3, 4];
% Before test flight 1, reindeer 8 was given food 3
constraint fed[1, 8] == 3;
% Before test flight 1, a total of 2 reindeer were given the wrong food.
constraint count([fed[1, r] - favourite[r] | r in REINDEER], 0, 7);
% Before test flight 1, reindeer 9 was given food 6
constraint fed[1, 9] == 6;
% Before test flight 2, reindeer 9 was given food 5
constraint fed[2, 9] == 5;
% Before test flight 3, reindeer 9 was given food 1
constraint fed[3, 9] == 1;
% Before test flight 2, reindeer 4 was not given food 9
constraint fed[2, 4] != 9;
% Before test flight 2, 2 reindeer were given the wrong food
% =====UNSATISFIABLE=====
%constraint count([fed[2, r] - favourite[r] | r in REINDEER], 0, 7);
% Reindeer 1 was given food 1 before all three test flights
constraint fed[1, 1] == 1;
constraint fed[2, 1] == 1;
constraint fed[3, 1] == 1;
% Before test flight 2, all the reindeer were given different foods
constraint all_different([fed[2, r] | r in REINDEER]);
% Before test flight 1, reindeer 7 was not given food 7
constraint fed[1, 7] != 7;
% Before test flight 2, reindeer 8 was given food 2
constraint fed[2, 8] == 2;
% Before test flight 3, reindeer 5 was not given food 7
constraint fed[3, 5] !=7;
% Before test flight 3, 3 reindeer had the food equal to their number
constraint count([fed[3, r] - r | r in REINDEER], 0, 3);
% Before test flight 3, reindeer 7 was given food that is a factor of 148
constraint fed[3, 7] == 1 \/ fed[3, 7] == 2 \/ fed[3, 7] == 4;
% Before test flight 3, reindeer 7 was not given food 1
constraint fed[3, 7] != 1;
% Before test flight 3, no reindeer was given food 2
constraint forall([fed[3, r] != 2 | r in REINDEER]);
% Before test flight 1, reindeer 7 was not given food 9
constraint fed[1, 7] != 9;
solve satisfy;
output [
"Favourites = ", show(favourite), "\n",
"Test flight 1 = ", show([fed[1, r] | r in REINDEER]), "\n",
"Test flight 2 = ", show([fed[2, r] | r in REINDEER]), "\n",
"Test flight 3 = ", show([fed[3, r] | r in REINDEER]), "\n"
];
请注意，以下结果应该满足所有线索：
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]
我不知道是否有通过从该解决方案向后工作以查看未满足哪些约束（如果有）的调试方法。
第一个约束中有一些拼写错误，可能是 copy/paste 个问题。以下是更改：
% 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=Minimal Unsatisfiable Subsets）。它可能会显示冲突的地方。在此处查看有关 findMUS 的更多信息：https://www.minizinc.org/doc-2.5.5/en/find_mus.html
实际上我首先尝试了 findMUS，但在这种情况下并没有太大帮助。相反，我查看了所有线索并与约束条件进行了比较。
以下模型按预期工作：
% Christmas Puzzle 2021
include "alldifferent.mzn";
% There are 9 reindeer numbered 1 to 9 and there are 9 different types of food.
% The reindeer fly on three test flights and are fed one of the foods prior to
% each test flight.
set of int: REINDEER = 1..9;
set of int: FOOD = 1..9;
set of int: FLIGHT = 1..3;
% Each reindeer has a favourite food
array[REINDEER] of var FOOD: favourite;
array[FLIGHT, REINDEER] of var FOOD: fed;
%%% CLUES %%%
% Reindeer 2’s favourite food is 4
constraint favourite[2] == 4;
% Before test flight 1, reindeer 2 was given food 4
% constraint fed[1, 4] == 4;
% changed reindeer from 4 to 2
constraint fed[1, 2] == 4;
% Before test flight 2, reindeer 2 was given food 4
% constraint fed[2, 4] == 4;
% changed reindeer from 4 to 2
constraint fed[2, 2] == 4;
% Before test flight 3, reindeer 2 was given food 6
% constraint fed[3, 4] == 6;
% changed reindeer from 4 to 2
constraint fed[3, 2] == 6;
% Before test flight 3, a total of 4 reindeer were given the wrong food
% constraint count([fed[3, r] - favourite[r] | r in REINDEER], 0, 5);
constraint 4 == sum([fed[3, r] != favourite[r] | r in REINDEER]);
% Reindeer 4’s favourite food is a factor of 607
% 607 is a prime number
constraint favourite[4] == 1;
% Reindeer 4 was given the same food before all three test flights.
% constraint fed[1, 4] == fed[2, 4];
% =====UNSATISFIABLE=====
% constraint fed[1, 4] == fed[3, 4];
constraint forall([fed[1, 4] == fed[f, 4] | f in FLIGHT]);
% Before test flight 1, reindeer 8 was given food 3
constraint fed[1, 8] == 3;
% Before test flight 1, a total of 2 reindeer were given the wrong food.
% constraint count([fed[1, r] - favourite[r] | r in REINDEER], 0, 7);
constraint 2 == sum([fed[1, r] != favourite[r] | r in REINDEER]);
% Before test flight 1, reindeer 9 was given food 6
constraint fed[1, 9] == 6;
% Before test flight 2, reindeer 9 was given food 5
constraint fed[2, 9] == 5;
% Before test flight 3, reindeer 9 was given food 1
constraint fed[3, 9] == 1;
% Before test flight 2, reindeer 4 was not given food 9
constraint fed[2, 4] != 9;
% Before test flight 2, 2 reindeer were given the wrong food
% =====UNSATISFIABLE=====
%constraint count([fed[2, r] - favourite[r] | r in REINDEER], 0, 7);
constraint 2 == sum([fed[2, r] != favourite[r] | r in REINDEER]);
% Reindeer 1 was given food 1 before all three test flights
constraint fed[1, 1] == 1;
constraint fed[2, 1] == 1;
constraint fed[3, 1] == 1;
% Before test flight 2, all the reindeer were given different foods
constraint all_different([fed[2, r] | r in REINDEER]);
% Before test flight 1, reindeer 7 was not given food 7
constraint fed[1, 7] != 7;
% Before test flight 2, reindeer 8 was given food 2
constraint fed[2, 8] == 2;
% Before test flight 3, reindeer 5 was not given food 7
constraint fed[3, 5] !=7;
% Before test flight 3, 3 reindeer had the food equal to their number
% constraint count([fed[3, r] - r | r in REINDEER], 0, 3);
constraint 3 == sum([fed[1, r] == r | r in REINDEER]);
% Before test flight 3, reindeer 7 was given food that is a factor of 148
% 148 = 2 x 2 x 37 = 4 x 37 = 1 x 148
% constraint fed[3, 7] == 1 \/ fed[3, 7] == 2 \/ fed[3, 7] == 4;
constraint fed[3, 7] in {1, 2, 4};
% Before test flight 3, reindeer 7 was not given food 1
constraint fed[3, 7] != 1;
% Before test flight 3, no reindeer was given food 2
constraint forall([fed[3, r] != 2 | r in REINDEER]);
% Before test flight 1, reindeer 7 was not given food 9
constraint fed[1, 7] != 9;
solve satisfy;
output [
"Favourites = ", show(favourite), "\n",
"Test flight 1 = ", show([fed[1, r] | r in REINDEER]), "\n",
"Test flight 2 = ", show([fed[2, r] | r in REINDEER]), "\n",
"Test flight 3 = ", show([fed[3, r] | r in REINDEER]), "\n"
];
作为第一次使用 MiniZinc 的用户，我曾尝试用它编写一个我已经知道解决方案的逻辑难题。但是，当我尝试编写所有拼图线索和 运行 代码时，它会报告 =====UNSATISFIABLE=====。下面的代码 运行s 但如果两个注释掉的约束中的任何一个未被注释，则找不到解决方案。
很可能是我在某处犯了错误，但我正在努力寻找它。非常感谢任何帮助！
% Christmas Puzzle 2021
include "alldifferent.mzn";
% There are 9 reindeer numbered 1 to 9 and there are 9 different types of food.
% The reindeer fly on three test flights and are fed one of the foods prior to
% each test flight.
set of int: REINDEER = 1..9;
set of int: FOOD = 1..9;
set of int: FLIGHT = 1..3;
% Each reindeer has a favourite food
array[REINDEER] of var FOOD: favourite;
array[FLIGHT, REINDEER] of var FOOD: fed;
%%% CLUES %%%
% Reindeer 2’s favourite food is 4
constraint favourite[2] == 4;
% Before test flight 1, reindeer 2 was given food 4
constraint fed[1, 4] == 4;
% Before test flight 2, reindeer 2 was given food 4
constraint fed[2, 4] == 4;
% Before test flight 3, reindeer 2 was given food 6
constraint fed[3, 4] == 6;
% Before test flight 3, a total of 4 reindeer were given the wrong food
constraint count([fed[3, r] - favourite[r] | r in REINDEER], 0, 5);
% Reindeer 4’s favourite food is a factor of 607
constraint favourite[4] == 1;
% Reindeer 4 was given the same food before all three test flights.
constraint fed[1, 4] == fed[2, 4];
% =====UNSATISFIABLE=====
%constraint fed[1, 4] == fed[3, 4];
% Before test flight 1, reindeer 8 was given food 3
constraint fed[1, 8] == 3;
% Before test flight 1, a total of 2 reindeer were given the wrong food.
constraint count([fed[1, r] - favourite[r] | r in REINDEER], 0, 7);
% Before test flight 1, reindeer 9 was given food 6
constraint fed[1, 9] == 6;
% Before test flight 2, reindeer 9 was given food 5
constraint fed[2, 9] == 5;
% Before test flight 3, reindeer 9 was given food 1
constraint fed[3, 9] == 1;
% Before test flight 2, reindeer 4 was not given food 9
constraint fed[2, 4] != 9;
% Before test flight 2, 2 reindeer were given the wrong food
% =====UNSATISFIABLE=====
%constraint count([fed[2, r] - favourite[r] | r in REINDEER], 0, 7);
% Reindeer 1 was given food 1 before all three test flights
constraint fed[1, 1] == 1;
constraint fed[2, 1] == 1;
constraint fed[3, 1] == 1;
% Before test flight 2, all the reindeer were given different foods
constraint all_different([fed[2, r] | r in REINDEER]);
% Before test flight 1, reindeer 7 was not given food 7
constraint fed[1, 7] != 7;
% Before test flight 2, reindeer 8 was given food 2
constraint fed[2, 8] == 2;
% Before test flight 3, reindeer 5 was not given food 7
constraint fed[3, 5] !=7;
% Before test flight 3, 3 reindeer had the food equal to their number
constraint count([fed[3, r] - r | r in REINDEER], 0, 3);
% Before test flight 3, reindeer 7 was given food that is a factor of 148
constraint fed[3, 7] == 1 \/ fed[3, 7] == 2 \/ fed[3, 7] == 4;
% Before test flight 3, reindeer 7 was not given food 1
constraint fed[3, 7] != 1;
% Before test flight 3, no reindeer was given food 2
constraint forall([fed[3, r] != 2 | r in REINDEER]);
% Before test flight 1, reindeer 7 was not given food 9
constraint fed[1, 7] != 9;
solve satisfy;
output [
"Favourites = ", show(favourite), "\n",
"Test flight 1 = ", show([fed[1, r] | r in REINDEER]), "\n",
"Test flight 2 = ", show([fed[2, r] | r in REINDEER]), "\n",
"Test flight 3 = ", show([fed[3, r] | r in REINDEER]), "\n"
];
请注意，以下结果应该满足所有线索：
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]
我不知道是否有通过从该解决方案向后工作以查看未满足哪些约束（如果有）的调试方法。
第一个约束中有一些拼写错误，可能是 copy/paste 个问题。以下是更改：
% 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=Minimal Unsatisfiable Subsets）。它可能会显示冲突的地方。在此处查看有关 findMUS 的更多信息：https://www.minizinc.org/doc-2.5.5/en/find_mus.html
实际上我首先尝试了 findMUS，但在这种情况下并没有太大帮助。相反，我查看了所有线索并与约束条件进行了比较。
以下模型按预期工作：
% Christmas Puzzle 2021
include "alldifferent.mzn";
% There are 9 reindeer numbered 1 to 9 and there are 9 different types of food.
% The reindeer fly on three test flights and are fed one of the foods prior to
% each test flight.
set of int: REINDEER = 1..9;
set of int: FOOD = 1..9;
set of int: FLIGHT = 1..3;
% Each reindeer has a favourite food
array[REINDEER] of var FOOD: favourite;
array[FLIGHT, REINDEER] of var FOOD: fed;
%%% CLUES %%%
% Reindeer 2’s favourite food is 4
constraint favourite[2] == 4;
% Before test flight 1, reindeer 2 was given food 4
% constraint fed[1, 4] == 4;
% changed reindeer from 4 to 2
constraint fed[1, 2] == 4;
% Before test flight 2, reindeer 2 was given food 4
% constraint fed[2, 4] == 4;
% changed reindeer from 4 to 2
constraint fed[2, 2] == 4;
% Before test flight 3, reindeer 2 was given food 6
% constraint fed[3, 4] == 6;
% changed reindeer from 4 to 2
constraint fed[3, 2] == 6;
% Before test flight 3, a total of 4 reindeer were given the wrong food
% constraint count([fed[3, r] - favourite[r] | r in REINDEER], 0, 5);
constraint 4 == sum([fed[3, r] != favourite[r] | r in REINDEER]);
% Reindeer 4’s favourite food is a factor of 607
% 607 is a prime number
constraint favourite[4] == 1;
% Reindeer 4 was given the same food before all three test flights.
% constraint fed[1, 4] == fed[2, 4];
% =====UNSATISFIABLE=====
% constraint fed[1, 4] == fed[3, 4];
constraint forall([fed[1, 4] == fed[f, 4] | f in FLIGHT]);
% Before test flight 1, reindeer 8 was given food 3
constraint fed[1, 8] == 3;
% Before test flight 1, a total of 2 reindeer were given the wrong food.
% constraint count([fed[1, r] - favourite[r] | r in REINDEER], 0, 7);
constraint 2 == sum([fed[1, r] != favourite[r] | r in REINDEER]);
% Before test flight 1, reindeer 9 was given food 6
constraint fed[1, 9] == 6;
% Before test flight 2, reindeer 9 was given food 5
constraint fed[2, 9] == 5;
% Before test flight 3, reindeer 9 was given food 1
constraint fed[3, 9] == 1;
% Before test flight 2, reindeer 4 was not given food 9
constraint fed[2, 4] != 9;
% Before test flight 2, 2 reindeer were given the wrong food
% =====UNSATISFIABLE=====
%constraint count([fed[2, r] - favourite[r] | r in REINDEER], 0, 7);
constraint 2 == sum([fed[2, r] != favourite[r] | r in REINDEER]);
% Reindeer 1 was given food 1 before all three test flights
constraint fed[1, 1] == 1;
constraint fed[2, 1] == 1;
constraint fed[3, 1] == 1;
% Before test flight 2, all the reindeer were given different foods
constraint all_different([fed[2, r] | r in REINDEER]);
% Before test flight 1, reindeer 7 was not given food 7
constraint fed[1, 7] != 7;
% Before test flight 2, reindeer 8 was given food 2
constraint fed[2, 8] == 2;
% Before test flight 3, reindeer 5 was not given food 7
constraint fed[3, 5] !=7;
% Before test flight 3, 3 reindeer had the food equal to their number
% constraint count([fed[3, r] - r | r in REINDEER], 0, 3);
constraint 3 == sum([fed[1, r] == r | r in REINDEER]);
% Before test flight 3, reindeer 7 was given food that is a factor of 148
% 148 = 2 x 2 x 37 = 4 x 37 = 1 x 148
% constraint fed[3, 7] == 1 \/ fed[3, 7] == 2 \/ fed[3, 7] == 4;
constraint fed[3, 7] in {1, 2, 4};
% Before test flight 3, reindeer 7 was not given food 1
constraint fed[3, 7] != 1;
% Before test flight 3, no reindeer was given food 2
constraint forall([fed[3, r] != 2 | r in REINDEER]);
% Before test flight 1, reindeer 7 was not given food 9
constraint fed[1, 7] != 9;
solve satisfy;
output [
"Favourites = ", show(favourite), "\n",
"Test flight 1 = ", show([fed[1, r] | r in REINDEER]), "\n",
"Test flight 2 = ", show([fed[2, r] | r in REINDEER]), "\n",
"Test flight 3 = ", show([fed[3, r] | r in REINDEER]), "\n"
];