So welcome to the reference section material on flattening. So what is flattening? So flattening is the process that MiniZinc does of taking your model and data and creating an input to the solver. 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. 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. You can see the result of flattening if you're using the IDE by using compile button. From the command line, you can either use mzn2fzn, which actually directly creates a FlatZinc or let's say mzn-gecode. So using gecode solver with -k to keep. And that'll keep the FlatZinc around so you can have a look at it afterwards. So what's flattening expressions? So basically, we've got to simplify the expressions. We certainly gotta evaluate all the fixed expressions and we've got to name subexpressions. And that's essentially how we would flatten. 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. 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. And then finally here is where the subexpression is new so the y * z we had here is replaced by this new integer variable. That's the idealized FlatZinc. What FlatZinc actually looks like is this. So we have a new feature here. We've got some annotations here. This annotation says this constraint, the times constraint. All right, so this is the same as INT01 is y, z, it defines the variable INT01 as the local variable. 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. So there's the actual FlatZinc result where we can see this annotations and this form of how we write down the equations and the multiplications. 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. But in fact, if we'd rewritten this as- y- x, we could have got an array 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. 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. 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. So objectives in FlatZinc are just converted to a single variable so when I have this complex objective. I'm going to evaluate that, so I'm basically going to build the array that this represents. And we build the sum and that that result will be a new variable INT10. Now, I'm going to maximize the variable. Now so lets look at the final version of knapsack after the constraints application. So we get outbounds but the limit constraint ends up being a single constraint. And this expression for evaluating the objective is again single linear equation and then we have solve maximise INT10. And so that's how it looks like in the final FlatZinc, so Arrays in FlatZinc are different arrays in MiniZinc. They're only one dimensional and they always start with index 1, so, when we're translating arrays from MiniZinc to FlatZinc, we have to modify these multi-dimensional arrays to be one dimensional. And that means we have to also shift in distance. 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. 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. So element constraints are in fact how arrays are implemented inside solvers. At least inside CP solver, they are mapped to linear constraints inside MIP solvers. So the element constraint provides this functionality so array is an element. It's an index and array in a result and they co-exist. The array of index value you can see is = result so our constraint x[INT02] = 2 becomes effectively this. array_int_element, there's the index value, there's the array, and there's the value of looking up that index value, all right. So how do we flatten if, then, else, endif? 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, the t expression there. And then we look up this array by taking the b value whether this is true or false and adding 1. So if the b evaluates to false then this would be 1 and we'll get the result of the b. If b is true this evaluates to 2 and we'll the result of t this constraint here, we found this, right? This is [y,x] would be equal to the expression 0 and then, with a bit of flattening, you'll get down to this and then you'll build this final FlatZinc. So how do we flatten Boolean expressions? So we've gotta recall that solvers only take a conjunction of constraints so when we've got something complex like this. Which is clearly not a conjunction of constraints the way we do it by naming constraints right. So reification of a constraints c creates a name, so b is our new c, it basically makes b a name for whether this constraint holds b is true c hold and b is false if c doesn't. 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 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. 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. 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. That has to be replaced by a reify so this reified constraint b, so b will give us whether this constraint holds or not and then we replace this by b implies it's equals 0. just keep the remains of this expression using array of information. And then of course the reified constraint will be unrolled array of and so will replace it by its definition, which will do this, and will be more flattened. 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. And then, we'll float out these variable declarations to top, and float the constraint, which is just a single Boolean, to nearest enclosing Boolean context. Let's look at an example of that but here we've got this not over a sum of 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. Notice that if we can push negations, to get reifications, we can get a much better result. So because, in this place, we, well actually, we've got to be very careful. this may not be the same. Looks like it's pursued with the model of what we wanted, which looks to be the same. Square roots actually may not exist. So the square root function is a partial function. 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. 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 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, with the b2 here that represents the constraints that are implicit in this local variable declaration, flow at the same context where x * y != 9. 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.