As a first-time MiniZinc user I have tried to use it to code up a logic puzzle I already know the solution to. However, when I attempt to code up all of the puzzle clues and run the code it reports back =====UNSATISFIABLE=====. The code below runs but if either of the two commented out constraints are uncommented the solution is not found.
It's more than likely that I've made a mistake here somewhere but I am struggling to find it. Any help greatly appreciated!
% 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"
];
Note that the following results should satisfy all of the clues:
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]
I don't know if there's a way to debug by working backwards from this solution to see which constraints (if any) are not met.
There are some typos in the first constraints, probably copy/paste issues. Here are the changes:
% 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
Now the model outputs the unique solution:
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]
----------
==========
There is one way to debug an UNSAT model systematically in MiniZinc: using the findMUS solver (MUS=Minimal Unsatisfiable Subsets). It might show places of the conflicts. See more about findMUS here: https://www.minizinc.org/doc-2.5.5/en/find_mus.html
I actually tried findMUS first, but it didn't help much in this case. Instead, I looked through all the clues and compared with the constraints.