One of the scholars Liu Bei recruited during the feast was named Xu Su. Cao Cao had conquered provinces in the north and decided to start claiming those in the south. He ordered his subordinate, Cao Ren, to lead an army to attack Liu Bei's city, Xinye. The brothers and Xu Su observed the formation of Cao Ren's approaching army, and Xu Su recognized that they were adopting the azure dragon formation, which was inspired by the shape of one of four mythological creatures. To defend against this formation, Xu Su recommended that the brothers' army use the other three mythological creature formations, which were the vermilion bird, the white tiger, and the black turtle. To create these formations, battalions of soldiers with special skills, such as archers, shield carriers, and swordsmen were needed. Lu Bei had 24 battalions of soldiers, and some of them had one or more special skills. He planned to form four brigades consisting of six battalions each. To create the vermillion bird formation, one battalion of archers, two battalions of swordsmen and one battalion of shieldsman were needed. For the white tiger formation they needed three battalions of swordsmen. To form the black turtle formation, two battalions of archers and two battalions of shieldsman were required. [MUSIC] Xu Su insisted that at least two of the three special formations were necessary for defeating the azure dragon formation, but more formations would be even better. Liu Bei pulled out the tablet to help allocate the battalions to these formations. [SOUND] >> So Xu Su is one of the scholars that has joined Lu Bei after the scholar feast, and he's an expert on military formations. And he sees the army of Cao Cao using this Azure Dragon Army Formation, which is very powerful. So he tells Liu Bei about the Four Mythological Creatures that make up powerful army brigades, and how they can be built. So the three other possible army formations are the Vermilion Bird Formation, the Black Turtle Formation, and the White Tiger Formation. And these rely on the soldiers being able to take on specialized roles, either as archers, or shield bearers, or swordsmen. And now, if Liu Bei looks across the 24 battalions that he has available, then some of these battalions can take on these specialist roles, and some of them are very talented and can take on multiple of these specialist roles if needed. And so, he's going to build brigades out of these battalions, and so, six battalions in each brigade, and he's going to try to build these elite kinds of brigades, that's going to help him defeat Cao Cao. So, the vermilion bird formation for brigade requires two specialist sword battalions, a specialist shield battalion, and a specialist archer battalion. The remaining two battalions can be anything, they don't have to have any speciality. But they could. It doesn't matter if they do. The White Tiger Formation requires three specialist sword battalions, and the other battalions can be anything. And the black turtle brigade needs two specialist shield battalions and two archer battalions, and the other two can be anything. And Xu Su says that in order to comfortably or reliably defeat Cao Cao, he needs to have at least two elite brigades. So let's look at the model. So we have this enumerative type of all the possible battalions and we're also given for each set of battalions which can take on an archer specialist role or swords specialist role or a shield specialist role. And the size of the brigade which for example, a brigade is six battalions. Now, how many brigades can Lui Bei produce, well, if we take the number of battalions he has and divide it by the size, and that's the number of brigades he can build. So, what we're going to do, the principle decisions are, for each brigade, what are the set of battalions that make up that brigade? Now we need those to be all_disjoint, right? We can't use a battalion in two brigades. They're going to be put on the battlefield at the same time, so we can use this global constraint all_disjoint to do that for us. Now, we also want that the cognality of each of these brigades is equal to the size of a brigade, so that's fairly straightforward. Now let's think about the more difficult part of this, which is that we want to build elite brigades. And to do that we're going to introduce this predicate elite, which is going to check whether a brigade is actually elite. So if we take a brigade, which is of course a set of battalions, then we're going to look for this pattern in the brigade. So either the brigade has an archer, an archer, a shield, and a shield, which of course makes it a black turtle brigade, or the brigade has a sword, sword and another sword which makes it a white tiger brigade, or it has an archer, two swords and shield, which makes it a vermilion bird brigade. So this is using another predicate pattern, because we're doing a very similar thing here, we're looking for a pattern of types of brigade in terms of battalion inside that brigade. So here's our definition of the pattern predicate. So we're given against this brigade that we're checking and this array of sets of battalions. So this is the types of the various things. ARCHER, ARCHER, SHIELD, SHIELD are actually sets of battalions, remember. Now, here we're going to look up the size of this array. The length of that array is T, and we're going to use that to build the index set of this set of local decisions here. So here's where introducing new variables inside this predicate with a let, and we're saying, okay this is the battalions that are going to match these requirements. So what we need to do for each of these requirements in this index set that we're iterating over, we need to pick our battalion which is in the type, so in this archer or sword, sword, or shield. And that battalion also has to be in the brigade that we're selecting. So basically this is forcing that we've got the right number of specialist brigades of the right types and they're also all in the brigade. And of course we need them to be all different. So we can't actually use the same specialist battalion to meet all of these constraints. All right, so now we're solving the satisfaction problem first. We need at least two brigades to be elite, we'll add this constraint saying that the first and the second brigade are elite, and do solve satisfy, and what happens is we get an error message from MiniZinc. So it says flattening error: 'all_different_int' is used in a reified context but no reified version is available. So this is very mysterious. So in order to explain this, we're going to have to talk about contexts. So root contexts are the first kind of contexts we're going to talk about. So constraints solver only solves a conjunction of constraints. That's the key thing. It only takes conjunction of constraints. And that means then if you write a model with disjunction, implication, or bool2int, all of these things are going to be translated to conjunction. And the ones where the constraints which don't appear in a root context will have to have something happen to them. So what is a root context? So a root context is if the constraint appears straight after constraint. So this constraint must hold, right, in any solution, so constraint in a root context must hold. If we have this conjunction in a root context then each of the conjuncts like you see are also in a root context. And similarly, if we have this whole expression is in a root context, then all of the constraints here which occur inside the forall are also in a root context. So alternatively, you can think about this way. If I look at this constraint that I'm thinking about somewhere in my model and if the only connectives I see between c going up until I hit the constraint definition, the constraint keyword, are conjunction and forall, then c is in a root context. If that's not the case, then c is not in a root context. So why is this important? So if you look at this, let's look at our example, then this whole thing, this constraint is in a root context. And since that's a conjunction, that means this is in a root context and this is in a root context. Now, the first constraint, this one here, has to hold, and it's going to be flattened down to something like this. This is the body of the definition of elite. And you can see that we're getting pattern or pattern or pattern. Now, we've got a disjunction. This whole thing is in a root context, but each of these guys, these disjuncts, is not in a root context because the connective is disjunction. So the pattern calls are not in a root context. If we now look inside one of this pattern calls. So, this pattern call is going to be flattened by it's definition to be something like this, which introduced this set of decision variables and all of this constraints. And we see this alldifferent (s). And that means that alldifferent is also not in a root context because it's a part of this pattern which is not in a root context. So if I look at alldifferent, yes, we conjunctions up until we hit here, but then we see a disjunction on the way back to this constraint, which is where it actually appears. So our alldifferent call is not in a root context, and that's what's causing the problem. But to understand that we're going to have to talk a bit about reification. So as I said before, solvers take a conjunction of constraints. And so something has to be done to negation and disjunction. And the way we do that is by reification. So we're going to take the constraint and attach a boolean variable to it which is going to be true if the constraint holds and false if the constraint doesn't hold. And one of the key things about once you're not in a root context is in solution to the problem the disconstraint may not hold. So if we think about this simple case here in this disjunction, it's not the case in all solutions to this problem x is greater than y. Because that might be false, but this part of the constraint may be true. And that would make the whole constraint true. So the way we map this down is we map it to this. So we're going to say b[1] is true whether this constraint holds or not. b[2] holds whether this constraint holds or not. And then we're going to constrain this. So this is now not only about boolean variables and says, so this whole constraint must be true. Either b[1] must be true or b[2] must be false, all right? So this is a constraint that the solver can handle. It's just a raw disjunction with a negation at the end. And these are making sure that we don't force that x is greater than y, that p(x,y) holds. Because we don't know necessarily in any solution that they hold. Now this becomes more complicated for global constraints. So global constraints in non-root context are usually not supported. And that's what we're saying here. So we have something like some big constraint or, and there's an alldifferent (s), and not in a root context. Because what MiniZinc will try to do is look for a new predicate, which is the reified version because that's how it's going to treat this. So it's going to look for a constraint, all different reified, which is basically equivalent to this b is true if and only if the alldifferent constraint holds. If that was available, then we can map this to this thing where we've got a reified version here. We replace this boolean in here, and now this is just a simple disjunction of booleans, which is a constraint the solvers can handle. But unfortunately, most solvers don't implement these reified versions, like all different reified, of global constraints. And there's a reason for that. They can be very, very difficult to implement, or even more or less impossible. But there is one workaround this, the default definitions of the globals worked by decomposition. So they map down to really base predicates. And all of the base predicates can be reified. So if we use a definition which just maps a global down to smaller basic constraints then we can use reification. But of course that's going to be slow since when we implement by decomposition we tend to get a big constraint and a weak constraint. And sort of take home messages, you should avoid using globals in non-root contexts. Now, we can't really do that in our case. We really want that alldifferent constraint. It's not in a root context. How do we do this? Well, we're going to effectively put in the library definition of alldifferent into our model. So rather than including the alldifferent library function, which is going to be the direct one implemented by the solver, we're going to write our own alldifferent. Here is it. It's very simple. We just look forall (i, j in index_set(b). So again, we're just using index_set to find out what is this array. Index is varying over. So if all pairs are i less than j, we make sure that b of i is not equal to b of j. So just make sure that the two battalions are different. Now this will be unrolled to only not equals constraints, conjunctions of not equals constraints and then that whole thing can be reified. So this will be reifiable but, of course, it won't be using a global. It'll be using this much simpler definition of alldifferent. So once we do that our model will now run and we'll get an answer. But of course what we are trying to do is maximize the number of elite brigades so we can move this requirement that the first two brigades were elite and add a solve satisfy. I'm sorry, remove this solve satisfy and replace it by this maximization which is what we're trying to do. So we're trying to sum up how many elite brigades we have and maximize that amount. Now if we run, what happens? Now we get a different error message, long-winded error message. But basically, look down at the bottom. It says in the let expression in variable declaration for 'b' a free variable in a non-positive context. Okay, what on Earth is going on here? So in order to explain this we're going to need to know more about contexts. So we introduced new other kinds of contexts, positive, negative and mixed contexts. So a constraint c is in a positive context if there's an even number of negations on the path from the constraint where it appears in the model down to the actual copy of the constraint, right, the constraint declaration, the key word, down to the copy of the constraint in the expression that it's built up into. That means, of course, that root contexts are always positive. Because if you look through that, we'll only see foralls and ands which don't change. We don't go through any numbers of negations so root contexts are always positive. Constraint under an odd number of negations is in a negative context. So usually, we don't have many negations. So it will usually only be one. And some operators create mixed contexts which we use as plus minus symbol to do. And if you think about bool2int (c), c is in a mixed context. If you think about c1 if and only c2, both of these expressions are in a mixed context. The easiest way to think about this is, this c1 if and only if c2, is equivalent to writing c1 and c2, or, not c1 and not c2. And so you can see that c1 then occurs both under an even number of negations, 0, and under an odd number of negations, 1. And basically since we'll end up having this behavior it's like we're adding both odd and even. Doesn't matter how many negations we add above, it'll still have both odd and even amounts. So mixed contexts are effectively signage and they're both and odd and an even number deviations. And so, how do you work out the context of something then it's basically counting the number of negations from this constraint keyword. So we start at the constraint keyword and we start in the positive context and then if this thing is in a positive context then the argument of negation is in a negative context obviously. And if it's this not expression is in a negative context then its argument is in a positive context. And if the whole not expression is in a mixed context then the argument is in a mixed context. So we're going to read these as rules about how we propagate context downwards. If we have this disjunction expression in some context then the arguments are in the same context, whatever it is. And, similarly if we have a conjunction expression in some context, then both arguments are in the same context. Now this is true for positive and negative and mixed context, not true for root obviously. If you're in a root context here, these two are not in a root context. We can treat A -> B as just the same as not A\/B, that's what it means, and we know that these if and only if symbol twins, basically their arguments are always in the mixed context, because they're really doing something like introducing something like two effective copies. One which has an even number of negations and one which has an odd number of negations. So that's how you work out the context. The positive negative or mixed context of some part of the model. So, there is a rule. A let-in construct cannot introduce uninitialized variables, except in a positive context. So, let's look at a smaller example. Here we have a predicate even. It takes a variable and it introduces this variable y and says a variable x is even if there is a number y where x is equal to 2*y. So it's a legitimate definition of even, but here the context of this not even(u) is positive but the context of this even(u) is negative which means the context of this let is negative. And when we try to run this model we get this error saying that the let expression in the variable declaration for y is free variable in a non-positive context. So here we're introducing value y, and we're not initializing it, that's the other key thing. If we were to give it a value, say equal to x div two, then this would be okay. Actually that would also be a correct definition of even. So if we think about it a bit further, what are we trying to do with this model? We've said not even(u), which is the same as saying this not (let (var int: y) in u = 2 times y) Which we can just replace by this existential quantifier, not there exists a y where u = 2*y. And then if we push this negation in, we're saying well for all y, it's not the case that u = 2*y or indeed, for y, u does not = 2 * y. And you can see what we're doing here is universally quantifying over y. And constraints always do not support universal quantification. So all of the variables in a constraint solver are existentially quantified, so this just isn't supported. All right, so let's go back to our example. So the call to pattern appears in a mixed context. So if we think about that, where did this mixed context come from? Well, this is the declaration for this local variable which is not initialized that's inside pattern. And why is it in mixed context? because when we wrote this objective function, sum(i in BRIGADE) (elite (S[ i ] } ), we basically had this bool2int here. Right? So that means the call to elite inside this objective function is in a mixed context. And so this local variable here, which is called inside pattern, which is inside elite, is also in a mixed context. And so it's disallowed. All right so we didn't really talk about what happens for the context for the objective function it's the same as the constraint counting from here. So how can we solve this problem? Well the easiest way in this case is we can do our optimization by hand. We've already found a value with two elite brigades, so let's just add a constraint saying three elite brigades. Now all of these things now are in a positive context. And so that creation of the local variable is in a positive context and everything is fine. And so since this case returns unsatisfied, well we know that there's no solution with three elite brigades. We know actually the optimal value is two. So here we're really doing the optimization by hand to avoid that context problem. Now we can get around it, we can build a version of pattern where we replace this local variable by exists. But it's very very nasty, it's complicated to do and it works in certain circumstances and it builds huge models which are very very very slow to solve. So in this case, it's not a good solution. So if you're using existential qualification, you're using local variables inside constraints, they really can't afford to be in a non-positive context. So here in this section we've talked about context, root context, positive, negative and mixed context. And context is determined by the path basically from the constraint expression, the root of a whole expression down to the sub-expression of interest. So that sub-expression, what context is it in? And so we can do this calculation by looking at that path and seeing what connectives we go through. So, globals can usually only appear in root contexts, because we don't usually have reified versions of them available. If we need to, then we can use a decomposition which can be reified. And local decisions without a definition, alright, uninitialized local variables, there's things we're really not just giving a name to something, so often we build, an intermediate variable, which is actually defined by the rest of the thing. Here, this is a case where we're making a local decision where we actually have to choose what it's going to be, they can only occur in positive contexts.
