Alright. In this section, we're going to look at how MIP solvers actually solve MIP problems. Because remember a mixed integer programming solver really only handles constraints which are linear, and only has integer and floating point variables. So, we have to map a MiniZinc model into this MIP formula. So, we look at things like representing Boolean variables and Boolean operations, and reifying linear constraints or whether how we turn constraints on and off, and some MIP definitions of globals. Alright. So, a Boolean variable is fairly naturally modeled in MIP solver as a 0, 1 integer, right? So, that's just the same as if I applied a Boolean end result. And then we can map the common Boolean operations as linear constraints fairly straightforwardly. So, here we have b1 is b2 or b3. Obviously, if b2 is true, then b1 has to be true. So, that constraint will force that. Alright, b1 is greater than or equal to b2, similarly if b3 is true, and that will force b1 to be true. And finally, if both of these are false, then this has to be false. So, that's a mapping of this disjunction into three linear constraints which will have exactly the same set of solutions. And similarly, we can map conjunction into three linear constraints, and we can map negation just as 1 minus b2. Alright. So, fairly straightforward to map Boolean operations into linear constraints. Alright, more importantly is we're going to have to reify integer linear constraints in this MIP solver. So, in order to transform complex constraints where we keep track of whether constraints hold or not, we basically need be able to model this, b if and only if sum linear expression. Alright. So, we've already made the part of the complex constraint linear, and we got down to this reified form. So, how are we going to do that just using straight linear constraints? So, the simplest way, think about it, is this we're gonna work out what's the smallest value this expression could take? Alright? We just take the lower band of each of this a of i, x of i terms, which will depend on the sign of a of i and the values that those integer x of i can take, let's call that l. Then, we work out the upper bound on what this term could ever be, let's call that u. We're going to need to add two constraints to force this behaviour. The b, if b is 1, this constraint should hold, and if b is 0, the opposite of this constraint should hold. So, if you think about it when B is 1, we need to force this inequality to hold. So, if you look at this expression here, so we're summing ai, xi. Now, if b is 1, obviously we get c here and this term disappears. And so obviously, the constraint holds. But we have to be careful. What happens if b is 0? If b is 0, this constraint should be nothing, no constraint whatsoever. And if you think about it what happens when b is 0? Then this disappears and we get u, and we know that this expression is always less than or equal to u. So, this constraint basically turns itself off. Then, when B is 0, we have to force the reverse to hold. So, if you look at our constraint here, when B is 0, this becomes true and we get its greater than or equal to c plus 1. And this b times 1 disappears. If b is 1, we have to basically turn this constraint off and if you think about what happens when b is 1, this disappears and we just get l and of course, this sum is always greater than or equal to l, so that's no constraint. So, basically, these two linear constraints encode this reification of an integer-linear inequality. Alright, so, let's look at an example of using this encoding of reified linear constraints for this example, of nonoverlap. So, we have to start variables s1, s2 which take variables between l1, u1 and l2, u2. And we basically want that they don't overlap in times. So, if we take the end time of Task one, it's before the start time of task two, or the end time of task two is before the start time of s1. So, this will be flattened by MiniZinc regardless of the solver to something like this, we'll say b1 or b2, where b1 is the name basically, keeping track of whether this constraint holds or not. We're going to force at least one of these constraints holds. And of course, here is where we're going to have a reified linear constraint, we're going to convert into linear constraints. So, we'll have these 0,1 in variables b1 and b2. Keeping track of this and of course the or constraint, just converts into this, we just need one of them, at least one of them has to be 1. So, b1 plus b2 greater than or equal to 1. And then we're going to translate each of these reify constraints, we're actually only gonna give half of the translation. Because if you think about what we need here, we need to make sure that one of the constraints holds. So, what we need is the part of the translation which, if the constraint doesn't hold, will set these b's to false. That's the first half of the translation. So, here's the first half of the translation for each of those two constraints. So, this is just forcing that if this b is true, then the constraint will hold. And conversely, if the constraint doesn't hold, then the b will be 0. Alright. And so with that, actually we've got enough to translate that entire disjunction. Now, we could do the full translation or we could add the other two linear constraints on the end. We could even add some more things about the disjunction although it's always true. So, that's all we need. But that's just going to make the model less efficient. Alright, modeling multiplication in MIP is difficult, there's no multiplication operator. So, what can we do? Well, we can model multiplication of a Boolean by an integer. That's not too difficult. So, here we've got a Boolean variable of 0, 1 variable b and two integer variables, right. So, none of these are fixed, y and x. So, we can think about those as modeling these constraints. If the constraint b, if the Boolean is true, if it's 1, then Y has to be equal to x. And if it's false, if it's 0, then y has to be equal to 0. So, we can actually basically build a reified version of these constraints as we've seen before. Add those in and that'll give us the same behaviour as y equals b times x. In general, if you have to multiply an integer variable by an integer variable, then we're going to have to do a lot more work. We'll look at that a little later on. So, what about fixed array lookup. So, here I have an array from 1 to m, all fixed integers. And I've got this array lookup here where I'm looking up with a variable y, so x is a variable which takes a value which is the yth value in this array. Basically, we're going to need a 0, 1 variable to represent each possible value of the index y. So, you can think of this array 1 to m of the values that y can take. So, it's 0, 1. So, basically, by is representing that y takes the value, particular j value, by of j is y takes the value of j. Of course, y can only take one value, so if we sum those up, there is exactly one of them which takes the value of 1, and then we can work out the value of y. Right? Relate the value of y to these by's by saying, well, if one of these by of j's will be true, then y will take the value of j. So, if we sum up across those, that will give us the value of y. And now, we can work out the value of x straightforwardly. We just sum over all of the j's from 1 to m. We get the coefficient of this fixed array a of j and multiply by these Boolean. of course, since only one of these Booleans will be true, we'll just pick out the right value a of j from this array, so we can model this fixed array lookup by this system of linear constraints. What about if it's a variable array? Right. So now, our a is a set of variables. Then again we're going to do the same thing for y, we're just gonna have a 0, 1 variable to represent each possible value of y. And then, we're going to have the same thing down here, but now, notice whereas this before was a fixed value. So, this was a linear expression to begin with. Now, this is a Boolean times an integer and so we're going to have to do our Boolean times integer translation that we talked about a few slides back. We're going to have to do that for each of these sub expressions that we generate. But that can be done. Alright. So what about multiplication? How do we linearise z equals x times y when x and y are both integers? Well, the simplest way to do this is, we're going to basically build a variable array and we're gonna to put i times x in that array. So, for each of the i values which y can take. Now, we can see that this is now just z equals a of y is the same as z equals x times y because basically, we've taken the value of y and that tells us the index i where we put this i times x value. So, we're looking up i times x using this array. So now, we can encode z using this expression here and again, this is a Boolean variable times another variable. So, I'm gonna have to use our Boolean times integer encoding trick again, but we solve that. Of course the problem with this is if y can take lots and lots of variables this array is very, very big. So, this is not gonna be great. But then again, there's not much we can do. Linear constraints solvers really don't want to handle multiplication. Alright, what about global constraints in mixed integer programming solvers? So, MiniZinc translates them to a linear decomposition and this is usually quite different than the way they'd be translated for a CP solver. So, if we have our all different constraint then we know that that's in a CP solver it's default decomposition is to a whole lot of not equal constraints. But, in a linear solver what we're going to do is basically take this variable, we're gonna have 0, 1 values for each possible value. Right. So, basically b of ij represents the fact that x of i equals j. And now, once we've got that we can basically say okay, at most one exactly one of these b of ij value is true. That's just saying that x only takes one value. We can again relate x of i, to these b of ij values, it's just that, we did earlier for relating Y to it's Boolean decomposition. But once we have the b of i's, now we can constrain the all different constraint. Which is just saying, for every possible value that we can take. One to m, if we sum up across all of the b of ij's, it has to be less than 1. Which is saying that, only one of these x variables can take that value j. And that encodes all different and you can see that's very different than the CP decomposition. Where it uses a lot of not equals. Alright, when should we use MIP versus CP? So, one of the good things about MiniZinc is that you often don't have to make that choice. Make a model and then try a MIP solver or try CP solver. But it's good to know where things are good. So, MIP excels when most of the constraints are linear to begin with or in particular, when the objective is a large sum of components, particularly if those components have linear constraints that relate them. So, that's where MIP is strongest. CP excels when the constraints of combinatorial. So, when they're strange and interlinked using disjunction or other kind of things not equal. Things which are not naturally linear. And it's not very good when the objective is a large sum of linear related components which is unfortunate because that's very commonly the case. But for example, in things like scheduling where we've got to minimise make span, then the objective is just a single time variable and that's one of the cases where CP is very, very good. But of course, as I said at the beginning, you should just use MiniZinc on both. Try both solvers on the same model and then you'll see which one's better. So, just to recap, when we're mapping MiniZinc to MIP. We basically have to map reified linear constraints, on-off constraints and we've seen how to do that. We can map those down to each reified linear maps to two linear constraints. Of course, the effectiveness depends on how tight the bounds on the integers are because we have to workout this lower and upper bound for each expression. The tighter they are, the better we're going to get that mapping, the more and more easily the constraint solver is going to be able to handle that. And we end up often having two views on this bounded integer, so we got this integer variable x which we're going to use in some places and then we got an array of Boolean variables bx meaning b of x equals j, so bx of j is meant to mean that bx takes the value j.
