0:05

Welcome. In this lecture,

Â I want to show you Gaussian elimination as

Â a simple technique to solve Boolean equation systems.

Â So if you have Boolean equation systems,

Â then the question is how can we systematically solve that?

Â And if they are relatively small,

Â then there's a very elegant method - and that's called Gaussian elimination.

Â And Gaussian elimination got this name after Carl Friedrich Gauss,

Â who invented this rather famous method

Â to solve linear sets of equations in number theory.

Â And because our method somewhat resembles this approach,

Â we also call this Gaussian elimination to solve Boolean equation systems.

Â What's the idea of Boolean - of Gauss elimination?

Â Well, there are three rather simple rules and I will explain these rules.

Â So the first rule is called variable elimination.

Â If you have a single equation of the shape nu X is phi,

Â then we can replace it by this equation,

Â where you place every occurrence of X in the right-hand side by true.

Â So all the occurrences of X in the right-hand side are removed in this way.

Â And the fact that we take true is directly related to the maximal fixed point.

Â If you have a minimal fixed point equation,

Â then we replace X by false.

Â And this can always be applied at - in a Boolean equation system,

Â but we will specifically apply it at the last rule of the Boolean equation system.

Â So let's take our example.

Â And let's look at the last creation.

Â It says mu Y is equal to X or Y.

Â And now, because it's a minimal fixed point operator,

Â we can replace Y in the right-hand side by false.

Â So what we obtain is this.

Â And then you can simplify the equation a little bit.

Â And this is what we have.

Â In particular, note that Y does not

Â occur anymore in the right-hand side of this last equation.

Â Now, look at the second rule.

Â That's called backward substitution.

Â So if you have a sequence of

Â Boolean equations - and here the sigmas indicate either mu or nu,

Â so we can do it with arbitrary fixed-point operators.

Â And we look at the last equation.

Â Then this says sigma Y is equal to phi.

Â And what we can do is we can substitute the phi for Y in all earlier equations.

Â And this is what we obtain.

Â And what we see is that we remove Y from all earlier - all earlier equations.

Â 3:10

So if we apply this to our example,

Â the last equation says mu Y is X - and now we

Â can replace every occurrence of Y in the early equations by X.

Â So we obtain this equation - nu X is equal to X and X.

Â We now forget about the last equation,

Â because Y does not occur anywhere anymore in our Boolean equation system.

Â And what we have done now is that we removed all occurrences of

Â Y and we actually obtained a really smaller equation system.

Â And what we can do is repeat this procedure until we only have one equation left,

Â namely the first equation - and have a right-hand side that is equal to true or false.

Â And then we know the solution for the first variable of our Boolean equation system.

Â But first, let's simplify this equation.

Â So we get nu X is X as the first equation.

Â And we can then apply variable equation - variable elimination to the first equation.

Â So we have nu X is X.

Â And because it's a maximal fixed point operator,

Â we can replace by nu X is true.

Â And we know the solution for the first equation of our Boolean equation system.

Â Now we have the third rule, that forward substitution.

Â And we can only apply forward substitution if the right-hand side of

Â the equation that we use for substitution does not contain variables.

Â So let's look at the general scheme.

Â Here we again have a sequence of Boolean equations.

Â We have these minimal and maximal fixed point operators in sigmas - indicated by sigmas.

Â And if phi does not contain variables,

Â so it's effectively equal to true or false,

Â then we can substitute this true or false for all occurrences of Y elsewhere.

Â So let's apply that to our example.

Â We have nu X is equal to true.

Â And because the right-hand side does not contain variables,

Â we can substitute true for X in all later equations.

Â Well, that's only one in this case.

Â But we simply obtain X is equal to true and Y is equal to true as

Â the solution for our Boolean equation system.

Â And what we have seen is a very general method.

Â This works for all Boolean equation systems.

Â I mentioned that the order of Boolean equations is important for the outcome.

Â So what we can do is we can take

Â two Boolean equation systems with exactly the same equations,

Â but the order of the equations is different.

Â And we can try to solve both sets and see that the answers are different.

Â So let's look at the first equation system.

Â The second equation already does not have a Y in its right-hand side,

Â so we do not have to apply variable elimination,

Â but we can immediately apply backward substitution.

Â And what we obtain is,

Â as first equation, nu X is equal to X and X.

Â And because the first equation is a maximal fixed-point equation,

Â we can use variable substitution and replace X by

Â true and we obtain nu X is equal to true.

Â And if we then do forward substitution,

Â we obtain mu Y is equal to true.

Â And we have solved this Boolean equation system.

Â Let's now also solve the second Boolean equation system.

Â So we first apply variable elimination on the second equation.

Â We still have an X in the right-hand side and replace it by true.

Â We then substitute the Y and we simplify the equation.

Â And we - so we get nu X is Y and we substitute Y for X in the first equation.

Â And we can now apply variable elimination to the first equation.

Â And now we have solved the first equation.

Â Do forward substitution, and we obtain,

Â as a solution, Y is equal to false and X is equal to false.

Â So if you look at this solution - and we look at this solution,

Â I think it's completely obvious that sequence in which the variables

Â occur do matter for the solution that we obtain.

Â So one of the questions is how efficient Gaussian elimination is.

Â And although it looks quite straightforward,

Â the procedure is still exponential,

Â although it's quite hard to figure out why that is the case.

Â Actually, the situation around solving Boolean equation systems is quite weird.

Â So for that, we have to understand

Â that solving a Boolean equation system is in NP and in co-NP.

Â So problems in NP are those problems where,

Â if you can give an answer yes to an instance of such a problem,

Â then you can check that in polynomial time.

Â So calculating it might be hard,

Â but checking that the answer is correct might be easy.

Â And problems in co-NP are those problems where if the answer is no,

Â you can check that easily.

Â And there's a big subclass of

Â these problems and that are those problems that you can simply solve in polynomial time.

Â So you can then also check whether the answer is yes or no.

Â And that's both in NP and in co-NP.

Â What we see here is that there is an area above this red area,

Â this triangle - and that are those problems that are in NP and in co-NP,

Â but do not have a - a polynomial algorithm.

Â And what is commonly believed is that there are no problems in this area.

Â So for a long time,

Â it was believed that primality testing was in this area,

Â so it was in co-NP and it was in NP and no polynomial algorithm had been found.

Â But ultimately, people came up with polynomial algorithm.

Â As it appears now,

Â solving a Boolean equation system is in NP,

Â it is in co-NP and we still do not have a polynomial algorithm for it.

Â And this causes a lot of people to

Â believe that we should be able to find this polynomial algorithm,

Â although I spoke to a few colleagues that said that they were

Â giving up on this because it's so hard to find one.

Â Let's look at exercises.

Â In a previous lecture,

Â we had this formula.

Â And the question was how does

Â the Boolean equation system look like to

Â verify this formula on the given transition system?

Â And the answer was this.

Â And now the question is can you solve this Boolean equation system?

Â And how does the solution look like?

Â So what did we do?

Â We introduced Gaussian elimination as

Â a set of three simple rules to solve Boolean equation systems.

Â And Gaussian elimination is fairly useful to solve

Â simple Boolean equations - equation systems.

Â We showed that the order of

Â equations in a Boolean equation systems is of importance for the solution.

Â And we also shortly hinted that it's still an open question

Â to find a polynomial algorithm to solve Boolean equation systems in general.

Â Fortunately, for all those Boolean equation systems

Â that we generate for our practical applications,

Â there are efficient algorithms and we can solve them quite quickly.

Â So we are now at the end of the third MOOC,

Â where we looked at modal formulas to express requirements on behavior of systems.

Â In the next MOOC, we will deal with application

Â of everything we learned to a whole range of examples.

Â I hope you enjoyed what I told you and I really hope to see you in the next MOOC.

Â