ILP Part 104 — 12 stones riddle

~ afish

This is the one hundred and fourth part of the ILP series. For your convenience you can find other parts in the table of contents in Part 1 – Boolean algebra

Today we are going to solve the 12 Stones Logic Puzzle. We have 12 stones, 11 of them are of equal weight, 1 is of unequal weight (could be lighter or heavier). We can use at most 3 weightings on a balance scale to find the odd stone and tell whether it’s lighter or heavier.

That’s gonna be a little bit tricky to understand, but let’s try it out. We want to implement an ILP model that will give us a recipe for finding the odd stone. Notice, that this problem seems to be even harder than NP class because we can’t verify the solution in polynomial time.

The idea is as follows:

  • We create 24 lists. Each list contains exactly 3 integers. Each integer indicates which subset of stones to put on the left side of the scale, and which stones to put on the right side of the scale.
  • Each list is supposed to determine the “designated stone”, so provide the weightings that will determine that the stone number l is lighter (heavier).
  • For each list, we calculate the results of weightings for every possible input (which stone is odd and how). This gives us a three dimensional list of [listId][number of weighting][which stone is odd and how].
  • For each list, we make sure that we get unique weighting results for the “designated stone” of that list (so results of weightings for that list for other stones must be different).
  • Each list must expect unique result of weightings.
  • When two lists have the same prefix of how to put stones and what result to expect for k first steps, then their k+1-th step must be the same (to have deterministic solution).

That was quite a lot. Let’s see the code:

We set initial conditions in lines 1-3.

Next, we create the variables for weighting results (lines 7-20). That’s the four dimensional array. First dimension indicates which list this refers to. Second dimension indicates which weighting we perform (we have exactly 3 weightings in this scenario). Third level is for indicating which stone is odd (from the input). Last dimension consists of three binaries: whether the left side was lighter (moved up), whether the right side was lighter, whether both sides were equal.

Next, we make sure that we can get only one result for each weighting. This is in lines 22-29.

Next step defines another part of the model we have (lines 32-42). We need to define variables indicating which stones to put on the scale in each step. This is three dimensional array. First dimension indicates which list we have. Second dimension indicates which weighting we consider. Third dimension consists of 24 binaries: first 12 binaries indicate whether a given stone was put on the left side. Next 12 binaries do the same for the right side of the scale.

We now need to encode correctness conditions for the scale. First, we want to make sure, that we put some stones on the scale for each weighting. This is in lines 44-49. We basically take all the variables from the third dimension and make sure they are not all zeroes.

Next, we make sure that if we put a stone on the left side of the scale, then we don’t put it on the right side (and the opposite). This is in lines 51-60.

Next comes the core of the weightings. We need to calculate the result for a given list. ILP will evaluate some subset of stones to put on the scale, and we need to calculate how the scale moves. This is in lines 63-133. We iterate over every list, over every weighting, and over every instance of the input (which stone is odd and how). We then calculate some helper variables indicating whether we put more stones on one of the sides, whether this list is for checking if the stone is lighter or heavier, and whether the special stone has been put on the scale (and on which side). We then encode if conditions to make sure that the result of the weighting is stored properly.

Once we have that, we need to make sure, that our lists can actually identify the solution. We first make sure, that the algorithm we produce is deterministic. For each pair of lists, we take their prefix of k steps, and if the prefixes match (so both lists tried weighting the same stones and expected the same results), then next step in both of the lists (which stones to put on the scale) must be the same. This is in lines 136-163.

Now, we need to make sure that our lists generate unique solutions. First, let’s take some list that is supposed to confirm that the third stone is lighter. We get the subsets of stones to weigh, we get the results of the weightings. We need to make sure that the result is unique, so for every other stone from the input we would get different results in weightings. This is in lines 165-.

Finally, we need to make sure that all 24 lists generate some unique weightings. If that’s the case, then we can be sure, that we get the proper algorithm for finding the odd stone. This is in lines 192-214.

We then solve the problem, and we print the solution.

Here comes some sample output:

Let’s see how to read that. In this simpler example, we consider 4 stones, 3 weightings, we want to find whether the odd stone is heavier or lighter. Notice, that first step in all of the lists is the same. This makes sense (we actually enforced that), because we need to have a deterministic algorithm. Pick any input instance you want to verify. Let’s say, that we assume, that the odd stone is the stone number 3, and the stone is heavier.

We take the first list from the top, and we perform the first weighting. The solution tells us to weigh stones 2 (on the left) and 4 (on the right). We weight them together. Since we know that the odd stone is the stone number 3, we know the result of this weighting will be “both sides are equal”. We see that the first list expected the result to be equal (just like second, fifth, and sixth list). Since our first list is still correct, we move to the second step of the list.

This time we need to weigh stones 3 (on the left) and 4 (on the right). We know the stone number 3 is heavier, we get the result indicated as “<" (meaning that the left side is lower than the right one). We see that the first list expects a different result. So does the second list. Third, fourth, and fifth lists expected different results in the first step. So we move to the sixth list. That list matches our results, so we move to the third step. In the third step we weigh stones 1 and 4 (on the left) with the stone number 3 (on the right). Since we have two stones on the left, the left side is heavier This is exactly what this list expects. So we know that the odd stone is the stone number 3, and that the stone is heavier (as indicated by the list). We can try other inputs. Notice, that only one list will take us through all the steps properly. Let's see another example:

We have 4 stones and 2 weightings this time, but we only need to find the odd stone, without telling whether it's heavier or lighter. Let's assume once again, that our odd stone is the stone number 3, and that the stone is heavier. Let's take first step. We weigh stones 1 and 2, we get that they are equal. There are four lists that match this result. Let's take first list from the top that works for us, that is the list number 5. Second step asks us to weigh stones 4 and 2. We know these stones are equal. However, this time we have at least two lists that match this input. Those are lists 5 and 6. Both of them indicate that the odd stone is the stone number 3, but we can't tell whether the stone is lighter or heavier. Let's take another example. Again, 4 stones and 2 weightings, but this time we want to know whether the stone is heavier or lighter:

CPLEX indicates there are no solutions. This makes sense, we can't tell the solution for sure with 2 weightings only. Here comes the solution for 12 stones and 3 moves:

Big thanks to Tomasz Masternak. We had lots of fun discussing the problem.