This lecture will be about SAT solving. I will give the definition, and I will make some basic observations. First the definition. It's about propositional formulas. A propositional formula is by definition composed from Boolean variables and the number of operations. These operators are the negation, the "not", the disjunction, the "or", the conjunction, the "and", the implication, written as an arrow, and p implies q is equivalent to not p or q, and the bi-implication which, as the name already suggests, is just a combination of two implications. The propositional formula is defined to be satisfiable, abbreviated to SAT if it is possible to give values to the variables in such a way that the formula yields true. The mapping of the variables to these values is such a way that the formula yields true, that mappings is called the satisfying assignment. So, let's give an example. Here we have a formula p or q, and not p or not q, and p or not q. This formula is sastisfiable. Why? Well, if we choose p to be true and q to be false, we see that all parts of the formula yield true. So, the conjunction of the three parts also yields true. Here's a next example. It's a conjunction of four parts, and this formula is unsatisfiable. Since, no matter which values we choose for p and q, it's always the case that one of these four parts yields false. So, the conjunction is never true. So, this formula is unsatisfiable. SAT is the decision problem giving a propositional formula, is it satisfiable? Yes or no? The basic methods for SAT that always works is a method of truth tables. Essentially, this consists of computing the values of the formula for all possibilities of the values. If we have n variables, there are two to the power n, possibilities to check for all possibilities we check the corresponding- we compute the corresponding result. By definition, the formula is satisfiable if and only if at least one of the two to the power n cases yields true, abbreviated to one. Filling the truth table of an arbitrary formula is based on the truth tables of the building blocks, the operators, negation, distinction, conjunction, implication, and bi-implication. In fact, these truth tables of the building blocks define these operators. The first one is the negation. If p is zero false, then not p is true one, and conversely this defines not p. Disjunction is defined as follows, If p and q both are false, the result is false, and in all other cases the result is true. For the conjunction, it's the other way around. It only yields true if p and q both are true, and in all other cases it yields false. For the implication, we have p implies q as the same as not p or q. So, that means it yields false if p is true and q is false, and in all other cases it yields true. Bi-implication yields a one if p and q have the same value n to zero if p and q have different values. Based on these building blocks, we can make the truth table of an arbitrary formula. Let's give an example. Here we take a quite arbitrarily formula and let's build the truth table of it. So, we put the letters occurring in it and all combinations of zeros and ones that are possible for n variables. There are two to the power n rows in this truth table. First, we end up for all ingredients, we take the truth table based on the building blocks. So, for p and q, we get the following; it only yields a one if both p and one are true, and in all other cases it yields false. For p or r, it yields a zero in case both p and r are zero, and in all other cases it yields a one. For the implication, it only yields false in case the part before the arrow is true, and the part behind the arrow is false, but it turns out that it doesn't occur at all. So, here we get, for all cases, a one. If we put a negation around it, we get for all cases a zero. So, the conclusion is, of our formula, we have only zeros in the final column. That means that the formula is unsatisfiable. This truth table method always works, but it's exponential in the number of variables, since, the number of rows in such a truth table is two to the power n, if we have n variables. So, it's clear that this will be infeasible for big n, so we need something better if we want to use this in practice. The bad news is that SAT is NP-complete, and that's a theoretical standard for hard problems. So, it's very unlikely that a SAT solver exists that is efficient for all formulas. In fact, this whole SAT analysis was the starting point of research in NP-completeness. Many results on NP-completeness and eventually they all boil down to NP-completeness of SAT. But now we have the good news, and the good news is very good news. It's a big surprise, namely; current SAT solvers are successful for several big formulas. As an example, we will mention it in a later lecture, we will see that solving the n-queen problems for n is 100, that yields a 50 Mb formula over 10,000 variables, but is solved in only 10 seconds by the SAT solver Z3. So, success stories are not only in this toy problem, but they exist from a wider range of application areas. In the forthcoming lectures, we will see extensions to SMT, then we not only deal with Boolean variables, but also with numbers and inequalities. We will consider tools for SAT and SMT, and we will describe the syntax to SMT-LIB syntax in which they can be expressed, and the tools can apply on, and we give several examples and applications. There will be several lectures on the underlying mechanisms and the theory. But for now, the main thing to remember is NP-hard is not always hard. Thank you.