[MUSIC] This lecture is about the eight queens problem. In chess we have a queen, and the queen is a piece that may move horizontally, vertically, or diagonally in any number of steps. And now the question is, is it possible to put 8 queens on the chess board in such a way that no two can hit each other? Well, we want to solve this problem. And as usual in SAT/SMT solving, we do not think about how to solve it. We just specify the problem, and then the SAT or SMT solver may find the solution automatically. And in this problem we can do in pure SAT. We do not need numbers. We do not need inequalities. We just need boolean variables. The idea is for every position in the chess board, we choose a boolean variable stating whether there should be a queen on that position or not. So organized for the whole chess board, we get these 64 variables. Each expression, whether on the corresponding position, there is a queen or not. And whether a field is black or white, that doesn't play a role. We just want to express everything in these 64 variables. Let's first consider rows. Here we see a row, and what's typical for a row? Two Ps are in the same row. Pij and Pi'j' are in the same row if and only if i = i'. Let's investigate such a row. For such a row, we have the requirement that there should be at least one true, and at most one true. At least one, since in total there should be eight queens. So on every row there should be at least one queen. And on every row there should be at most one queen, otherwise they can hit each other. So let's start by at least one queen. That is easily expressed in the following formula. At least one of these Ps should be true. It can be expressed by simply taking the or of all of these variables. And in shorthand notation, we can write it in this way. The next requirement is that we should express at most one of them is true. How can we do that? Well, if we have a sequence of variables, and at most one may be true, that means if we take two of them, then it's not allowed that both are true. So if we take two of them, at least one of them should be false. And that's expressed in the formula not Pij or not Pik should be true. And this should be true for every j less than k and expressed in the formula in the shorthand notation that looks as follows. Next we consider columns. Well, for columns we have exactly the same requirements. The only difference is that now the i and the j are swapped. The requirements we have until now are. We have requirements for at least one queen on every row, at most one queen on every row, at least one queen on every column, at most one queen on every column. And now it remains to express the requirements on diagonals. On every diagonal there should be at most one queen. Let's consider such a diagonal. What's typical for such a diagonal? Well, here we see that two elements are on the same diagonal Pij and Pij' if they have the same sum. In this case, the sum is 11. 8 + 3 is 7 + 4 is 6 + 5, and so on. And now we should express that it's not allowed that two of these variables are both true. In the other direction, we have something similar. We again make a picture. But now the requirement is not the sum, but expresses the difference. Pij and Pi'j' are on such a diagonal if and only if i- j = i'- j'. So for all i,j i'j' in such a way that ij is different from i'j'. But they are on the same diagonal, expressed by i + j = i' + j' or i- j = i'- j'. We have the requirement that it's not allowed that both are true. So not be ji or not be i'j' should hold. And we can do this for all ij i'j'. But then we have many things double. We may restrict to the cases where i is less than i', and then here, we have the big formula. We let i and i' run over all values from 1 to 8 and j and j' run on all values in such a way that they corresponding two positions are on the same diagonal. Now we have collected all ingredients of the total formula, and here is the total formula presented. The resulting formula looks quite complicated, but it can easily be generated in the required SAT syntax by a program you can write in your favorite programming language. The total formula consists of 740 requirements, which is quite a lot. But a SAT solver can easily find a solution. It finds that it is satisfiable. And from the satisfying assignment, you can easily reach the solution. And here, you see one of the solutions. I want to give some further remarks. There is not just one solution. In total, there are 92 solutions. And you can find all of them by the following trick. First find one in the way we just described, but then, add the negation of the found solution to the formula and again apply the SAT solver. And this you can repeat. You can do it by hand, and it is quite elaborate. You can also write a script, doing this automatically. And then, it turns out, that after having found 92 solutions and adding the negations of these 92 solutions, you get a formula that is unsatisfiable, showing that, apart from these 92 solutions, there are no more solutions. And we have, indeed, all solutions. The problem can also be generalized for n queens, for n greater than 8. And it's quite surprisingly, that even for n is 100, Z3 is able to find a solution quite quickly. Then the formula is quite big, something like 50 megabytes, but within ten seconds on a normal computer, a solution is found, which is quite surprising. You can also use the same problem, the same approach for the variant of the problem, namely the situation where already a number of queens have places on the blackboard, a number of Ps already have been put to true. And the question is, is it possible to fill the rest of the chessboard in such a way that it satisfies the requirements. And this is known to be an NP-complete problem. But this approach can be used to solve it for not too large numbers. Summarizing, we gave a way to express this chess problem in a SAT problem. The SAT solver can solve it. We generate the formula by some program. And then the SAT solver is applied to the resulting file. And this is done quite immediately. And we conclude by another solution, thank you.
