0:14

And this is called flattening because basically the complex expressions,

Â etc of the model are flattened down into very simple things in the resulting

Â flattening that is sent to the solver.

Â So flattening involves a number of different steps of flattening expressions

Â so making large expressions into flat things.

Â Unrolling expressions, how we handle arrays, how we handle reification,

Â and that is complex Boolean expressions.

Â What do we do with predicates and functions and what happens with lets.

Â 0:46

So first of all let's look briefly at the MiniZinc Tool Chain.

Â So you start with a model and then some data.

Â And then there will also be the globals library for

Â the particular solver that you're using.

Â All of those things go in to the translator which will basically flatten

Â the resulting model into a flattening point.

Â It'll also reduce something for producing the output, but that's really separate.

Â That's for making pretty output.

Â Then the FlatZinc model would be sent to the solver and

Â the solver will return solutions.

Â And then finally there's a process where we take this definition of the output and

Â the solution and we produce that pretty output.

Â So flattening is this process of taking the model and the data and

Â the global definitions and creating a FlatZinc model.

Â And a FlatZinc model basically only has variable declarations and some parameters

Â and primitive constraints and a solve item and some output annotations, possibly.

Â 2:19

We also do a bounds analysis because we're going to name subexpressions and

Â introduce new variables to name them.

Â We want to introduce them with five bounds.

Â And the most important part of flattening is to know these common subexpressions and

Â not basically introduce two names for the same thing.

Â So let's have a look at the small model here.

Â We've got two parameters i and j.

Â We've got three integer variables x, y and

Â z with x just an unbounded integer, but y and z with strong bounds.

Â And then we write, x*y + y*z <= i*j.

Â So the resulting flat model is shown below.

Â So we can see that we've got the basic things, x, y, and z are in there.

Â These parameters i and j are just weird, because they're not interesting.

Â They've just been evaluated wherever we use them, so

Â we don't need them in the flat model.

Â 3:12

We've got expression evaluation, so you see i and j we used here.

Â Instead of just putting i x j, we just put the value 6.

Â We've also introduced a subexpression name INT01,

Â and it's got bounds from 0..6.

Â And then this is clear when we look at it, what it refers to.

Â INT01 isn't holding the y * z expression, and we know that y and

Â z take variations 0..2, 0..3.

Â So the bounds analysis worked out,

Â well this can only take away from 0..6.

Â 4:22

And this annotation here tells us that this is a local

Â variable which is defined some way later on in the model.

Â So now I'd like you to write down what you think results from this very

Â similar example.

Â We've got two parameters, i and j.

Â And it's 3, we've got three variables.

Â And then we've got this link expression along

Â with that expression.

Â So the first thing we noticed was, did you notice the common subexpression.

Â So if we look at what's going on here,

Â we've got the original variable declarations.

Â We're going to introduce INT01 for this expression x - 3.

Â This expression here is x - 3.

Â This expression here is also x -3.

Â We don't have to introduce two variables on the bridge,

Â we can introduce the same variables.

Â We can do some bounds in analysis obviously x is between 0 and 5 and

Â x -3 is between -3 and 2.

Â And then this expression here is INT01 * INT01, that's INT02.

Â And then finally the rest, this is all linear, this INT02,

Â this expression, plus y + z + 6 is >=0.

Â What we don't want to do is introduce two names for the same expression.

Â We don't have a name for this and a name for that which is different.

Â 6:04

So, comma subexpression elimination works this way,

Â when we're flattening, the flattener checks is the expression

Â has been seen before and if so, it uses the same name.

Â This is very important to get small models and efficient models.

Â Because you don't want the solver to have two names for the same variable.

Â But it's not perfect.

Â So if we look at this expression here (x- y) * (y- x) >= y- x; well,

Â we're going to get two subexpressions.

Â This is (x-y) and this is (y-x).

Â We'll reuse this (y-x) here so INT03 equals the multiplication of these two and

Â then this INT03 is greater than INT02.

Â 6:53

with one less expression.

Â So, there's what it looks like in the actual written down these linear constraints

Â in the int_lin form There's no time constraint and the less than or equalo to.

Â So, it's good to have tight bounds on variables.

Â They help the solver and the reduce the size of unrolling if we

Â have unrolling over some variable that we don't particularly know.

Â So when we introduce a particular variable,

Â some INT01 is equal to our expression,

Â the system will try to find the minimum possible way that expression will make.

Â And the maximum possible way that expression will take and

Â then declare that variable with this bounds l, u.

Â 7:40

It may not be able to in which case we'll just do bar INT or bar float.

Â So if we look at this example here, we've got x between -2 and 2 and

Â y between 0 and 4.

Â Then we're going to get INT01, which this is x * x, and

Â we can see it displays values from -4 to 4.

Â We can get INT02 and it's going to be y * y which is going to take values 0..16.

Â So you can see that you get these going.

Â But notice that we could actually do better than this because

Â we could think about this expression and this expression are <=6,

Â then one of them could be bigger than 6.

Â Which means that we couldn't have zero, 16 here for INT02.

Â And it also means since x * x is actually square,

Â it can't be less than zero.

Â So we can update that to zero and furthermore,

Â when we see if y times y is between 0 and 6.

Â In fact y can then take var 0..2 If y were take the value 3 then

Â this would evaluate to 9, it took the value 4 it would evaluate to 16.

Â So this is possible if we do what's called presolving where we're

Â going to presolve with the model before we actually finish the flattening,

Â and that is one of the features that we'll added to MiniZinc shortly.

Â 9:04

So linear expressions are basically one of the most important kinds of expressions.

Â And basically a linear expression is, we never multiply two variables together.

Â Now naively, we could look at this constraint and write it down

Â And they would get y minus x, that's that expression.

Â And we get 2 times that we get that expression and we get x plus INT02,

Â that's this expression.

Â Then we get INT03 plus z, which is that expression and

Â then we get 4 times z, this expression.

Â And then we say that this left hand side INT04 <= INT05, but in fact we don't do that.

Â What we do is collect together all the linera terms so we have +1 x here from- 2 x.

Â So that's over all -1 * x we have 2 * y here and bring it here.

Â We have +1 z here and -4z here, once we move to this side, so

Â we have -3 and here we get just one constraint rather than this large list,

Â and then we'll convert it to a FlatZinc.

Â So models are typically not fixed size.

Â Usually they're going to read the data and

Â a number of constraints that depend on the size you get, but here is a problem.

Â We've got our end object which has a size and value and

Â we're wondering how many of each to take.

Â We have to take the positive amount and basically if we solve

Â the sizes by however many objects we take, it has to be less than our size limits.

Â And we're trying to maximize the value becomes the number we take and so

Â here's a small example with four objects.

Â The sizes 5, 8, 9, 12, the value 3, 5, 7, 8 and

Â the limit on the map of size, total size, okay, 29. So what happens,

Â well, when we see this,

Â remember that this generator call is really the same as this comprehension.

Â It says build this array these things my i in OBJ, and

Â then apply the sum onto that array, and that's what's <= limit.

Â So you can see, we have to build these expressions 5*x[1], 8*x[2], 9*[3], 12*[4].

Â And then we build this array, which has all those expressions,

Â that's building up this expression then we can apply some

Â to this to get INT05 and then we can say it's full.

Â But in this case of course obviously we're dealing with one particular linear and

Â in fact that's what MiniZinc will do,these are the steps it will go through to get to that linear.

Â If you think about top level conjunctions, they are forall very commonly,

Â then we can split this in separate constraints.

Â Because if we think about what this is actually saying about fixed data,

Â we're going to build this array of X1 greater than 0, X2 greater than 0,

Â X3 greater than 0, X4 greater than 0.

Â Or booleans and then we're going to find a forall for that array of booleans but

Â the result of this is just to basically to enforce each of these constraints so

Â we get what we would expect.

Â 13:28

If I have an array with a lower and upper bound in the first dimension,

Â lower bound and upper bound in the second dimension.

Â And the way I'm going to convert this expression, x of i,j is I am going

Â to have a one dimensional array which has the right number of elements.

Â This is the difference between these plus one, the difference between

Â these plus one multiply together, that's the right size of the array.

Â And the way I convert x of ij into a look up in this one dimensional array

Â Is if I take the i and subtract from the lower bound.

Â I multiply that by the size of the second dimension,

Â and then I add j - 12 + 1.

Â 14:10

So if we look at an example of that,

Â here's our MiniZinc with a 2 dimensional array, which goes from 0 to 2.

Â Is the sum and here we go a complicated look up all right x[x[1,1],1] = 2.

Â So, first of all we flatten, so here's the array is for

Â this sum of the constraint become x[0,0], + x[1,1] + x[2,2] <= 1.

Â Now to introduce a local variable for this x of (1,1) expression and

Â then we look up x INT01(1)= 2 so

Â once we convert it to one dimensional what happens?

Â So this array obviously have nine elements in it within the bounds of.

Â And still haven't changed and

Â this constraint if x of 0 0 is the first element in this one, x of 1,

Â 1 is the fifth element in this array and x of 2, 2 is the last of the groups.

Â INT01 is x(1), 1 it's just saying it's x(5) and then.

Â Now I have to calculate what's the index value for the first two, so

Â it's going to be the same calculation.

Â We take INT01, we subtract the log ID which is 0,

Â so we get INT01 and we multiply by the size of the second

Â which is 3 and then we take the second lookup value 1.

Â We subtract the lower bound of each dimension which is zero and

Â then this gives us a variable we'll look up, so

Â we don't know the medium here that looks up to the right one.

Â 16:34

So, if b is fixed, so we know it Flattening time then we just evaluate it.

Â If it's true, we replace this expression with whatever you've put for

Â t and if it's false, you replace it with e.

Â If b is not fixed, we're going to build a little expression which evaluates

Â the same thing but here's an array, we put the e expression there.

Â This would be the name of the result column of the expression,

Â 18:03

And so, FlatZinc primitives often have reified versions, so,

Â here's the linear constraint primitive.

Â There's also a reified version whic adds to this extra Boolean on.

Â Exactly encouraging b if known linear constraint holds.

Â So, if we consider our expression here then the flattening is analogous to

Â other expressions x > 0 is going to be different to BOOL01.

Â So is y > 0 and z > 0 and then, so

Â is also this conjunction expression which is BOOL02 and BOOL03.

Â Then we're going to do an integer to hold our results coercing that into

Â a an integer from the Boolean.

Â And then we're going to boolean this

Â constraint is easier and finally we're going

Â to say that this implies the Boolean that represents this

Â 19:01

And that's what it looks like in the actual flattening.

Â So, we have to be careful to flattening boolean expressions,

Â we want to avoid negative contexts.

Â So In doing so we try to push negation down to the bottom level,

Â we gotta be careful.

Â This is only correct if there is no possibility to find results we can push

Â negation.

Â So x greater than zero implies bool2int this is the same as not x

Â greater than zero or and which is the same as x less than equal to zero.

Â Because [this can never be undefined or bool2int and

Â then you'll see we flatten this as before,

Â so predicates and functions act like macros.

Â Basically when we see any expression including them we expand it

Â with the arguments and then flatten.

Â Basically, if we see some function f(x1 .. xn) we place

Â the arguments in the right positions then we flatten the result in three,

Â so let's have a look at an example.

Â Here we've got a predicate far_or_equal which says either

Â the man_dist:{x1,y1,x2,y2} >= 4 \ / or they equal.

Â And, this is our Manhattan distance function we've seen before,

Â which distance between two points, u1 -u2, v1- v2.

Â And here's an easy to follow and the first place we're going to place this

Â the definition of Method, x1, y2, x2, y2 being replaced by a, b, c, d.

Â And then we've got a use of this function here, we're going to replace

Â it by its definition and then we can flatten the resultant, right?

Â Something like this.

Â 20:59

So we have to be careful that if we use a global constraint,

Â Which is native to a solver is only a definition,

Â so it's only a declaration, not a definition.

Â So before we get to this native of a solver,

Â we just say whenever you see alldifferent send it directly to the solver.

Â So, if we have a call to this level constraint, how do we translate it.

Â 21:23

Well, in the root context it's fine, we can leave it unchanged and

Â then we send it to the solver If it doesn't appear in the root context then

Â it appears in the negative or mixed context.

Â We're going to have to reify have to get a boolean which names whether or not.

Â So that we can apply the right equation

Â so if we have an example library where alldifferent is native, but

Â alldifferent_reif is given by this translation.

Â This says that b is true, if now we have for each pair of i,

Â j are different, then all different x, y, zed.

Â This stays unchanged but

Â this all different, which notice is a negative context.

Â 22:34

So let expressions are another important feature of

Â that allows us to introduce new variables and indeed new constraints,that can be unrolled.

Â But FlatZinc only has variable declarations and constraints.

Â All the variables that we choose in As we floated up to the top level and

Â the key thing we have to do is rename copies of new variables.

Â We have to be careful because of relational semantics,

Â we have to be careful about having partial functions and local constraints.

Â So basically, if we have some let expressions inside this expression,

Â by introducing an integral x on the constraint c in some

Â expression of 2 to the x we're first going to rename the variable to be u.

Â So that it doesn't clash with any other x's we'll build a new variable y

Â interface and replace it with the uses of x e by y,

Â we'll name the local constraint by introducing a new boolean.

Â so var bool: b=c and then constraint b,

Â so this type of constraint on the Boolean.

Â 23:53

adding up the integer square roots of a of i.

Â So, this function is meant to give you each of the square roots.

Â Its says, well the square root of x is number y, so

Â it's the y times the y equals x, and y zero.

Â So, if we unroll this sum expression,

Â we're going to get not 8 is greater than or equal to 12.

Â Well, the first figure of this is the square root of ai.

Â Is this one.

Â This is when i is one and here's the square root of when i is two.

Â Now obviously these two y's are not meant to be the same thing.

Â So the first thing we do is rename both two y's to be different, so

Â this is y one and this is y two.

Â So there's no confusion So we don't have to float them that way.

Â They'll eventually be the same.

Â Next thing we do is name the Booleans.

Â So we had this constraint, local constraint,

Â y1*y1=a(1), let's call that b1.

Â Oh and y1 >= 0, the whole constraint put together, and give it a

Â name and now you have a constraint b1 rather than the

Â whole thing.

Â Now we can float out these variable collections to the top, okay?

Â We've got to float out the constraints to the nearest enclosing boolean context

Â constraints greater than or equal to and so here's our result.

Â There was the equal to and the constraints which are the b1 and b 2 floated out to

Â the end and in and then all the other definitions just got floated out the end.

Â All right and that's our formula to multiply.

Â 26:03

But imagine if this is the model that we actually need.

Â Then we can float out the declarations as they were.

Â But now, this is 8 < y1 + y2 and b1 and b2, and we can flatten the result in MiniZinc,

Â and then we can make these booleans which are forcibly true, to be true.

Â You can flatten a bit further and

Â you can see we get a much tighter more simple model for the solver.

Â So the local variables defined by partial functions need fairly careful treatment.

Â 26:38

It's because if they are only partial,

Â then that the failure of the partial function has to be captured in the right format.

Â But here we're introducing an x, which is a division by y, 9 divided by y,

Â which obviously this x could evaluate to undefined, which means this expression could be false

Â So what the translation does is what we

Â are first going to do is make a version of this which cannot go wrong.

Â So we are going to introduce y1 which is the same as y except it

Â doesn't have the value 0.

Â Pass it by value so we are going to do the division by this y1 so

Â you just divide by the value x and of course y base value of

Â 27:27

zero then x doesn't meet values just x.

Â We are going to have constraint b2 which is representing what's going on in here.

Â Which says, well, this whole thing,

Â this context here, a local constraint if you think about it that way.

Â With the calls then y has to be to zero.

Â Otherwise this division by zero would happen.

Â And if it holds, we also want that y1 and y are the same value.

Â But if y is not equal to 0, then to force y1 and

Â y at the same radius means that x will have the y value.

Â And then we can write the whole constraint like this,

Â 28:17

But none of this can cause failure.

Â So in this work on flattening, we're trying to understand how MiniZinc works

Â and this can help you in debugging models.

Â When you see how they get flattened,

Â you might possibly understand that they're not doing what we expect it to.

Â It also can help you in understanding why different models that are preferable.

Â You can see why some models will produce big flat results and some small ones.

Â The flattening is this converting MiniZinc to a conjunction of primitive constraints,

Â which the solver can handle, and so it's a critical step you're actually getting a result.

Â That brings this segment.

Â