Yuan Shao had an army with many soldiers, presenting a challenge for Cao Cao's army that had fewer soldiers. Zhang Liao, a general in Cao's camp, recommended the cavalry wedge formation, which would help split and weaken Yuan Shao's army during any forceful charge or attack. The Calvary wedge formation is established by arranging odd numbers of forces and soldiers in the shape of a wedge. To keep this formation every horse needed to run faster than the one behind it. Also, each soldier posted to the front of the formation had a larger chance of fighting with the enemy. And thus needed to have a higher endurance rating than the one behind it. Only some of his horses and soldiers were compatible to pair up with each other. Faced with determining the best possible wedge formation in order to maximize the strength of the cavalry, Guan Yu offered to solve this problem using the magical tablet. Unfortunately, it failed to provide a solution, so again, he called for some help, [MUSIC] >> So Cao Cao is interested in having the strongest possible attack formation he can, so this gives us the cavalry wedge problem. So we're given some riders, some horses, and we're trying to build a cavalry wedge with the greatest strength. So there's some rules about building our cavalry wedge. So each of the horses has to be faster than the horses behind it. Otherwise, then, they bunch up, they hit each other, it doesn't work. So the fastest horse has gotta be here. These ones have to be slower. And these ones, slower yet. So also we have the endurance of the riders, so the first rider has to have the most endurance then the second rows below have to be less endurance and less endurance as we go back and back in the formation. Otherwise the riders with more endurance can catch up with the other ones as they run out of endurance. And finally we have this horse rider compatibility problem. If we put some riders on some horses they're going to complain, it's not going to work. So we have to have a horse ridden by a rider which is compatible. And what are we trying to do? We're trying to maximize the strength of the formation, which is the strength of the riders that we actually use. So here's our Cavalry Wedge Problem. We're going to build this line of an odd number of horses. So if it's a wedge it has to be an odd number like this. So here's that wedge of size five you can imagine what a wedge of size seven is and each horse has to be faster than the neighbors that are ahead of it. So 3 has to be faster that 2 and 4, 2 has to be faster than 1, 4 has to be faster than 5. And each rider has to have more endurance than the neighbors that it's riding ahead of. So the rider of 3 has to have more endurance than the riders on 2 and 4. The rider on 2 has to have more endurance than the rider on 1 etc., etc. And each horse has a compatible rider, so we're basically deciding for each position a horse there and a rider. And the aim is to maximize the total strength of the riders. So, here is our Calvary Wedge model. The first part is just the data declarations and the decision variables. So we have two enumerated types here, because with two sets of objects we're reasoning about, we're reasoning about the horses, and we're reasoning about riders. Now what data do we have, for each horse, we have its speed, which is going to be important, and for each horse you also have the set of riders we were compatible with that. So that's really a piece of information that joins the two pieces of data together. For each rider we have the endurance of that rider and the strength of that rider. And then we have this size of the wedge and here we have an assertion that the size of the wedge has to be odd. And if not, its going to abort. Now there should be a constraint item here. Right, the constraint keyword should be there. This is a constraint and that assertion should be there, but we're going to frequently in the models from now on we're going to omit that constraint keyword just to save space on our slides. All right, and the positions that we're going to deal with are these positions in the wedge, one to five in our example of a wedge of length five. So we need to make two different decisions for every position, for every position we have to choose a HORSE to go there, let's call that h. And for every position we have to chose a RIDER to go in that position, let's call that rider r. So that's basically the data declarations and the decisions that we need for our cavalry wedge problem. So let's look at the constraints and the objective for our wedge program. So we're going to have that the horses are all different. So the horse we put in each position has to be different, and the riders are all different. So the rider we put in each position is different. Now, remember again, there should be a constraint keyword here, which we're leaving out just to make things fit in the slides more easily. Then we have our constraints saying the speed of the horse in the ith position has to less be than the speed of the horse in the ith plus one position. So basically in the first half of the wedge, basically the speeds have to be going upwards, and similarly the endurance of the rider in the ith position has to be less than the endurance of the rider in the ith plus 1 position. And then we have a similar forall looking at the second half array position, saying the speed of the horse in the ith position is greater than the speed of the horse of the ith plus 1 position. As we go down the other half of the wedge, now the speed should be decreasing, and similarly, the endurances of the rider should be decreasing. Now of course we need that in every position the rider at that position is a compatible rider for this horse. So that's just looking up here. That's a very interesting use of a variable lookup of a set now which we hadn't seen before. And finally, our objective is simple. We're just summing up the strength of all the riders that we chose for the different positions. And we're going to output the horses and the riders, which are those things which we're interested in. So here's our data, so we got a set of horses, a set of riders. For each horse we've got a speed. For each rider we got an endurance and a strength. And then we've got this compatible array. So for each horse, which riders can ride on that horse. And then the size of the wedge that we want to build and of course it's odd, so it's going to pass our assertion. So, when we run our model and the data, we're going to get the answer, unsatisfiable which is not very satisfactory. So, obviously something has gone wrong. We'd expect there should be some ways that we can build to make this all work. Now there's a whole bunch of warnings, let's have a look at what's going on. What went wrong with our model? So it's a little hard to see, it's often very hard to see what a loop is doing. So we're going to introduce a new feature of MiniZinc which is going to allow us to print out what's happening in a loop. So we can see what's going on. And that's Trace. So the built-in trace function does this. It takes a string expression and another expression, it prints out the result of the string expression and then just returns the expression. So basically it's just a wrapper around this expression before we evaluate this expression we'll print out this string. So we'll see what's happening during our model compilation. We can use this to see what's happening during the model unrolling and flattening. So your MiniZinc model that you've built has array declarations, things like this, it all has to be unrolled. Well those loops have to be unrolled, and they have to be flattened down into individual constraints which each solver can understand. And those are the two main steps in the compilation process. And we'll be able to see what's happening in the middle of that process. In this case, we're going to use trace in particular to look at what's happening in this loop unrolling that's going on. So we're going to change our model by adding these trace declarations in our two loops. So I'm going to trace here. I'm going to print out the speed constraint and the endurance constraint in the first loop just before I assert those same constraints. So notice here I'm using the syntax that I'm going to print out speed of h where I'm going to print out the actual value of i which is going to be given from this loop. So we're going to see what's going on in this loop and then in the second loop again, do the same thing. We're going to trace, we're going to print out the speed constraint we're about to assert and the endurance constraint we're about to assert before we assert them. So this has no difference in terms of what the solver sees. Nothing changed in what the solver sees. We're still sending it the same set of constraints but now we're printing out each time we go through the loop, what constraints we're about to assert so we can see for ourselves what's going on. Now, we run our model. Now with this trace thing we're going to see the speed and endurance constraints which were asserted, printed out. And we're going to get an unsatisfiable result. Now our attention should be moved to this last one here because here it's very clear that we've got an array out of bounds. So we're looking at the sixth horse. Right as soon as we do this, MiniZinc is going to say you're looking at something out of bounds, so this whole thing must be false. And so this, by itself, this constraint, if we assert it, will just be false, and so we'll have no solution. Right so there's an error in the second loop. And we see what's happening is we're actually going one to far in that loop. So we can change that loop by just saying, okay, from n div 2 to n minus 1 rather than to n. So we're just going too far with the second loop and that by itself will cause unsatisfiability. So now we fixed that model. We run it again. Unfortunately we still get unsatisfiable. You can see that by fixing that loop we got one less output statement. So we've made that change and you can see that there is a problem here, we've got some incompatible constraints here. So this says that the speed of horse 2 is less than the speed of horse 3 but this says the speed of horse 2 is greater than the speed of horse 3. And together those two have no solution. So we can see when we've printed out effectively the constraints that are going to the solver that something's going on here. And the problem is that this is wrong right? We don't want that the speed of horse 2 is greater than the speed of horse 3. And the problem is again in our second loop and our second loop starts too early, right. It should start from here with horse 3 be going to horse 4, that's the way it should be working. So we can again, fix our second loop by saying it's from n div 2 plus 1 to n minus 1, all right? So we changed our loop twice, using our trace each time to see what happened. Now when we run, the constraints look like they should for our wedge constraints, and we actually get a solution. So we found what was wrong with our model and we've finally been able to get a solution. Okay, now let's change the data file so it says n equals 7. We run the model. We look at these constraints. They look correct, right? 1 2 3 4 going up, 4 5 6 7 going down. But we get unsatisfiable. Is there still an error in our model? Well there might be, but actually in this case it's simply that there is no solution for this data, there's just no way of putting seven riders and seven horses to fit the constraints, and we've gotta be aware that that can be a valid answer. Sometimes when we're building complicated models the valid answer, that there's no solution with our data. And so we have to be aware that this is correct. This is not an error in the model or an error in the data. This is just the correct answer, there is no solution. And that is a valid part and that's one of the parts of debugging models. So we have to be aware that sometimes the correct answer is there is no answer. So, in some way we've introduced the trace expression for MiniZinc. And what this allows us to do is trace what's happening in a comprehension to see what's going on. You can put trace anywhere in MiniZinc that expects an expression. And whenever that expression is about to be flattened or unrolled or evaluated then MiniZinc will print out something so you can see what's going on. So trace is invaluable for understanding complicated models. But unfortunately, it won't help you find all the bugs in your models. Subtle semantic errors, the trace will show you, it's asserting all the constraints that you actually expected it to assert, but unfortunately, those constraints are the wrong ones. So we'll still need more ways of tackling bugs in our models.