After recruiting their army with help from the magical tablet, the brothers started to train the soldiers. Some soldiers fled because of how tough the training was. The brothers observed the loss of the soldiers and wanted to know how many soldiers remained without counting them one by one. Zhang Fei proposed to adopt a similar method to one used by the famous military scientist, Han Xin. They arranged the soldiers in five lines of equal length and two soldiers were left out. They then arranged the soldiers in seven lines of equal length, and two soldiers were left out. They further arranged the soldiers in 12 lines of equal length, and one soldier was left out. But later, Zhang Fei could not work out the number of soldiers using these three arrangements. So, Liu Bei took out the magical tablet to see whether it could help. Preparing the army to take on the yellow-turbaned rebels is hard work and not all of their soldiers are up for it, so some of them are running away. So, our heroes would like to know how many they have left. So, they line them up in a column of rows of five, and they have two left over. And they line them up in rows of seven, and they also have two left over. And they row them up in lines of 12, and they have one left over, so how many soldiers do they have? Well, we can do some maths, and we'll show you how to do it later on. But why do maths when you can just have it answered for you directly? Let's build a MiniZinc model to do it. So we can see that we have an army. Now, how many people do we have in our army? Well, in fact, this is very loose, between 100 and 800 vars. Given we had originally had something like 496, it's not going to be 800, but it's somewhere in that range. We don't think we lost too many of our soldiers. And then the constraint's saying, well, our army mod 5 was 2. We had 2 left over if we lined them up in lines of 5. And our army mod 7 was also 2 because we had 2 left over if we lined them up in lines of 7. And our army mod 12 was 1, And, then, this solve satisfy. So here we're not trying to optimize anything, we're just trying to find a solution. So is there a solution to this problem? So this is a different kind of discrete optimization problem. It's not really a discrete optimization problem, it's a discrete satisfaction problem. Just trying to find a solution to these kind of constraints with this decision variable. So there's no output in this model either, and we'll make use of that, as well. Show what happens when we have no output in our model. So we can run our MiniZinc model as follows. We can just type MiniZinc count.mzn, and we get this result. So, we find the army is 457. And we have our line of ten dashes indicating that we found the solution, and then we don't have a line of ten equals indicating there might be other solutions. Right, so there might be 457 soldiers left, or there might be something else. So we don't actually know. So we'd rather run this. We're going to run MiniZinc with all solutions on. So we're asking it to print out all the possible solutions there are to this problem because what if there's another solution which is 453 or 452? Then we wouldn't be sure how many soldiers we have. Now if we run, we get that the army is 457, That is a solution, and there's no other solutions. Right, so this line here indicates there is no more solutions, so we know the three heroes know that there must be exactly 457 soldiers left in their army. So, the all solutions can also be set in the Configurations tab in the integrated development environment. So for optimization problems, it's the default. For satisfaction problems, like the one we're running here, it's not the default because typically for satisfaction problems you only want one solution. You don't want to see all solutions. But, here, we wanted to make sure that there weren't any other solutions. So, if we look in the IDE, and you go to the Configurations tab, and you run down, so here's the default behaviour, that's normally how you'd run it. You can set user to find behaviour, and ask for all solutions, and then you can get the same behaviour out of the IDE. So note that we didn't have an output statement and we still got some output. So what happens is if you don't declare an output statement then MiniZinc will output all the declared variables in your model which are not assigned to an expression in your model. So, here, we only had one variable and so that was output. And this is a very useful feature for simple models. If you're building simple models, you don't have to worry about output, you'll get a very useful output out of MiniZinc just by having no output item. But for later models, you'll be interested in building specific output functions to write out the bits of the decisions that you're interested, or writing out the decisions in a way that's understandable to you. So we could've done this without using MiniZinc because there's a Chinese remainder theorem which is about solving simultaneous congruences. And we could write down here's all the algebra for doing this. We know that our army = 5t + 2, where t is some integer, because it was, remember, rows of five plus two left over. So that's saying it was 2 mod 5. Similarly, our army is equal to 7u, some integer u + 2 because it was equal to 2 mod 7. And it was equal to 12v + 1, as well, because it was 1 mod 12. And then we have to do some substitution. So if we substitute A into B, we're going to get that 5t + 2 = 2 mod 7. And then we have to do a bit of multiplication. We subtract over here, we're going to get that 5t = 0 mod 7, And then if we multiply both sides by the number, the inverse of 5, we're going to get that t is 0 mod 7, in other words that t is 7w. So, now, we can substitute that back into D. Sorry, we can use D to substitute back into A, and we know that the army is 2 + 35w, for some number, w. Now, we can use that to substitute into C. And we're going to get 2 + 35w is 1 mod 12. With a bit more simplification, we'll find that w is 1 mod 12. And then we can substitute that back, and we'll end up with this thing that army is 37 + 420x. And you can see, basically, the only solution to this in the range that we're interested in is that the army is 457. So, in summary, here we're seeing a satisfaction problem. So sometimes we're interested in just finding a solution, not necessarily finding the best solution, for a particular objective. And we've also seen that constraints don't just need to be linear equalities and inequalities. So here we've used modulo, and we've used disequality, or we could also use multiplication, division. And we'll see many more complex constraints later on. One of the powers of modern modeling language is being able to write down very complex, highly non-linear constraints, and have our solver solve them.
