This lecture is about solving Sudokus by SAT/SMT. Here we see an example. Maybe you know this kind of puzzles. Let's first give the rules of the game. We should fill the blank cells in such a way that in every row, and in every column, and in every fat three times three block, exactly the numbers one to nine occur, all occurring exactly once. Doing by hand this puzzle, the first steps are quite easy. For instance, on this position, we can put a two. Why can we do that? Well, in this block, there still should be a two. In this line, there is no two allowed since there is already a two. In this column, no two is allowed since there is already a two. So, this is the only position in this block where two is allowed. After a few steps, this particular puzzle becomes very hard, and backtracking and/or advanced solving techniques are required. In fact, I designed this puzzle myself. A few years ago, I wrote a book about Sudokus and generating Sudokus, and for preparing that book, I wrote some programs to generate it, and this particular example was one of the hardest. Solving by hand can be hard, but for SAT/SMT, it's really peanuts, it's just specify the problem. How can we specify the problem? Well, there are different ways to do that, and in fact, all work well. A first approach would be, do it in pure satisfiability, just boolean variables. For every cell and every number 1 to 9, introduce a boolean variable describing whether that number is on that position. Then, we have 9 to the power 3 is 729 boolean variables. It looks a lot but for SAT solvers, it's no problem at all. A second approach is that we apply SMT. For every cell, we just define an integer variable for the corresponding number. Here we exploit the latter. How to specify that in every row and in every column and in every three times three block exactly the numbers one to nine occur all exactly once? Again, this can be done in several ways. We chose to specify that these numbers are all at least one and at most nine, and they are all distinct. Then the next question is, how to express that the number of numbers is distinct? Well, we could do it directly. Simply, for every pair, write down that they are different, not equal. But the SMT syntax also has a special construct called distinct and that can be used by just writing down distinct and then the variables that should be distinct. Doing so is very straightforward. We start by declaring the variable. Well, in fact, we only have one function to be declared depending on two integers and the result is also an integer. Next, we have the requirements by and assert, and what are the requirements? Well, all values should be greater or equal 1, and less or equal than 9. Here it's specified for A 1 1, but it's similar for all other IAGA running from one to nine. And next, the elements in a row, let's say row one should be distinct, and that is described by this formula. And similar for the other rows, and similar for every column, and similar for every three times three block. Like distinct and here we see the elements of the upper most leftmost three by three block. And then the full formula is concluded by the given numbers in the Sudoku puzzle. On position one three row one column three, there was nine, so we simply gave that that value should be nine. And for one four it should be eight and so on. This we do for all given numbers in the Sudoku puzzle. And now applying the set 3 or any other SMT solver on the resulting formula, yields a satisfying assignment giving the values for all variables being the solutions of the Sudoku puzzle and this hardly takes time, it's within a fraction of a second. Here we see the puzzle as it was given, and if we fill in the values as they were found by the SMT solver, we get these values and indeed you can check that everything is okay. So, this is a solution of this puzzle found in the fraction of a second while for a human, this is a hard job. Great part of the formula is the same for all Sudoku puzzles. Namely, the value shoot in between one and nine, and in every row, column and block the values should be distinct. And the rest of the formula just specifies the values given in the Sudoku puzzle. And in this way, we can quickly solve all Sudoku puzzle as you find them in newspapers or whatever. The next question is, how to generate a puzzle? And surprisingly, using this idea, we can also find a way to generate Sudoku puzzles ourselves. The idea is as follows: We start by a full Sudoku, let's say a solution of any Sudoku puzzle. And then we remove given numbers one by one until the formula extended by the negation of the known solution is satisfiable. So, the formula we build, we are not only looking for a solution, but we are looking for the solution which is distinct from the known solution. And if this exist, it does not have a solution. But if it does not exist we know that the solution is the only one. And then the idea is, if we do not take the last one which is satisfiable, but one before, we know that by construction it's a Sudoku having a unique solution. And that can be the new Puzzle generated in this SMT approach. Concluding, solutions of Sudoku puzzles are quickly found by just specifying the rules of the game and SMT format and apply an SMT solver. And for many other types of puzzles: Kakuros, killer sudoku, binarios, there are lots of other kind of puzzles. The SAT/SMT approach works very well to solve or generate such puzzles. Thank you.