Guan Yu finally escaped from Cao Cao's control, and arrived at the rest point outside of Liu Bei's city. After hearing about this, Liu Bei, together with a small troop of soldiers, went to the rest point to welcome His brother. Surprisingly, Liu Bei's messenger reported that Xiahou Dun, the general in Cao Cao's camp, had been chasing Guan Yu and was approaching the rest point with the trooper soldiers. Liu Bei was so excited about seeing Guan Yu that he had brought fewer soldiers along with him compared to those of Xiahou Dun. In such an emergency, and in order to scare Xiahou Dun, Zhang Fei proposed to insert strawmen among the soldiers to fake a large troop. Soldiers and strawmen were arranged in a grid-like formation. There was to be at least one soldier adjacent to a strawman to hold it straight. [MUSIC] The straw men were all of the same height, so if the soldiers standing in front were shorter, then it would be too easy to notice them. Therefore, at least one taller soldier had to stand in front a strawman. The brothers needed to fake as large an army as possible with the straw men that they had. Guan Yu pulled out the tablet but it failed to provide a solution after a long while. And thus Guan Yu called for help. [SOUND] >> So in his excitement to meet Guan Yu, Liu Bei has rushed out with only a small number of troops. Unfortunately his scout reports that Xiahou Dun is following, chasing Guan Yu with a large army. So Zhang Fei has an idea. Why don't we parade with a whole lot of straw soldiers to make it look like we've got a much larger number of troops than we actually have? And that will prevent us from being attacked. So, we're going to set out soldiers in a grid formation, the way we normally parade. And we're going to need a real soldier next to each straw soldier. Otherwise, they're too likely to fall over, and that would give away the game. So they can be in front or behind, as long as there's one real soldier next to every straw soldier. So basically, we can't have this kind of pattern of five straw soldiers in a cross. because the middle straw soldier doesn't have any real soldier next to them. Now the strawmen are all of equal height but we have to be careful Xiahou Dun, if he sees a line up like this, then he's going to notice this straw soldier is obviously not real and the game will be up. That's because all of the real soldiers in front of the straw soldier are too small. So this is not going to be allowed. What we need is just to have at least one real soldier in front of every straw soldier who's taller than the straw soldier. And it doesn't matter where that real soldier is as long as there's one then Xiahou Dun will not be able to see the straw soldier. And we're going to try to put together a whole parade as big as possible so that each straw solider is covered up. There's always a tall soldier in front. Now we're trying to maximize the apparent size of this army so we're trying to use the maximum number of rows and columns so if we multiply those two together that gives the apparent size of the army. So here's a summary of this. We are going to fill the parade with nrows and ncolumns and those are going to be decisions. That's how big the apparent army's going to look. We have all straw soldiers have the same straw height. Each straw soldier has a real soldier adjacent to them. No straw soldiers have only soldiers of less or equal height in front of them, and objective is to maximize this apparent number of soldiers which is the number rows times the number of columns that we use. Now in order to model this we're going to have to pick some maximum number of columns and maximum number rows to fit our parade into. So that's going to be some starting data. So let's look at the data and decisions of our model. So we've got a number of soldiers, let's call that type SOLDIER. But we're also going to use an extra soldier, SOLDIER0 to represent either an empty position or a straw soldier. So we're introducing this set SOLDIER0 to do that. For the real soldiers we have the height and then we have a maximum number of rows and number of maximum columns that we're going to be interested in laying out our parade. And the key decision are this, in every row and column we're going to put some kind of soldier. Now, it could be 0. It will either represent a straw soldier, or it will represent an empty position, if we're not using those rows and columns at all. And the other decisions, the key decisions, are how many rows are we using, and how many columns are we using? And basically, if we see a 0 inside this row, nrow by ncol, that we're using, it'll represent a straw soldier. If we see it outside this, it'll represent an empty position. So let's look at our constraints. We need that every real soldier appears at most once, so we can look at any two positions r1, c1 and r2, c2 that are different, right? So at least one of the two, the row or the column has to be different, and then either It has no real soldier in it, so it's either a straw soldier or empty. Or the two soldiers in these two positions, one of them is empty or the two soldiers in these positions are different. Notice if r2, c2 was 0 and r, c1 was not 0, then this would automatically hold anyway. Right, so, that's one way of modeling this constraint, it's very direct but it's very inefficient. So, we're going duplicate this 0 condition many, many times. Right, so, we're going to duplicate it for each r2 and c2, we're going to actually build this constraint again. And we're going to constrain each pair of r1, c1 and r2,c2 twice because if we switch r1 with r2 and c1 with c2 we're going to build the same not equals constraint anyway. So when we're building models, we need to make sure that when we're building loops that they're as efficient as possible. That means we don't create the same constraint multiple times, and we try to make the loops as small as they are needed. And also we add test or constraints into the loop as early as possible, so that they're only used once, or so they can constrain the loop as soon as it's possible. So let's have a different way of building this parade constraints, so here we're going to look through the positions in the whole parade around. So this from 1 maxrow to maxcolumn, and i is going to be the first position we're considering and j is going to be the second one. And now we've order all those positions so we're only going to look at j walues which are bigger than i. So now we're not going to have this possibility of seeing the same position twice. We're going to take that position and work out which row and column it refers to using some local variables. And now we can do our constraint. So basically either this first position we're looking at is empty, in which case there's not going to be any problem, we don't have any further constraints. Or we have to look at all the further positions. So we know now that this position i or r1, c1 has a real soldier in it. And we have to make sure that all the further positions have a different soldier in them. And again, we're just iterating over the different positions. And converting that position number into a row and column number. All right, so this is good. It iterates over position numbers. It only tests this = 0 once for each position. And it only constrains each pair of i and j once. The two positions are only constrained once. So that's good, but is there a better way? So, a key thing that we've seen throughout this course is that we have global constraints which could be very effective. They can make our model smaller and they can make our model solve much more efficiently. So we need to be familiar with the globals library and look for cases for using a lot at global. And notice that even if we actually use a global which is implemented by decomposition, so our server doesn't support it natively. At least it will be a different decomposition tailored to that solver and it's likely to be reasonable at least. So, actually there's exactly a global constraint to do what we want here. All we want is that in each position in this parade ground every real soldier, so every number except 0, occurs once. So all the numbers in this array are different except 0 which can occur any number of times. So here, our global is doing exactly what we want. All right, so we need to be aware of what's in the library so we don't miss out on the opportunity to doing this, because this will be much more efficient than any of the previous examples. Now, we need also that each real soldier appears at least once, so we're not leaving out any soldiers. So we could do this directly by saying, for every soldier, there exists some position which has that soldier there. Now, that's very inefficient. It's a direct translation of the constraint, but it's highly conjunctive. It's building this exists, big exists over all possible positions for every soldier. Can we use a global? Yes we can, so remember the global cardinality family constraints are about counting things. And here we just have to count the number of times that a soldier occurs. So we're looking at all of the different positions, and we're going to count the number of times all the different soldiers occur, and each soldier has to occur exactly once. So there's a global_cardinality constraint doing exactly what we want. In fact, this encodes the previous constraint as well. It also encodes that each soldier appears exactly once. So we could remove the alldifferent_except_0 constraint as well. But in this case, we might also find a simpler way. And that's because really, once we know that all the real soldiers appearing in the parade are different, then we can just count up the number of real soldiers that appear. So that's just looking over the whole parade group and counting the number of real soldiers. And if that's equal to the number of soldiers, then we know that every real soldier appears at least once. So I think this is a much simpler constraint than the global cardinality constraint, and it'll do what we need. So this relies, of course, on the all different except 0 to make sure that all the soldiers appearing are different. But in this case once we've got that we can do this much more simply. All right, we need to make sure that each real soldier appears in the area nrow*ncol area of the parade. So that's easy enough, we look at every position. If it's in a row that's too late, then we force it to be empty. If it's in a column that's too late, we also force it to be empty. So that's straightforward. All right, we need that each straw soldier has a real soldier adjacent to them. And this is fairly straightforward, but a bit complicated. We look in every position, and if it's got a straw soldier in it, so it's in the real parade area and it's equal to 0, that makes it a strong soldier. And then we're going to have to look, so we have to be careful here, if the column is less than the max column. So there is actually a soldier to the right, then we want to make sure that the soldier to the right is not, is a real soldier. Or, if we're not at the first column, then we have to look at the column, that soldier to the left. That should be a real soldier. Or, if we're not in the last row, then we look at the soldier behind us. That could be a real soldier. Or, if we're not in the first row then we look at the soldier in front of us, and that should be a real soldier. So there's our disjunction of one of the four positions around us. And there may be less than four positions around us depending on whether we're at the edge of this parade ground has to have a real soldier. All right, let's look at this constraint. No straw soldier has only soldiers of less or equal height in front of it. So we can write this more or less directly by saying well, it's not the case that there is some position which is in the real parade ground, right, where there's a straw soldier. Because 0 in this real parade ground area means a straw soldier. So there's no position r1, c, which has a straw soldier, such that if we looked at all the rows where the rows in front of where it is, so r2 less than r1, there's either a straw soldier or the height of the real soldier there is less than or equal to the straw height. So that's making sure that there's someone as no exactly this statement, no straw soldier has only soldiers of less or equal height in front of them. Right, so we should look at this and be aware that this r2 < r1 is fixed. See, r1 is going to be fixed by this loop and r2 is going to be fixed by this loop, so actually we can move this check into the loop. So the first thing we can do is that. We only have to iterate over all the rows in front of row r1. So that makes out loop better but it's still inefficient. We can see this disjunction here in the inner loop. So every time this is going to create a large set of constraints and this disjunction in these loops is going to create a lot of disjunctions. Can we do better than that? Well, sometimes it's worth adding extra data into our model that allows us to write simple constraints. And we sort of sometimes doing something where we'd hope common subexpression elimination might find, that we're building similar constraints and do it once, but if we do it ourselves then we know it's going to be better. So in our case here, we can think about a different way about talking about that constraint about equal height. So all we need to do is build an extended height array. So this, our height array, maps all kinds of soldiers, real soldiers and straw soldiers, to their height. And that's very simple, we just take the height array of the real soldiers add the strawheight on the front and we need to change that back to have the right index set which is from 0 to the number of soldiers. Now, we can express this inner loop much more simply because we just look at the extended height of the soldier whoever they are. And that has to be listed with the strawheight. That's the same as saying either there was a straw solider there, which would have given us that this was true because strawheight is less than or equal to strawheight. Or there's a real soldier there and then we're checking whether their height is less than or equal to strawheight. And this is good, but negation, this negation at the front here, is terribly hard for solvers. So things we should try to avoid when we're modeling are negations, so solvers definitely do not like negation, and if we can, we should try to replace negation with the negated form. So if we have not x = y, much more efficient to write x not equal to y. Similarly disjunctions, so you will need to use disjunction to express complicated things in discrete optimization. But we try to make them as simple as possible, and similarly implication right? This has got a negation and a disjunction in it, so we want to make this This constraint here as simple as possible. And existential loops of course are just large numbers of disjunctions. So all of these things we're trying to avoid because essentially a solver only takes a conjunction of constraints, so all of these things have to be mapped to conjunctions in some way. And that makes the solving harder. So an example here, we can actually easily push this negation inside this exists, which becomes a forall, and push it further in and we get a much more efficient set of constraints. So now we're saying, forall rows and columns, if there is a straw soldier there, then there must exist some row in front of that soldier which has a height greater than the straw soldier's height. So we've basically pushed the negation through these quantifiers to get a much more efficient version of the same constraint. All right, we need to maximize the number of apparent soldiers. And if we do so, now we can solve our model. It's quite a challenging model still to be solved. And for the particular data that we're using or get 6 rows and 7 columns. And you'll see this kind of pattern where we have tall soldiers at the front making sure that all the soldiers behind are covered. And then we're carefully spreading out soldiers around so that every straw soldier is supported by one of these real soldiers. So there's our area of 6 times 7. So, we need to remember when we're modeling, constraints always take a set of variables and a conjunction of constraints. That's the only thing that they finally get, and they return an answer. So they're designed to handle problems of this form, and models can look very different to that, because we use things like misnegation, disjunction, and it for all exists. And so, if models have simple conjunctions, it's much easier to solve and we need to translate the other contracts into these simple conjunctions. And that makes it much more difficult to solve so if we can avoid using things like negation and disjunction. And we going to have likely to have a model just much more efficient. So, one last thing to think about, in terms of model improvement, generally the larger the model is, the more difficult it is to solve. So this tells us we should make use of global constraints, they will tend to keep our models much smaller. Although we have to be aware that sometimes we'll use a global, and it'll be decomposed without us noticing it. And if we want to look at how big the model going to the solver is, we can run minizinc with -k, or in the IDE we can set that in the preferences to keep the files. And we can actually examine the size of the FlatZinc file, and that'll sort of tell us how big the solver. What is being sent to the solver. We can look at the different models and different FlatZinc sizes and generally we'd expect that the smallest sizes are likely to be better models. So in summary, there are lots of ways to model problem and effectively the key skill we're trying to give you in this course is to be able to build good models for the problem. Because the difference between a good model and a bad model can be exponential in the amount of time it takes to solve. So things like avoiding negation disjunction exists. And bool2int, which is another form of negation, really. Unless they're very, very, simple. So we typically use bool2int to enter very, very, simple things and that's fine. All right, the size of the models matter, so we need to make our loops as tight as possible. We need to make them as efficient as possible. We need to able to discover that there's some useful intermediate that we could make and model more efficient for, whether it's fixed or variable, and reuse that. We need to look for other ways to model our constraints. The very first way we do it may not be the right way. We need to be aware of that.