brhfl.com

I’ve been playing a mobile room-escaping-themed puzzle game (I believe the title is simply Can You Escape 50 Rooms) with a friend, and there was a certain puzzle that we got stuck on. By stuck, I mean that we certainly would’ve figured it out eventually, but it was more frustrating than fun, and it consumed enough time that I thought up a fun way to cheat. I am not against cheating at puzzles that are failing to provide me with joy, or that I’m simply unable to complete, but I have a sort of personal principle that if I’m going to cheat, I’m going to attempt to learn or develop something in the process. If I cheat at a crossword, for example, I don’t just look at the answer key; I do research on the subject to figure it out. In this case, I decided to use a language that I’ve only barely dabbled in to solve the puzzle.

It’s worth noting that this is about the solve and not the solution, and I’m not including a solution here. There shouldn’t be any spoilers except to show/explain one puzzle from the game. With that said, the puzzle gives you something like this:

Fifteen discs numbered 1-15 can be moved freely among fifteen positions. There is essentially an outer ring of seven discs, an inner ring of seven discs, and a center disc. This forms seven diamonds: we can imagine a disc from the outer ring as the top of the diamond, then that connects to two discs ‘below’ it in the inner ring, and finally the center disc is the bottom of the diamond. So in the example above, 8-14-6-13 makes a diamond, 10-6-5-13 makes a diamond, and so on. The puzzle is to rearrange these so the sum of the four discs in every diamond is 30.

Every diamond shares one disc with every other diamond (the center), has one unique disc (the disc in the upper ring), and has two discs that are each shared with one other diamond (the discs in the inner ring). A lot of my intuitive thoughts proved impossible pretty quickly, and it devolved into a lot of random positioning between the two of us. When I was given the greenlight to write a program to solve it for us, I figured I could either brute-force it in any language, or I could do something fun and use Sentient.

Sentient is perfect for this sort of task. You don’t need to know how to solve a thing, you just give it a bunch of rules and it sorts that out itself. We’re going to map our fifteen positions to indices in an array; their respective values will be the corresponding disc. Let’s map out the indices:

Our seven diamonds are thus 0-1-2-8, 0-2-3-9, 0-3-4-10, 0-4-5-11, 0-5-6-12, 0-6-7-13, and 0-7-1-14. Our rules are that the sum of each of those sets of values be 30, each value be between 1 and 15, and each value be unique. I’m sure there’s a cleaner way to have coded this, but the following works:

array15<int5> discs;
invariant discs.all?(function (bt) {
	return bt.between?(1,15);
	});
invariant discs.uniq?;
invariant [discs[0],discs[1],discs[2],discs[8]].sum == 30;
invariant [discs[0],discs[2],discs[3],discs[9]].sum == 30;
invariant [discs[0],discs[3],discs[4],discs[10]].sum == 30;
invariant [discs[0],discs[4],discs[5],discs[11]].sum == 30;
invariant [discs[0],discs[5],discs[6],discs[12]].sum == 30;
invariant [discs[0],discs[6],discs[7],discs[13]].sum == 30;
invariant [discs[0],discs[7],discs[1],discs[14]].sum == 30;
expose discs;

We begin by declaring the array. Arrays in Sentient must be dimensioned at initialization; ours has fifteen values, so we initialize with array15. We also have to declare what it will contain, which in our case is integers. While array15<int> would have worked just fine, we can specify that we’re only using 5 bits¹ worth of integer values to speed up the search, hence array15<int5>. The array is called discs.

Our rules are written with invariant statements. These should be pretty straightforward: a function that checks if each value is between? 1 and 15, a requirement that everything be uniq?ue, and then one rule each for our seven summation requirements. The final expose command lets Sentient know what we want to see as our results. That’s it! Even on a slow in-browser version of Sentient, a set of results comes back in a handful of seconds. You can also ask Sentient to try to come up with multiple solutions; curious if there was only one valid solution to the diamonds puzzle, I asked for and was returned three unique solutions.