This lecture is about rectangle fitting. What's the problem of rectangle fitting. Given a big rectangle and a number of smaller rectangles, can you fit the smaller rectangles in such a way that they all fit in a big rectangle without overlap? This problem looks like just a puzzle but it has important implications. You can think of chip design, if you have to design a chip consisting of chip components all being rectangular, you have exactly this problem. Another application is printing posters, you can think of you have to print a number of posters of different formats it's all being rectangles and they have to be printed on a big sheet again a rectangle, again an instance of this problem. But let's start by a simple example. Here we have a big rectangle and here we have five small rectangles and the question is, it possible to fit the five small rectangles in such a way that they fit in the big one. Well, we can try to try the first one and then the second one. And then after a number of steps we have this situation and we see the remaining two do not fit anymore. And then we can do backtracking in several ways and we can think about backtracking how to do that. But one of the messages of this course is, do not think about it, just specify the problem and let dissolving solve the problem, let the dissolving do the backtracking for you. So, the question now is we have to specify the problem and then we will fit a solution. Here, we will see a solution that is found in this way. Okay, how to specify this problem? Well, let's number the rectangles from 1 to n and then we introduce a number of variables. We introduce variable W_i expressing the width of rectangle number i and H_i expressing the height of rectangle number i and an X and a Y coordinate of the left lower corner of that rectangle. Summarized in a picture, we see here the situation and the idea is we collect all requirements in a formula and we start by the width and height requirement. Let's say the first rectangle has width four and height six and then we can specify we have W_1 is four and H_1 is six, but it can also be the other way around if the rectangle is turned 90 degrees. So, this is the formula we get for rectangle one and similar for the other rectangles. The next requirement is all rectangles have to fit in the big rectangle. How does that look like? Well, then first we should define the coordinates of the big rectangle. Let's say 0,0 is the coordinates of the left-lower corner of the big rectangle and W is the width of the big rectangle and H is the height of the big rectangle. And now, we can express the requirements, the rectangle number i should not be too far to the left because requirement X_i should be greater or equal than zero. And not too far to the right. That is X_i plus W_i should be less or equal than W and similar for the height requirement. The next requirement is the non-overlappingness. The remaining question is how to express the requirement of non-overlapping. Let's first investigate what does it mean that two rectangles overlap. Here, we see two overlapping rectangles and we see one of the requirements of being overlapping is that the left part of rectangle j should be left from the right part of rectangle number i, expressed in a formula that yields X_i plus W_i is strictly greater than X_j. So, that is one of the requirements for overlapping, but we get four of such requirements. We also get such a requirement for i and j swapped then we get X_i is less than X_j plus W_i and we get the same similar for the vertical. So, then we have Y_i plus H_i strictly greater than Y_j and similar for the other way around. And these four requirements together exactly express the requirement of overlapping and we want no overlapping. So we should take the negation of this formula stated here and this can also be expressed equivalently by or/and removing the negation. And now, we get this requirement for every pair i,j and note that if we have n rectangles, we get quadratic number of such requirements, but that's no problem as empty solving can easily deal with a big number of requirements. Summarizing the full formula reads. First, we have a requirement for having the right width and height. Next, we have a requirement that all smaller rectangles fit into a big rectangle and finally for all i left in j we have a requirement that rectangle i and j do not overlap. The resulting formula exactly describes all requirements of our rectangle fitting problems and it's composed from linear inequalities and propositional operators like negation, conjunction and distinction. Hence, it is perfectly suitable for SMT solvers. The formula is satisfiable if and only if our fitting problem has a solution. That means it cannot only be used, this approach can not only be used for finding solutions, but also for proving that no solutions eX_ist in contrast to other approaches like using genetic algorithms. If the formula is satisfiable then the SMT solver yields a satisfying assignment that is the corresponding values of all X's, Y's, W's and H's for the small rectangles and from these values we easily obtain the solutions we want to see. Applying a standard SMT solver like Z3 or Yices or CVC4 this approach works well for problems until let's say 20 or 25 rectangles which is quite substantial and bigger than you could easily find by Hent. For generating the resulting formula typically hundreds of lines if you have the size of 20 or 25. Never write the formula yourself but just write a program or script that generates the formula. This is much easier and you make less errors using that and we conclude by an example found in this way which is slightly bigger. Thank you.
