So, Workshop 5 is about debugging. So, Jimmy and I have swapped seats, because Jimmy's going to solve this problem, because I made it, and I put the errors in, but Jimmy doesn't. So, this is the worst kind of debugging. This is debugging someone else’s model. Normally, you'll be debugging your own. So, go for it, Jimmy. >> Okay, thank you, Peter. So, Peter is Liu Bei, this time. He's the one, who's written this buggy model. So, let's take a look at the model together. Let's go to MiniZinc. Okay, that's the buggy model. Let's go through the model together. As you can see, the first three parameters k, l, and m are the one’s as described in the specification. k stands for the number of E type of stanza, l is the number of S type of stanza and m is the other kind of stanza. And making use of the three parameters, we defined ranges. ESSTANZA which is from 1 to k+l. And then the other type of stanza, we have a value of 0. And making use of that we defined the range stanza. So, we use 0 to denote the other stanza, one up to k will denote the E type of stanza and then from k+1 up to l would be the S type of stanza. Then we also have an enumerated type, KIND, to denote the different types of stanza. E, S, and O and then making use of that we would define an array KIND. Okay. Which has the first k elements as E, and then the last l elements as S, which stands for the kind of stanzas. Okay. Let's scroll down and then we also have another array, effect, which denotes the effectiveness of each of the stanzas. Okay. Remember that, both the effectiveness of the E stanza and the S stanza would both be put into the same array here. Right, Peter? >> Yeah. >> Okay. Then we also have the parameter n. That would have k+l+m. Which is the total number of stanzas we have in this poem here. And of course, making use of that, we also have a range 1 to n which stands for the position of the different stanzas in the poem. Okay, let's go to the variables here, okay. We actually are making use of the two viewpoints of the problem. In the first viewpoint, we have a variable array called place for each of the E, S type of stanzas. Where would we put that stanza, right? >> Yup, that's right. >> Okay, the second one is from the other viewpoint. We have for each of the positions or order in the poem what kind of stanza will we put in there, and remember that our 0 stand for the other stanza. Okay, so far so good. These are all the parameters as well as the variable of the model and then Peter also put in a symmetry breaking constraint in there which is guaranteed to be correct, >> Okay, so I put this in because it's going to make your solving much quicker, so some of these problems can take a lot of time to solve so adding this in is going to make the solving quicker, so you know it's correct Jimmy. >> Okay I don't have to worry about it. But essentially this constraint will enforce that the first position must be either an E or an S stanza, and then whenever we have two other stanzas in a row then they have to happen at the end of the entire poem. Okay, now we go into the potentially buggy part of the model, okay? Let's take a look at the first one. I think what Peter is trying to do is to channel the two viewpoints together, okay. And then we also understand that this is yet another permutation problem and that's why we will have a alldifferent constraint here. And then the next constraint says that hey if I have two stanzas of the same kind then, they must not appear in sequence. Okay. I think that's what it's talking about here. And then the last constraint essentially is going to compute the objective value. The objective value of this problem is to sum up the differences of the effects of the E or S stanzas. It will sum them up, and then we would like to maximize such an objective value. So let's load some of the data in there, and see how buggy this model is. I like calling this up, this way. Then we will run the model. And then, lo and behold, we get UNSATISFIABLE. So, this is difficult, because it's the worst of its kind, right? >> Right, this is the worst kind of bug, right? UNSATISFIABLE tells you very little. >> Okay, I think I have two ways of debugging this model because it is missing a solution. So one of the possibilities is for me to remove some of the constraints in the problem and see which one is really causing the unsatisfiability of the model. But the other possibility is that I'm seeing a whole bunch of forall in the model here. And also some in here, as well. I think what we learned in the lecture is that we can make use of the trace function. >> Yeah. >> And see what's going on with this, forall, okay? So I think that's what I'm going to do first. >> Okay. >> Okay. Maybe I can enlarge this a little bit. Okay. I'll put a trace function here, okay. I'm not copying properly. Okay. And then I'll paste the same thing here. And then, okay, what do I want to print out? I would like to print out the indices of the arrays there, so I'll put them in parenthesis. The same thing for the j Okay. >> You can see why I do most of the workshops. I can type faster than Jimmy. >> Right, okay, okay. >> [LAUGH] >> Then I also need to do this and then I'll run and see what's happening. Oh, I’ve forgotten to put a backspace (linefeed) there and then I run again. Let's take a look at the output. Wow, okay. So as you can see you know, this is a whole bunch of channelling between the place viewpoint and the what viewpoint. And then I think in the forall there, Peter has been very careful. Right? i is in the range of E or S type of stanza and j is in the range of position. So what we are seeing is, our i would be from one, up to six if we look at our data here, so we have k type of E stanzas, l type of, no k number of E stanzas, and l number of S stanzas, so altogether they have six, right? >> Yeah. So this looks okay, and then also for each type of i then we have 1 up to 9, so there's no array out of bound. So this looks okay. Let's take a look at another one. We have another forall in here, we could do exactly the same thing, put a trace here. Okay. I would also like to copy this. I hope I can type faster this time. >> [LAUGH] >> And then, I would also like to Debugging is fun, but it also takes a lot of typing. >> It does take a lot of typing, and a lot of time. >> Yeah. >> In fact, as you get to more complicated models you'll spend most of your time debugging. >> Yeah. >> It's not that difficult to get an initial model. Remember to put the new line in this time. >> All right, okay, thank you, Peter. Okay new line. Okay so let's run and see what's happening. So the purpose of this constraint is really to make sure that, if we have two E type or S type of stanza, if they are the same kind, then we would prevent them from appearing next to each other in the sequence of stanzas. And then let's take a look at here, okay? kind[1] and kind[2], kind[1] and kind[3], kind[1] and kind[6]. And then we have 2, 3, 2, 4, 2, 6, 3, 4, up to 3, 6, 4, 5, 4, 6, 5, 6. Okay, again, I could not see any array out of bound here. >> Mm-hm. >> So things look okay. How about the last one? sum essentially is also a loop, we also put the trace there and see what's happening. Now we add a trace. Okay, again. Okay. Okay, yes, a new line, I remembered this time. >> [LAUGH] >> Okay. And then, I will also like to look at this here. And what will happen if I run it? UNSATISFIABLE. Okay. Okay. >> It's probably earlier. >> Yeah. >> The trace has happened not necessarily in the order that you wrote them in the program. >> Right, okay. >> But in the order that MiniZinc processed these parts of the code. So have a look if it's there earlier. >> Okay. >> You might want to turn off the other ones. >> Right, right, right. Okay. Yes. They are printed at the beginning. Okay? >> Mm-hm. >> Again we could not see any, okay, If all the arguments to what they are just from 1 to 8 and then 2 to 9. Okay. But let's take a look at the definition of the array, because unfortunately I will not be able to print out the value of what[p], right? >> Right. Because trace is before the solver. >> Exactly. >> And what[p] is decided by the solver. >> Right. So I cannot do that. Okay and let's take a look at the definition again. Okay. The values that we could, the values of what would be STANZA. >> Mm-hm. >> Okay and then you could also see that the indices of effect should take the type, the range ESSTANZAs. There seems to be a mismatch here, because when I was looking at the output here I could see that what could have the possibility of having 0 as a value. >> Yep. >> If we have effect 0, that means out of bound so that could be a possibility of the you know. So what I would do is to, so there could be potentially a bug here. Let's see how we could, I'll copy first and then I'll comment it and then first of all, I'll remove the trace in preparing for fixing the code. Okay, so I think what's happening is that I remember from the specification, it says that we are summing up the differences in the effectiveness only for E or S type of stanza. But here, in the definition here, we are trying to sum up the effectiveness of all kinds of stanzas. I think that's where the bug is. So I think what we should do is to add an if then else in here. So I would like to check that if the kind of stanza for p is equal to other or… Okay, okay, I'm running out of space here. Okay. I should check that… >> You've got two copies of what[p]. >> what[p]. Okay. >> kind[what[p]] = other \/ kind[what[p]] = other. >> Okay, yes, thank you. p+1, either one of them. then we actually have a 0 here. >> Mm-hm. >> else, I should put else down there. Then I would have the absolute difference between the effectiveness of the two stanzas. >> Yep. >> Okay let's see whether it will run. Okay always save. Okay. >> You're missing an endif. >> Yes. This I always do. So what I should do is to put an endif there, save it again, and then run. Okay. But it's still UNSATISFIABLE. Okay, okay. There's still bugs in there. Then I will have to resort to the second way of debugging. Because we have a missing solution here. So what we should do is to start commenting out some of the constraints in there and see what's happening. So let's try to comment. >> Actually, before you go on Jimmy, I might point out something before we go down that path. Because this what[p] can take a value from 0 to E stanza, and what's the array index for kind? Array index for kind. Let's take a look. Array index for kind. ESSTANZA. >> Yeah, you've actually trying to fix the use of looking for an other, you've on the wrong test. Can you write that test which doesn't use an array? >> Right. So essentially, I should not need to use kind, I should just test. Exactly. This is better? >> Yup. >> Okay, so I hope I have fixed the bug here. But we'll see, right? As I said, we should start commenting out some of the constraints- >> Well, run. >> Run? >> It might work now. >> All right, okay, >> Still UNSATISFIABLE. >> Okay. >> Okay! I know it's going to be hard. >> [LAUGH] >> We would comment out this constraint and see what's happening. We will run again. Still UNSATISFIABLE! How about this one? Oops. We are getting some output. >> Yup. >> So it seems that the alldifferent constraint could be our culprit here. What's wrong with that? Okay, let's take a look at the definition of what again. The what variable array would have stanza as value. Look at the definition of stanza again. Up there, okay. stanza is the range from 0 to k + l. We have 0 to stand for the other stanza, we also have 1 to k to stand for E stanza, and then k + 1 to l to stand for the S stanza. So that means, in the what array, we could have a whole bunch of 0 values in there, to stand for the other stanza. So actually, I think I could see the problem here right now. Instead of using the alldifferent constraint, we could use an other global constraint that we have learned before, this is called alldifferent_except_0. >> Yeah. >> Okay? Zero. Let's see whether it is going to work. We're still seeing some output. >> Okay, you've still got one comment. You still got a constraint. >> Yeah, so I should remove this comment and then see whether it would still work. >> Right. >> Yeah. >> We are seeing output again. So that means I could remove the trace statement as well, right? >> Yup. Or don't worry about it. >> Okay. >> Does this solution look like the best that we expected in the- >> Let's take a look at the specification. >> Yup. >> Because I'm using the one that was given in the specification. >> That's right. >> The best objective should be 29 and then it's 4 3 6 2 5 1. Let's see. Okay, best objective, 29 is 4 3 6 2 5 1. It's exactly the answer. >> Okay. >> So it's a good sign, but of course, I should still test using the other data files, right? We actually have a whole bunch of other data files prepared. From poetry one up to poetry five, I'll add them into the model here and then go over here. Let's try with 31. Okay. We have an answer again. The objective is 21. Okay. With poetry one, the objective is 21. Okay. And then, what's the next one? The next one should be 19, let's see. The next one is 19. 19, okay. How about the next one? 3, which is 16. Let's see, has the best answers 16, okay. But then when we look at the answer here- >> Yeah. >> I see a 0 in here separating two E and S stanza. >> Yeah. >> But I thought the best way is really to have all the other stanza towards the end of the sequence. Did you understand what my question is? >> Well, yes. I mean, why should we have some other stanzas, because we know we're only getting value out of the objective? >> Right. >> When we put an E and an S stanza next to each other, that's the only time we actually add something to the objective. But this is the optimal answer, and I guess you should be able to see the reason why, is that we have so many more E stanzas than S stanzas, that we can't actually put them all together. >> Yes. We have four E stanzas and two S stanzas. And the two S stanzas, they are not enough to separate all the E stanzas. >> Exactly. >> And that's why we have to have to insert an other stanza there, to separate the two of them. Okay, so that makes sense. Let's take a look at the fourth one. We have UNSATISFIABLE. And I think that was also predicted in the specification as well. Okay? It said, should be UNSATISFIABLE. Is it an error in my model or is it a correct answer? What do you think, Peter? >> I think you've found all the bugs, Jimmy. >> Yeah. I think so too. But actually, we should go and take a look at what's happening inside the data file here. You could see that we have six E stanzas and zero S stanzas, and then three other stanzas. And then, the reason is actually very similar to the last one, we do not have enough other stanza to separate all the E stanzas. And we do have a constraint in the problem saying that we could not have two stanzas of the same kind in a row. So that's why we have unsatisfiability here. So unless we remove that requirement, we are not going to get anywhere with this data here. Okay, let's try the last data file. This is a difficult one with a fairly large scale data set. And we get up to 85 as an answer. Which is I think between what is best, you know between 80 and 88. So we are doing quite well. >> Yup. >> But I think the problem is just too difficult. That we are not able to find the optimal answer within a short time. >> Well, maybe you can look at adding some extra constraints to the problem or maybe using a different solver and you can experiment with your own solution to see if you can find the optimal solution. >> Okay, let's try that. Let the students try that. >> Exactly. >> Okay. So this is the end of the workshop.