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.