0:04

So Boolean Expression are critical for modeling.

Â Because of course, what we're mainly doing in modeling is building up

Â constraints which are themselves, Boolean Expressions.

Â So there's lots of ways of building Boolean Expressions.

Â The simplest way of course is to write in one of the built in constraints like greater than or less than or

Â the global constraints.

Â They can also build Boolean Expressions of more complicated form using Boolean connectives.

Â So we can use conjunction,

Â to join two Boolean together, ensuring that both have to hold for

Â this thing to be true.

Â Dis-junction, which requires that one of them has to be in control for

Â this to be true.

Â Implication, which is going to hold as long as either b1 is false or

Â b2 is true and, biimplication, requiring that they have the same truth value, and

Â of course negation, and Boolean expressions can appear frequently in parts

Â of MiniZinc models as constraints as already said as the where conditions.

Â When we have loops with where conditions, as the conditions in if-then-else-endif

Â statement, or the values of Boolean variables or parameters.

Â 1:05

So let's have a look at some Boolean expression examples.

Â So we've got some intermediate to beginning expressions, so

Â we can talk about more complicated Boolean expressions later on.

Â So here we've got a fixed parameter Boolean b,

Â which is going to take the truth value of whether x is greater than 0.

Â Here we've got the where condition of a sum,

Â which is only going to sum up the cases where a[i] is not equal to 0.

Â Here we've got the if then else condition of the assignment to this probability,

Â which is going to get either x or

Â z depending on the way of this Boolean Expression.

Â Here we've got a more complicated Boolean expression.

Â A conjunction implies this z greater than 0, and

Â here we've got a variable Boolean Expression d, which is taking the negation

Â of this fixed Boolean Expression or the fact that letter u is 3.

Â Obviously this is var bool because, we don't know what the real value of u is

Â going to be at the present time and the solver, is going to have to decide that for us.

Â So, what's the value of each variable?

Â So, it's fairly easy to see that x is greater than 0.

Â So, b is going to be true.

Â When we look at the sum, when a[i] is not equals to 0.

Â That is the case when i is 2 and when i is 3.

Â So we going to add up the second and third value of y which is 5 and

Â 2 to get 7. Now, if we look at this boolean of expression,

Â we can see the b is true and z is less than 7 is false.

Â So overall, that is false, which means we're going to get the result of z,

Â the else branch is going to be what we assigned to t, in other words,

Â t is 7. Let's look at this expression here,

Â so x greater than 0, that's true, t greater than 0, that's also true,

Â z less than 0, that's false.

Â So this true and true becomes true.

Â True implies false overall is false.

Â That's the only place where the implication doesn't hold.

Â That left-hand side is true, and the right-hand side is false, so

Â overall, c is false.

Â 3:11

Now we can evaluate the value of this expression d, well,

Â not c so we just put c is false, not false is true.

Â And now, and then we have short circuiting where we know true or anything is true.

Â So in fact, we can know the d value is true regardless of the value of u.

Â 3:31

So we can remember Boolean Expressions,

Â allow us to define very complex constraints.

Â So, for example, if you wanted to say that two points, x1, y1, x2,

Â y2 are either coincident, the same point, or

Â have a Manhattan distance of at least d we could write it this way,

Â to say is to say they're coincident is to say that x1 = x2 with y1 = y2.

Â That's one case. Or, we have to have a Manhattan distance of at least d which

Â means they have to be d way one of the coefficients so

Â either x1 is greater than x2 + d or x2 is greater than x1 + d,

Â well similarly, y1 >= y2 + d \/ y2 >= y1 + d.

Â So this expression and defines this condition, coincident or

Â have a Manhattan distance of at least d, and so

Â these Boolean connectors give us a lot of freedom in defining constraints.

Â But we have to remember when we're using such connectives, that

Â the underlying constraint solvers take basically a set of variables to decide,

Â and only a conjunction of constraints on those variables.

Â So when we use complex Boolean expressions, they need to be mapped down

Â to conjunctions for the constraints to be able solve them. And the process

Â of mapping these complex expressions to conjunctions is called flattening, and

Â the key trick it uses is what is called reification.

Â Which is basically giving names to all of the Boolean sub expressions,

Â which occur in these complex Boolean expressions. So, in order to map

Â the connectives to conjunctions, we need to reify constraints.

Â Basically attaching a Boolean variable to hold the truth value of that constraint.

Â So, if we look at this expression here x > 0 or y > 0.

Â We can't enforce that x is greater than 0 it might not hold.

Â We cannot enforce that y is greater than 0 that might not hold.

Â So instead we're going to give them a name.

Â So b1 is the name of whether this constraint holds or not.

Â It takes a truth value of this constraint.

Â This is what this is, b1 is true if z is greater than 0, and

Â b1 is false if x is not greater than zero,

Â and simply b2 is going to be the name of this constraint and

Â 5:37

effectively the trutyh value of this constraint. And then we can just write a simple or on these Boolean variables.

Â so here is this is a constraint that only takes two Boolean variables, and so

Â it didn't matter what we had, how complicated the expression was

Â here because we've given it a Boolean name to hold the value, whether that's true or false and

Â we can write a simple dis-junction only on Boolean variables, and nothing else.

Â 5:59

So, top level conjunctions don't cause problems for flattening.

Â So if we consider the very similar constraint here, x > 0 and y > 0,

Â we can flatten it to this.

Â We can just separate out our conjunction and say,

Â well that's a constraint x > 0, and this constraint also has to hold.

Â They're both forced to hold in any solution, and that's not going to add

Â any complexity for our solver, because our solver can handle a top level conjunction.

Â But we should note that when you use a conjunction inside where it's

Â not at the top level, so here this is b implies this conjunction.

Â And we're going to have to reify these constraints in order to have names.

Â To be able to build up the value of this conjunction expression here.

Â Because it's not the case in every model x, is going to 0 and y is 0.

Â We don't require any of those.

Â So remember we're making efficient models,

Â are more likely to be efficient if we don't use the disjunction and negation,

Â since those are going to be flattened using reification.

Â Now, sometimes we have to use disjunction or

Â negation to express what we want to express.

Â But what we should try to do is minimize the amount that we use.

Â Also, we have to be very careful that most global constraints can't

Â be used except at the top level conjunction.

Â So I write an expression like this, which is b or alldifferent based on x3,

Â so this alldifferent is not necessarily going to be forced to be true, right?

Â If b is true, then which constraint doesn't have to be hold, and

Â we're likely to get a compiler error like this, saying that

Â when the compiler tried to compile this down to the integer variant alldifferent,

Â it couldn't find the reified version, because we need the reified version.

Â You can give a name to the expression

Â in order to use it in this non top level conjunction.

Â 7:51

So a very important Boolean function is the forall function which maps a list of

Â Boolean expressions to a conjunction.

Â So when I write forall b1 to bn, it's exactly the same as writing b1, and

Â b2, and ... bn, and of course, it's very commonly used to define large

Â collections of constraints, because if this forall is at the top level and

Â all of these conjunction of constraints, all

Â get flattened down to individual constraints and sent to the solver, the solver can take a big conjunction, so that's what it does.

Â The exists function very similar,

Â maps a list of Boolean expressions to a large disjunction.

Â So exists b1 to b2, bn is exactly the same as writing down this expression,

Â and it's less used than forall because this expression all of these

Â Boolean expressions are going to have to be reified to build this disjunction.

Â So, we should try to avoid disjunction emeralds when possible,

Â of course it's not always possible. One of the key things of disjunction makes us able

Â to express many more things than they express without disjunction.

Â 8:54

So let's have a look at some examples of forall, exists.

Â Here we started off with a fixed array a and some variable arrays x and y.

Â To do we've got some interesting conjunction and disjunctions forall and

Â exists.

Â So what is going to be the result of unrolling each of these expressions?

Â Remember we have to basically break it down into a small expression.

Â So let's look at the first one, so this is looking at values i in one to 5, where

Â a of i is less than a of i plus 1, and we can see that the only places where that holds is value two, right?

Â Which is less than 3, and value 4 which is less than 5,

Â So basically this where condition passes only in the cases where i is 2 and 4.

Â And basically we're going to build up this expression, x[2] is less than y[2].

Â And because the forall is putting an and

Â between the two values, x[4] is less than y[4].

Â And that will be, what b holds, all right?

Â So this will immediately be flattened further.

Â We'll actually give this a Boolean value in order to take into account for

Â whether that's true or false.

Â This will give another Boolean value, and then we'll build a single flap and get the value of b.

Â All right, let's look at the second one.

Â If c exists, i and 1 to 6 where i of a is greater than 3, and

Â this test passes when i takes a value of 1 or 5,

Â and so this will be the constraint that will be generated,

Â x[1]+y[1] = 0 or x[5]+y[5] = 0.

Â But we have to be careful here, this y[1] is not defined all right.

Â Notice the value of the array y only has indexes from 2 to 6.

Â So indexing outside the array.

Â So this is the relational semantics view of

Â MiniZinc which says if I build up a undefined expression.

Â Similarly if I try to divide something by zero, then what I do is look for

Â the nearest enclosing Boolean expression and set it to false.

Â And then this y 1 occurs inside this plus.

Â That's not a Boolean that's an integer, and it also put it inside this

Â equality test that's a Boolean, so that is replaced with false.

Â 11:19

Let's look at our last expression, for all i in 1 to 6,

Â does there exist j in i+1 to 4, x[i] is greater than y[j].

Â So we start with i equal to 1.

Â And then j is going to take values from at 2 to 4.

Â So we're going to generate this expression, x[1] > y[2],

Â x[1] > y[3], and x[1] > y[4], and

Â then we're going to put them all together, because this is an exist, by this all.

Â So that will be the result of the first iteration of the forall.

Â Then I will take the value 2, j will take the values from 3 to 4,

Â that will generate these two primitive constraints here.

Â And we'll put them in disjunction, and

Â that'll be the second result of this expression for that second variable.

Â And of course, i is going to conjoin all results together.

Â 12:12

So next, we take i is a value 3, and j will take the value 4 only.

Â We'll get this (x[3] > y[4]), and it's disjunction with nothing else.

Â And so that will be the final result.

Â Now we've gotta think a little bit carefully,

Â because, what happens when i gets a value 4?

Â And j takes a value from 5 to 4, which is an empty set.

Â So basically, we're going to build the exists of an empty set, and

Â the exists of an empty set is true.

Â Then we're going to conjoin that true to this expression here.

Â But conjoining true is making no difference, and so this will be the final

Â result of this expression unroll. It would the have to be further redefined,

Â have to introduce Boolean variables for all of these expressions, and

Â redefine these to finally get that flat result.

Â So, Boolean expressions are one of the most powerful modelling features

Â available in MiniZinc.

Â But of course, whenever you introduce complex Boolean expressions, it's going to

Â cause difficulty for solvers and you have to be careful that global constraints and

Â complex Boolean expression don't mix well.

Â Usually you can only use a global constraint as the top level conjunction.

Â In many cases global constraints are basically a way of

Â capturing a complex Boolean expression.

Â And allowing the solver to do something special about that instead.

Â