So, welcome to the reference material on Booleans Expression. 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 or or the global constraints. They can also build Boolean Expressions of more complicated form using Boolean. 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 ether b1 is false or b2 is true and, blimplication, requiring that they have the same truth value, and of course negation, and Boolean expressions can appear frequently in parts of music bottles as constraints as already said as the way it conditions. When we have loops with wear conditions, as the conditions are anything else in Gifs statement, or the values of Boolean variables or parameters. 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 [INAUDIBLE] variable and 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 revenue 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 so, we're going to have to decide it first. So, what's the value of h variable? So, it's fairly easy to see that x is greater than 0. So, b is going to be 2. When we look at the sum, when is I rho equals to 0. That is the case when I is 2 and when I is 3. So we going to end up with second and third y of r which is 5 and 2 to get 7 Now, we look at this pool of expression, we can see the big 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 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. 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 [INAUDIBLE] are true regardless of the value of u. 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 pace, 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 produced, coincident or have a Manhattan distance of at least d, and so these Boolean connectives 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 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, 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 it could 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 or 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 b 1 is the name of whether this constraint holds or not. It takes a truth value of this constraint. This is what this is, b 1 is true if z is greater than 0, and b one is false if x is not and zero, and simply b2 is going to be the name of this constraint and then we can just write a simple or at least Boolean variables. I think that this is a constraint we're to replace to Boolean variables, and so it didn't matter what we had, out complicated the expression was here because we've given it a Boolean name of whether that's true or false and we can write a simple dis-junction only on Boolean variables, and nothing else. So, top level conjunctions don't cause problems for flattening. So if we consider the very similar constraint here, x > 0 / \ 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 halt. They're both forced to halt 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. We're going 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 all different based on x3, so this all different 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 variable different, 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. 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 [INAUDIBLE] 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, or get individual constraints can take [INAUDIBLE], so that's what it does. The exists function very similar, maps a list of Boolean expressions to a large disjunction. Like exists b1 to b2, and exactly 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 when these things of disjunction makes us able to express many more things than they express without disjunction. So let's have a look at some examples of forall, exists. Here we started off with a fixed array a and some variables 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 see that the only 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 need to 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 and [INAUDIBLE]. 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. And that is the value here your right y indexes from 2 to 6. So indexing outside the array. So this is the relational semantics view of mini secret says if I build up a undefined expression. Similarly if I try to divide something by zero, then what I what do is look for the nearest closing 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. So, false or something is equal to the something, so we can just sub divide that and c is the result. The name of whether x 5 and y 5 equals 0. 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 for all. Then I will take the [INAUDIBLE] generate 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. 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 and get those, 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 [INAUDIBLE] difference, and so this will be the final result of this expression unroll [INAUDIBLE] have to be 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. That brings us to the end of the section.
