Hadean Lands post-completion discussion (spoilers galore!)

Oh, I see. You’re figuring one would solve other puzzles in the middle of awakening the dragons. That may very well be needed!

Yeah, I think you want to think of each reset as a chunk in which you should try and complete the maximum number of things. Calculating that maximum number depends on resource scarcity, so it’s a bit of a jigsaw - which puzzles you can fit together within the same reset chunk - followed by an optimisation problem - which is the optimal fit of those chunks.

You can compile Glulxe (or Git) with CheapGlk. I wrote copious test scripts based on this combination.

Oh, you mean doing the sensible thing? Why would I ever do that? (Works perfectly. Thanks! :slight_smile: )

For anyone else who is interested, here is a shell script that executes a (minimal, as far as I can tell) completion of the first ritual. (Not very interesting, but I have to go to work soon! :wink: )

[spoiler][code]#!/bin/sh

GLULXE=“$HOME/src/glulxe/glulxe”
HADEAN_LANDS=“$HOME/games/hadean-lands/HadeanLands.gblorb”

“$GLULXE” “$HADEAN_LANDS” <<END | fmt

Yes, I’ve played IF before.

y

Let’s exit the Secondary Alchemy Lab.

x table
x bench
x sheet
get all
open ginger
put bolt in bound
say simple sealing
say essential nature
wave rosemary
say lesser phlogistical
get bolt
touch bolt to panel
d
END
[/code][/spoiler]

Couple thoughts on this thread:

  • Some of the notes about the NPCs are signed “N”, but others are signed “M”. It doesn’t seem like any of the above theorizing noted this.

  • After you get out of the Med Wing, you still have a scalpel marked with the symbol of prophylaxis. Every other alchemical symbol fades after it’s no longer needed, so I kept expecting to find something else to use it on. Never did, but I’m still suspicious there’s something.

Zarf’s game website has a link to this talk he gave a couple weeks ago:
https://soundcloud.com/handeyesociety/andrew-plotkin-hadean-lands-wordplay-2014
in which he admits that he built a SAT solver (or something that sounds pretty much like one) to test the game with.

Unfortunately, it sounds like he was mostly thinking about it in terms of proving that players couldn’t “cheat” by finding ways to bypass puzzles he meant them to have to solve, and not in terms of proving that players could get to the end no matter which path (eg, choice of first dragon to waken) they took. I’d have thought you’d want to test from both perspectives …

The talk is worth listening to, if you have half an hour to spare (though you could probably skip the first 9-10 minutes which are somebody else introducing him).

Zarf’s puzzle exploration tool is called PlotEx: eblong.com/zarf/plotex/index.html

It’s only unfortunate if I screwed up and left the ending unreachable by one path! But I didn’t. (Leaving aside the question of ending variations, which I considered optional bonuses.)

I used two different test tools in development, actually. PlotEx is the dependency checker – it takes a model of the game and checks what states are reachable or not. RegTest is a fancy wrapper around the cheapglk rig I mentioned earlier – it tests the behavior of the game itself. (See eblong.com/zarf/plotex/regtest.html)

Obviously I used PlotEx during the design phase, before I started writing code. But I didn’t model absolutely everything in the game; at that stage I was designing around “critical resources”. I knew I’d be adding a lot of “flavor resources” to bulk out the ritual structure.

Once I started writing code, I mostly relied on RegTest. I went back to add some of the flavor resources to PlotEx, but generally in a “have you gained access to X?” way rather than strict quantity counting. (Consumable resources multiply the number of states; find-and-keep-forever resources do not. The flavour items are either unlimited supplies, like sand or the aroma impets, or items that you only need once.)

Here’s the thing: PlotEx is great for proving that certain states are not possible. To prove that a state is possible, you want to use RegTest and write a transcript that reaches it in the actual game! If your model is wrong, PlotEx can give a false result, but RegTest never does. (Unless you put debug commands in the transcript.)

This did happen at one point. I had never modelled gur avpxry ebq at all, because it’s only used it one ritual. When I got to the point of writing RegTest scripts for finishing the game, I ran out of the stuff. It had accidentally become a critical resource – which I hadn’t intended. So I had to add more very late in development. PlotEx could have revealed this problem if I’d modelled absolutely everything in the game, but that would have been wasted effort.

Here’s the confession: I have RegTest scripts to demonstrate reaching each dragon first, but not completing the entire game after reaching each dragon first. I’ve only finished the game Baros-first! That was somewhat lax, but I figured I had a good grasp of the high-level constraints – what happens when each dragon is reached. Between the old PlotEx model and my understanding of the game, I was confident that the ending was always reachable for everybody.

That’s intense. Thanks for the writeup :slight_smile: The methodology of making a complex metapuzzlegame sounds like it’s far, far more difficult than playing a complex metapuzzlegame.

[Warning: computer science content ahead.]

The reason I suggested a SAT solver originally is that while the number of states explodes exponentially, I imagine that the whole game only has a search space numbered in the thousands of boolean variables. (That is, while there may be 2^10000 states, that suggests there’s only 10000 variables to search.) While this is a big, difficult problem (especially if one is trying to solve it by hand or with straightforward tools), modern SAT solvers can grind though it with ease. (Which is a very interesting result in itself. From my reading of the academic literature, engineering has far outstripped theory in this area. We have no idea why these tools work as well as they do!)

The main difficulty for determining minimum resets, I think, is how the heck does one encode the problem in the first place!? This involves not just the (relatively straightforward, if tedious) task of tracking all of the dependencies between resources and puzzles, but one also has to encode what has been reached so far in reset number X and what has been consumed so far in reset number X. So, you have to track dependencies each of X times, and thanks to existing players we know X is less than or equal to 36. So I think the problem is definitely tractable, though it’s going to be a lot of work (both on collecting and writing down the single-reset dependencies, and on collecting and writing down the multi-reset dependencies).

(Finally, the SAT solver won’t give you minimum resets on it’s own. It’ll just tell you if the dependencies can be satisfied. You’ll have to re-run the solver with 36 resets, then with 35, then with 34, etc., until it can’t be solved any more. Then you’ll have your minimum resets.)

I just made a very nice dish with saffron, and I keep fantasising about rubbing it against my laptop screen.

1 Like

Can you use PlotEx to prove that there’s no way to plant the intensional ballast under the Birdhouse and beat the game? Seems like the only way we’ve found to use the ballast when Syndesis is active is to put it in one of the other locations, e.g. the Garden Pool.

Also, when do backers get to see the source code?

I did it in 31 resets, and I’m sure I wasn’t perfectly efficient, so X is less than that even.

Are you sure you want me to confirm that? :slight_smile:

I expect to start tackling that stuff next week.

I’m not sure how a SAT solver helps.

You could reduce all of Hadean Lands to a PlotEx problem, using a giant Reset action that sets a bunch of hasX qualities to False, a bunch of availableX qualities to True, while leaving knowledge-qualities untouched.

I didn’t dig into the algorithmic details of PlotEx, but I’m skeptical that would terminate in any reasonable amount of time.

Fortunately, Hadean Lands has a bit of extra structure that can help us: what I’ll call “knowledge qualities” never reset and are never consumed, whereas “material qualities” are. (Ignoring some fine details such as the dragon awakening order, but let’s be honest, the 4! different dragon combinations are the least of our worries. Fix one of them for now.)

So I might implement a Hadean Lands optimal play solver as follows:

  1. Call two subsets of knowledge qualities incomparable if neither is a subset of the other. Use PlotEx to find the maximal set of incomparable subsets that can be reached without resetting. In the worst case there are O(n!/sqrt(n)) of these, where n is the number of knowledge qualities, but in practice I image the cardinality of the maximal set is much lower.
  2. If Win is an element of one of these subsets, terminate.
  3. For each subset S I found in step 1, find a maximal set of incomparable subsets that can be reached without resetting, starting from state S. Take the union of all of these maximal sets and remove elements until you again have a maximal set of incomparable subsets, representing all knowledge states you could have achieved so far. With memoization I don’t think this step is substantially harder than step 1 where you start from just one initial state.
  4. Go to 2.

The short answer is “don’t reinvent the wheel.”

The long answer is that solving Hadean Lands is–at worst–in the NP complexity class (because it takes linear time to verify a solution), and SAT solvers are the standard tool for solving NP problems. (Also, frankly, a SAT solver would find the solution much, much faster than anything I’d write, which is a sobering thought given how long I’ve been a programmer. :stuck_out_tongue: )

As I said, the hard part is building a dependency graph of all resources and puzzles. :confused:

Yes, it’s in NP, but how are you reducing it to SAT? Just checking all possible sequences of actions until you find one that Wins? First, this doesn’t quite work: answering the decision problem “can Hadean Lands be beaten in N resets” will necessarily terminate in finite time only if the answer is affirmative. Second, I can guarantee this approach will be indeed be much, much slower than anything smarter you code up yourself!

My plan would be to simply encode whether a ritual is accessible in a reset as a boolean variable, and whether a ritual was performed in a reset as a boolean variable. Dependencies (“IF x THEN y”) are easily encoded as a simple expression, as are mutual exclusions (“NOT x OR NOT y”). That is, for example, one might encode that one cannot perform the aura invisibility ritual unless the knowledge was discovered in an earlier reset, and that one cannot perform both the aura invisibility ritual and the quartz aura imitation ritual in the same reset, or that one cannot perform a given ritual in a reset unless they had first performed some other ritual.

Assuming I’m not off my mark, if there are 50 rituals and a maximum of 30 resets to try and 2 variables per ritual, we’re looking at 3000 variables total, and maybe quadratically as many formulae. That’s not very many. (Even if we don’t consider rituals the only resource, we’re still only talking a couple hundred resources at most. Still easily solvable.)

So then you’ll have a problem representation such that a solver can say “Yes, you can perform the True Great Marriage within N resets.” and show you which reset each ritual was performed in. Then you just fiddle with N until you find the minimum.

At least, I think that’s a general enough representation to solve HL. I’m the kind of person who only really understands something by doing it, so maybe I need to spend some of my Thanksgiving week just buckling down and giving it a try. :smiley:

[Edited for clarity.]

Let’s look at a simpler game, One Element Hadean Lands.

You start with elemental fire. You can use it either to learn the Great Marriage (which consumes the Fire) or to perform it (which wins the game).

How would you encode OEHL as a SAT problem?

Learning the great marriage requires fire

learn_great_marriage_1 => fire_used_1
learn_great_marriage_2 => fire_used_2

#Performing the great marriage requires that it be learned in an earlier reset and that the fire isn’t consumed
performed_great_marriage_1 => learn_great_marriage_1 & !fire_used_1
performed_great_marriage_2 => (learn_great_marriage_1 | learn_great_marriage_2) & !fire_used_2

fire_used_1 & learn_great_marriage_1 & performed_great_marriage_2 is a solution

I think this does it? But it wouldn’t generalize, because I can’t figure out how to encode the fire usage properly.

Good question. Let’s posit that the game can be won in two resets.

We have the following variables:

know/learn_marriage/0 perform/learn_marriage/0 know/learn_marriage/1 perform/learn_marriage/1 know/marriage/0 perform/marriage/0 know/marriage/1 perform/marriage/1

We have the following rules. (In a SAT solver, each of these would get ANDed together.)

[code]# We start knowing the learn marriage ritual.
know/learn_marriage/0

We want to prove that we can win the game before running out of resets.

perform/marriage/1

We can perform any ritual we know, so long as it doesn’t

conflict on resource. (That is, we cannot perform both

learn marriage and the Great Marriage, since they both need

elemental fire.)

IF know/learn_marriage/0 AND NOT perform/marriage/0 THEN perform/learn_marriage/0
IF know/learn_marriage/1 AND NOT perform/marriage/1 THEN perform/learn_marriage/1
IF know/marriage/0 AND NOT perform/learn_marriage/0 THEN perform/marriage/0
IF know/marriage/1 AND NOT perform/learn_marriage/1 THEN perform/marriage/1

Performing the learn marriage ritual teaches us the marriage ritual.

IF perform/learn_marriage/0 THEN know/marriage/0
IF perform/learn_marriage/1 THEN know/marriage/1

If we know a ritual in any reset, then we know it in subsequent resets.

IF know/learn_marriage/0 THEN know/learn_marriage/1
IF know/marriage/0 THEN know/marriage/1[/code]

In theory (I havn’t tested this to make sure I didn’t screw up), it’ll give the following result:

know/learn_marriage/0 TRUE perform/learn_marriage/0 TRUE know/learn_marriage/1 TRUE perform/learn_marriage/1 FALSE know/marriage/0 TRUE perform/marriage/0 FALSE know/marriage/1 TRUE perform/marriage/1 TRUE

That is, we performed learn marriage in reset 0 and performed the great marriage in reset 1 (and won the game).

Now, if that all looks excessively complicated, it’s because no sane person would write it all by hand. We’d write a templated script that goes and writes the real thing for us.

Optimality, one can’t encode resources as variables, since it always has to be set. (That is, SAT solving is declarative and independent of time. You can’t have a variable be set and then unset… it always has to be one way or the other.) Instead, you have to encode whether a resource was used on X, or a resource was used on Y, and then say that you can’t use it on both. (That is, if you want to encode a resource, it takes N bits, where N is the number of things it can be used on. This is why I just treat rituals as the resource–it’s simpler, though it requires thinking a little meta.)