Liu Bei, Guan Yu, and Zhang Fei wanted to borrow horses from a wealthy man,
Zhang Shiping, to help suppress the Yellow Turban army.
Zhang Shiping wondered if the brothers were talented enough
to make good use of his horses for the suppression.
He decided to give them a problem and
promise to let them borrow the horses if they could solve it.
The problem was to color a map of the Han Dynasty, using at most four colors,
such that the adjacent states didn't share the same color.
Lupe thought for quite a while about the problem but was unable to solve it.
So urgent was the need to borrow the horses that he sought help using
the magical tablet.
[SOUND] >>
So, our three heroes are interested in building a stronger army.
And so they go to visit Zhang Shiping in order to see if he'll sponsor them for
horses.
But Zhang Shiping is a wise man and he sets them a challenge first to show
that if he's going to sponsor them, then they are going to show
the capabilities that's going to be able to defeat the Yellow Turban Rebels.
So he gives them this map of the Han Dynasty and says, four-color this map.
So let's look at MiniZinc model to color this map.
So here we have an enumerated type COLOR, which is made up of four different colors,
green, blue, pink, and yellow.
And each of the different provinces is declared
as a variable of this enumerated type COLOR.
So province Si, we're going to have to decide which color to color that province,
and the same all the rest of the provinces.
Now we have to write down the constraints of the map.
So any two provinces which are next to each other
we have to make sure that they have a different color.
And so we've written down all of those constraints.
You can see that there are so many that we've gone through a very small font size.
Let's just look at a few of them.
So, the province Liang is next to the province Yong and so
we've written this constraint here, the constraint Liang is not equal to Yong.
And similarly, the province Yong is next to province Yi.
So I've written that constraint, Yong is not equal to Yi.
The province Yong is next
to the province Jing so I've written that constraint, Yong is not equal to Jing.
And the province Yong is next to Si and so we've written this constraint,
Yong is not equal to Si.
And we write down all the rest of these neighbor relationships
between the different provinces.
We will solve satisfy,
we're just trying to find one particular solution to the map coloring problem.
And we can this run MiniZinc model and will result in the coloring.
Able to print out all the different colors of the map.
Notice we didn't need an output function and we're just going to get for
each particular province which color it got.
And if we look at the result we'll see a correct coloring of the map
where every province is colored different to every neighbor.
So, what we've seen here is a new feature
of MiniZinc which is enumerated types.
So enumerated types are a way of defining a finite set of named objects, and
then we can make decisions and parameters can be then about these enumerated types.
And array indices which we'll introduce later can also be over these enumerator
types and we can also choose sets over these enumerated types,
which we'll see shortly.
So they're declared by this enum and
then the name of the enumerated type and then they're defined by this equality,
enum-name is then given this set of identifiers.
So we got the example of the set of different colors that we were given.
And then we can declare the variables by this var, and the name of enumerated type.
And then variable name, or if we don't have the var in, it's a parameter,
and we're just picking a particular fixed version of this enumerated type.
So we could modify our program to have a different enumerated type.
Let's call it green, blue, and pink.
So can we color this map with just three colors?
And we could run our MiniZinc model then,
we will result in this, unsatisfiable, right?
So this is a new kind of output we haven't seen before, and
it should be fairly clear what it means.
It means that there is no way of three coloring
the map of the Han Dynasty provinces.
So we know if you know that there's a four color map theorem says there's always
a way of four coloring a plain out map like this one.
But there's no way of coloring this map with three colors.
And so our MiniZinc, our solver is telling us there is
no possible way of solving this problem and getting back the result unsatisfiable.
So in this lecture we've introduced enumerated types which is a way of
introducing a named set of objects.
So their real importance is that they introduce a notion of type safety
of models.
If I have two different sets of objects that I'm making decisions about,
then I don't want to mix them up.
I don't want to make decisions about this one when I meant to be making
decisions about that one.
So enumerated types will in fact map down in the solvers to be integers.
We could have used the numbers one to four to color our map,
instead of these color names.
And in fact the numbers one to four is what the solver will see
when it sees this problem, but by using this name type, we not only get
a model which is easier to understand, but we also get this notion of type safety.
Which will help us later on with more complicated models.
We also saw for the first time an unsatisfiable model.
We have to be clear that not every model has a solution, so
sometimes we'll ask to find a solution, there will be none.
More often, an unsatisfiable model will arise because we typed in a model
incorrectly, there's a bug in our model or a bug in our data, and
unsatisfiable will be a trigger for us to try and find out what's going wrong.
And the problem we solved here was graph coloring,
this is a very classic problem in graph theory.
It has applications in register allocation, in compilers, in timetabling,
a lot of other things.
And, of course, as I'll usually say,
pure graph coloring is better handled by specialized algorithms.
So lots of problems in graph theory are being studied intensely,
like graph coloring.
And if you are featuring a pure graph coloring problem, and
you should use a specialized algorithm.
But if we add some side constraints about how specific parts of the graph should be
colored, then using a general discrete optimization approach like MiniZinc,
is the way to go.