1:40

So, when we're digging tunnels, we can't dig under the huts, okay?

Â So the huts are actually impervious so

Â we can't just directly break through the bottom of the hut.

Â We have to dig to places which are open ground.

Â So the diggable spots are these ones particularly in the corridors

Â inside the thing, we can't dig directly to a heart.

Â Now, once the tunnel is built, then our soldiers are going to jump out of

Â the tunnel and they're going to run around and attack the bandits.

Â And basically, what we want to do is get all the bandits quickly.

Â So we want to be able to get to every hut within a distance of three.

Â So, that's a Manhattan distance.

Â The Manhattan distance counts basically the number of steps we take vertically and

Â horizontally.

Â So, here the Manhattan distance of three to here because we go one horizontal stop,

Â then two vertical steps.

Â So each of these are examples of Manhattan distance 3.

Â 2:44

So, if we open the tunnel here then we could reach all of these positions in red

Â within a Manhattan distance of 3.

Â And basically, that's how quickly we want to be there.

Â So we want to make sure that we're going to cover all of the huts within

Â a certain Manhattan distance, all right?

Â So we're going to make sure that huts are covered.

Â So for example, if we dug a tunnel to here,

Â we're going to cover these four huts in the corner.

Â If we dug a tunnel here, we're going to cover these four, right?

Â With these four tunnels,

Â we could actually cover all of the huts at Manhattan distance 3.

Â Unfortunately, Liu Bei and the other heroes only have three digging teams,

Â so this is not going to be a solution to our problem.

Â Now there's a cost of digging.

Â So basically, since the digging starts from over here,

Â the cost is how far away we are from that position.

Â So every different slot we can dig to has a different cost.

Â 3:39

And what we're trying to do is minimize the cost of the digging because

Â effectively that's going to be how much effort we have to pay for

Â from our diggers.

Â So let's look at that model.

Â So we have the size of the bandit's point, so

Â it's size times size, it's a square bandit camp.

Â Then the number of points that we're going to dig to is going to

Â be this number of points and the maximum distance that we can be, so

Â we can cover where we're going to escape from a tunnel.

Â What's the maximum distance that we're going to be able to get to

Â in Manhattan distance to surprise the bandits?

Â Okay, so for each position in this size by size bandit array, we've got a cost.

Â How much it costs to dig there?

Â And then the main decisions, of course, are for each point,

Â we have to decide which row does that point occur on.

Â And which column does that point occur on which variables from one to size.

Â Now, we need that all the tunnel exits are different.

Â So we could write that this way so basically we're taking the row

Â number minus 1 and multiplying by size and adding the column number.

Â And that will map our two decision variables into a single integer and

Â making sure they're all different will force that the positions that we exit

Â are all different.

Â But that's kind of difficult to understand, so can we do better?

Â Well, we're going to introduce a new construct from MiniZinc to help us

Â do that.

Â So the let-in construct is very powerful in fact.

Â So it allows us to introduce new variables and parameters "any point" in the model, so

Â any points inverted commas because it's not exactly true.

Â And we'll come back and look at some of the restrictions of any point later on.

Â So the format as we say, let and

Â then we have basically a declaration of the variable.

Â We could have an expression which we equate it to,

Â we're going to have to do that for parameters.

Â And we've got a list of all these normal variable definitions in MiniZinc.

Â And then we're going to finish that off with a close brace and in.

Â And then, we have the expression for

Â which these local variables are going to be available.

Â So the parameters, if we introduce a parameter in this we must have a defining

Â expression because otherwise there's no way to get that parameter value to that

Â parameter variable.

Â And basically, we've gotta remember that anything we define in

Â this let expression is only going to be visible in this expression here,

Â the one after the in, and not for the remainder of the model.

Â So let's see how to use let.

Â So here, we're going to build an explicit array for

Â each of the points of this particular integer, right?

Â Which is going to vary from one to psi squared which is the points.

Â So it's exactly the same expression we did before.

Â So we take the row number minus 1 times the size plus the column number.

Â So we're going to build up this array and

Â then we can just say, alldifferent of this set of values.

Â Okay, this makes the definition easier to understand,

Â because we're basically explicitly showing you what's going on.

Â It's not going to create actually anything different really,

Â in the underlying solver.

Â We're just going to make our model easier to understand, and easier to modify.

Â 7:33

Now, we need to make sure that all the building are covered.

Â So here's an example of where we can use a predicate, and

Â we're using some local variables to define that predicate.

Â So, do we cover a building on the position x, y?

Â This is what this predicate is meant to ensure.

Â So if we do cover a building on x, y,

Â there must be a point within a Manhattan distance of mDist from that building.

Â So we're introducing a local variable, i,

Â which is going to guess basically which exit point we're using.

Â And then we're going to calculate the distance from x, y to this exit point.

Â So the distance from x, y is just the position x minus the row of i,

Â the absolute value,.

Â Plus the absolute value of the y-th coordinate,

Â the column coordinate for the position we're looking at covering,

Â minus the column where we find the particular point we've picked.

Â So we're going to calculate that distance and then, say,

Â well that distance must be less than the maximum distance that we're

Â allowed in that model, in our example, which is 3.

Â So this is a predicate, which is going to test where this position x, y is covered.

Â And notice we're doing something quite clever here.

Â We're actually allowing it to pick which point is covering it.

Â So basically,

Â there's a pseudo decision here about which point is going to cover it.

Â Now, how do we apply the constraint?

Â So let's build basically the even numbers, right,

Â the huts occur on the even numbers, which is from i is 1 to size div 2 i times 2.

Â Let's build that array and then we'll say, forall i, j in huts.

Â So basically, picking all row columns in these even numbers,

Â we're going to check that it's covered.

Â All right, so we can see that by building this cover constraint,

Â we've made it clear what we're trying to do.

Â And then we're using this cover constraint on each of the hut positions,

Â improving readability and modularity.

Â Now finally, the objective we're trying to minimize the total cost of building, so

Â that's basically looking up the row and column.

Â Looking at the cost value for digging to that point and minimizing the total cost.

Â And if we can run their model, we'll find that we can actually cover the bandits

Â with only three points, if we pick these three points, and our cost is 18.

Â So, just to show you another use of let-in,

Â if we go back to the patrol problem we saw a number of lectures ago.

Â Then we needed that in every day,

Â the number of soldiers on evening shift was greater than equal some lower bound.

Â And every day the number of soldiers on the evening shift was less than equals to

Â some upper bound.

Â Well, another way we could do this rather than introducing direct common

Â subexpression based for this, we could just do it the same by using a local

Â variable to build up that expression that we're going to use twice.

Â So here, for each day, we're going to build a new local variable,

Â which is how many are on evening shift which is just this value, right?

Â The sum of the soldiers are on evening shift on that particular day.

Â And then we're going to add these constraints

Â that l is less or equal to u and on is less or equal to u.

Â Which is going to enforce these two constraints, so we're building a common

Â sub-expression but we're just using a local variable to do that.

Â It's often easier than building an array of intermediates,

Â which is what we did last time.

Â We were basically adding some global decisions into our model and

Â then use them in multiple places.

Â If we're only going to use them in one local place, we just add a local name for

Â this particular common subexpression and then reuse that local name.

Â So, let's look at another use of let-in.

Â Suppose our solver does not support division,

Â then we can actually define division using multiplication.

Â because really from a relation perspective,

Â they're really the same thing, like plus and minus are really the same relation.

Â 11:31

I only do it for non-negative numbers because it makes it simpler.

Â But if that's the case, then if I were to write that x div y = z,

Â it's really the same as saying this.

Â That there is a number, if I multiply z times y and

Â add in some extra remainder, then I would get x.

Â And I need that this remainder is between 0 and

Â less than y, so these are two equivalent statements.

Â We can define division in terms of multiplication by these constraints.

Â But we need a new variable for this remainder and so

Â this is a perfect example of where to use a let to introduce that new variable, so

Â here's a predicate defining division.

Â So here's the actual arguments we're interested in, x and y and z, and

Â we're going to introduce this local variable r,

Â which is going to take a value from 0 to the upper bound of (y)- 1.

Â So we can't use y here, because y is not a decision, so far.

Â We have to give it a fixed range, so

Â we're taking the largest possible value that y could take, -1.

Â And then, we just write down our constraints, so x = z * y + r,

Â and r is less than y.

Â Okay, of course the actual value of y will constrain r as well.

Â But any time we introduce a local variable,

Â we should try to introduce very tight bounds on its possible values.

Â That's going to make our model much more efficient.

Â So what happens, we should think how does this work with division by 0.

Â Well, if y is set to 0, then this constraint will fail, right?

Â Because r has to be 0 or bigger, so this will have no solution and

Â that's what we want.

Â Remember the relational semantics says, if we divide by 0,

Â the constraint should be false and so this division constraint will return false.

Â What happens with division by negative where you can see that if we

Â add in a negative number then this will also fail?

Â And so, it's not really correct because there are,

Â you can do division with negatives, this version of the predicate is only

Â meant to work when we're doing non-negative numbers.

Â 13:37

So, if we ever make an assumption in our model,

Â we should really check it using assert.

Â So we can do that by using a new form of an assertion that is specifically

Â useful because of things like predicates.

Â So our division predicate was only really meant to work if the lower bound of y was

Â greater than or equal to 0.

Â That is that y was definitely not going to be a negative number.

Â And so, this is our version of assert which says,

Â okay, if this test holds then we just give you the regular definition.

Â Otherwise, we're going to print out an error message and abort, right?

Â So this is good, it documents the assumption we made about this predicate.

Â It's only meant to work when y takes a positive value and

Â it prevents the misuse of this predicate.

Â 15:02

Now we gotta be careful because these bounds are not

Â guaranteed to be the declared bounds.

Â They're guaranteed to be correct bounds on the variable we were talking about.

Â So for example with this little snippet of code here, if we ask for

Â the lower bound of x, then MiniZinc could return 0.

Â Because well, x is the result of an absolute value call, so

Â it's definitely going to be a positive value.

Â It could return -4, that was the declared lower bound of x, so

Â that definitely is a lower bound to any possible value that x could take.

Â Or it could return 2,

Â because if we propagate this constraint just looking at the possible values

Â of y between -4 and -2, it means in fact that x has to take values between 2 and 4.

Â So all of these are correct lower bounds on x.

Â And you can't rely

Â on which one of these you get when you're using the lower bound code.

Â You can probably rely on the fact that we'll always get no worse than

Â the declared lower bound, if there is one, because it'll be impossible for

Â MiniZinc to lose that information.

Â And we'll see that this assertion that we've used here,

Â this new form of the assertion takes three arguments.

Â The previous version only took the first two arguments.

Â 16:45

So in summary, let-in expressions are actually a very powerful way of

Â introducing parameters and variables for use locally.

Â So we introduce a parameter basically if we want to build

Â some complicated expression and use it in multiple places.

Â That's very handy.

Â Similarly we use variables if we want to build some local decision or

Â common subexpression, we can use it locally or

Â we want to make a new local guess, basically a local decision.

Â As we saw in the covered constraint where we added a point variable which was going

Â to basically check which point it was covered the hut we were interested in.

Â Whenever we define local parameters, they must be defined by this expression,

Â because that's the only way they're going to get a fixed value.

Â But local decisions don't have to be covered.

Â And what let-in does is help us modulize expressions and improve the readability of

Â our model, and basically remove common subexpressions in another way.

Â