This lecture is about the simplex method. The simplex method deals with linear inequalities. Let's start by an example. Can we find real numbers x and y such that x is greater or equal y, y is great or equal 2x, and 2x plus y is less or equal than 7. Let consider this in a picture. Since we only have two variables x and y, we can draw this in a plane, an x direction and a y direction as usual. Let's consider this line. This is the line expressed by the formula x is y. On one side of the line, we have the values for which, x is less or equal than y and on the other side, we have x greater or equal than y. Let's consider another line, this one, horizontal line. On top of it, we have values y greater or equal than two and below, we have values y less or equal than two. As a third example, consider this line. On one side, we have 2x plus y greater or equal seven and on the other side, 2x plus y less or equal seven. So, the red part exactly expresses the values x and y such that x is greater or equal y, y is greater or equal than two and 2x plus y less or equal than seven. So, indeed there are real values such a way that these three inequalities all hold. For more than two variables, we cannot make such a picture anymore and in our applications, we do not want to do this for two or three variables, but thousands of variables into thousands of inequalities. So, we have a very high dimensional space in which we search for a solution. In our SMT approach, we have formulas with linear inequalities but also disjunctions and conjunctions. But the underlying approach here for this is the simplex method. The simplex method is a method for linear optimization, also called linear programming. In linear optimization, we are not only interested in whether there is a solution, but we want to find the optimal one, that is, we have a given linear expression and we are interested in the highest possible value for this linear expression, this goal function. So, among all are real values x1 until xn, and we require that all should be greater or equal zero. We want to find the maximal value of a linear goal function and they should satisfy k linear constraints expressed in a way like this. Here the v, and s, and c's and b's are given fixed real values and the requirement here is that the b's are greater or equal zero. That means, we always have a solution namely, the axis all have value zero. Then, it satisfies that all constraints. So, choosing all values x to be zero, we have a solution and this is called, the basic solution. But probably, this is not the solution with the maximal value for the goal function. So, now the approach of the simplex method is, start from this solution, in which all x is a value zero and then try to do steps by which the value of the goal function increases and the steps are called pivots. This applies to a more general format. For instance, if the inequality is not less or equal but greater or equal then we can simply multiply both sides by minus one. Here we see in example. If we have an equality rather than an inequality, we can replace the equality by two inequalities A is B is replaced by A less or equal B and B less or equal A. If one wants to minimize rather than maximize, just multiply the goal function by minus one. If a variable x runs over all reals, positive and negative, we are required that all variables should be greater or equal zero. Well, then such a variable x is replaced by x1 minus x2, for fresh variables x1 and x2, satisfying x1 and x2 greater or equal zero. We get an extra variable, but the tools can deal with it so we should not worry about it. A less trivial issue is how to deal if there is no trivial start solution as we had in our case where the b's are greater or equals zero. That's less trivial and that we will consider later. Now, we focus on the situation where all b's are greater or equal zero and we have a trivial start solution. The first step before we really apply the simplex algorithm is that we bring it to slack form. With slack form, dealing with equalities is easier than for inequalities. So, for our inequality, we introduce a fresh variable y_i greater or equal zero, and we replace it by the following equality. We just say, the part which is greater or equals zero is renamed to y_i, and we have the requirement y_i greater or equals zero and together with requirement y_i is greater or equal zero. This is equivalent to the original inequality. This format with equalities is called the slack form. Let's give some terminology on a slack form with equations. We say that the solution where the values of the y's isn't b's and all x's have value zero, that's called the basic solution. Y variables, the variables left from the equality sign are called the basic variables and the x variables, right from the equality sign, are called non-basic variables. Now, the simplex algorithm consists of repetition of pivots in which pivot chooses a basic variable and a non-basic variable and swaps their roles. So the basic variable becomes non-basic and the other way around. Then the result is brought to slack form again and the slack form which is equivalent to the original one, but with a higher value of the goal function. The idea is we repeat this until a further increase is not possible anymore and then we have found the optimal value. How this works in detail, we will see in an example in the next lecture. Thank you.