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.