Solving Myst Puzzles with Z3
How I Got Nerd-Sniped Playing VR Myst over ChristmasPosted on December 29, 2021 by Eric Hayden Campbell, debugging help by Frances Campbell
So my sibling, Frances, has a sweet new VR set, and as a family we spent a bunch of time over Christmas nerding out playing Half Life: Alyx, Beat Saber, and Myst. It was a great time! As we were playing, I got nerd-sniped by implementing one of the puzzles in VR Myst. Here’s the puzzle and my Z3 implementation of the solution.
Warning: Minor Spoilers for Myst
One of the early puzzles in Myst is to rotate a set of 3 vertically-stacked gears to a desired using a pair of levers. Once you find the desired combination from the environment (it’s 2-2-1), the trick is to pull the two levers to move the three gears into that position. The catch is that the left lever moves the top two gears up one and the right lever moves the bottom two gears up one. Holding either lever down causes the middle gear to move after the original simultaneous rotation.
So, being the nerd I am, this seemed like a fun cheesy SMT problem. So, I spent the rest of the evening not paying attenion to the game and hacking together an SMTLIB implementation, much to the chagrin of my family. My Dad (who was in the Index) solved the actual problem in only a few minutes, but I wanted to flex my Z3 muscles.
First, I wrote down the Datatypes for the problem. A
Gear is an enum with values
three as below:
(declare-datatype ((Gear 0)) (( (one) (two) (three) )))
Then the user can take one of three
Actions, pull the right lever (
PullRight), pull the left lever (
Hold the previouly pulled lever down. I added a
Noop action to give the solver a bit more freedom in finding solutions.
(declare-datatype ((Action 0)) (( (PullLeft) (PullRight) (Hold) (Noop) )))
Finally, I wrote down a triple,
Gears representing the
(declare-datatypes ((Gears 0)) (( (gears (top Gear) (mid Gear) (bot Gear)) )))
The Semantic Operations
With the datatypes in hand, I wrote down the functions that perform the specific actions. First I defined a helper function
shift that shifts the gear using plus-1-mod-3 arithemetic:
(declare-fun shift ((g Gear)) Gear (if (= one g) two (if (= two g) three one)))
Now, it’s easy to use these to implement the behavior of pulling the left and right levers, by shifting the appropriate gears. The
right functions are defined below.
(define-fun left ((g Gears)) Gears (gears (shift (top g)) (shift (mid g)) (bot g))) (define-fun right ((g Gears)) Gears (gears (top g) (shift (mid g)) (shift (bot g))))
hold function, which corresponds to holding down the previously-pulled lever is defined similarly,
shifting only the middle one.
(define-fun hold ((g Gears)) Gears (gears (top g) (shift (mid g)) (bot g)))
The Transition System
Now, in order to turn this into a synthesis problem, where the solver decides what actions to execute, we need interpret the
Action datatype. There are a few ways to do this,
define-ing the function,
declare-ing it, or
declare-ing it as a relation and
assert-ing the funcitonal constraint. My first attempt was to just
define it, but this triggered a known bug relating to inverted argument order in computing the model.
Instead, I had to declare the interpetation function, called
action, and specify it. For the cleanliness of specifying the transition system, I wrote it as a relation with a functional assertion.
So we define
action to be a relation with the following type:
(declare-fun action (Action Gears Gears) Bool)
Action argument is the action being interpreted, the first gear
g is the input, and the second is the output.
I enforced the requisite functional constraint in the standard way. It says that for any action
a and gear-triple
(action a gin gout1) and
(action a gin gout2) hold for gear triples
gout2 the it must be that
gout2 are equivalent.`
(assert (forall ((a Action) (gin Gears) (gout1 Gears) (gout2 Gears)) (=> (action a gin gout1) (action a gin gout2) (= gout1 gout2))))
Now, we can write the specification. of
action, which is just that if the action is
PullRight), then the output gear is the result of calling
right) on the input gear. Similarly, if the action is
Hold then the output gear is the result of calling
hold on the input gear. Finally, if the action is
Noop then the input and output gear are the same:
(assert (forall ((a Action) (g Gears)) (and (=> (= PullLeft a) (= (takeAction a g) (left g))) (=> (= PullRight a) (= (takeAction a g) (right g))) (=> (= Hold a) (= (takeAction a g) (hold g))) (=> (= Noop a) (= (takeAction a g) g)))))
Solving Myst’s Gear Puzzle
To use this machinery to solve Myst’s gear puzzle, I decided to use an approach related to bounded model checking. That is, first I try to solve the problem using 1 action, then two then three, until Z3 gives me a solution.
First, we need to declare the actions, and the intermediate gear states. It will turn out that we’ll only need six, so we’ll only declare that many
(declare-const act1 Action) (declare-const act2 Action) (declare-const act3 Action) (declare-const act4 Action) (declare-const act5 Action) (declare-const act6 Action) (declare-const g0 Gears) (declare-const g1 Gears) (declare-const g2 Gears) (declare-const g3 Gears) (declare-const g4 Gears) (declare-const g5 Gears) (declare-const g6 Gears)
Now we can write down the transitions that make
g_i the result of executing
(assert (action act1 g0 g1)) (assert (action act2 g1 g2)) (assert (action act3 g2 g3)) (assert (action act4 g3 g4)) (assert (action act5 g4 g5)) (assert (action act6 g5 g6))
Also, to obey the semantics of the game, we need the
Hold action to only occur after another action has occured (If no lever has been pulled, we can’t hold it down). My initial thought was to enforce this using a big disjuntion on the six actions, but Frances pointed out that it suffices to just ensure that the first action isn’t
Hold. Its a little tricky to justify in the presence of
Noop, because a
Hold following a
Noop is hard to realize. However, remembering that
Noop is really the absence of an operation, rather than an operation that does nothing, i.e. that
PullLeft Noop Hold is equivalent to
All this is to say that we add the following assertion to prevent bogus action sequences:
(assert (not (= act1 Hold))
So now we can compute the problem instance by just setting the start state to 3-3-3, which was the start state in the game, and the final state to the solution, 2-2-1. Now you can see why its important to have a
Noop operation. It might be the case that there is a solution that takes only 3 operations! If we care about the minimal solution, then we need that facility.
(assert (= g0 (gears three three three))) (assert (= g6 (gears two two one)))
Then we can compute the solution!
(check-sat) (get-value (act1 act2 act3 act4 act5 act6))
((act1 PullRight) (act2 Noop) (act3 PullLeft) (act4 Hold) (act5 PullLeft) (act6 Hold))
Notice that the last action here is
Noop! This means that we can actually get a solution in 5 actions. We can try this using the following commands
(check-sat) (assert (= g0 (gears three three three))) (assert (= g5 (gears two two one))) (get-value (act1 act2 act3 act4 act5))
Which gives the solution:
sat ((act1 PullLeft) (act2 PullRight) (act3 Hold) (act4 PullLeft) (act5 Hold))
Which gives us a solution in 5 moves!
This model-checking behavior made me wonder about generalizing this problem. How many moves do you need to get from any starting state to any ending state?
Formally, I want to know what the smallest number
N is such that, for any starting gear state
start and ending gear state
end, we can always find a action sequence of length
We’ll do this by slowly increasing the number
N until we find a value that works. We formalize the problem by dualizing it for a given
N. That is, we will attempt to find a pair of gear states,
end such that there is no sequence of
Actions that transforms
end. If this query is
sat, it gives us a pair of start and end states that require more than
N moves to solve. Whereas if it returns
unsat it says that no more than
From the concrete Myst problem instance, we know that we need at least 5 actions, otherwise the pair (
end=2-2-1) is an unsolvable problem. Let’s start with the hypothesis that 5 actions are sufficient.
In this version of the problem, we use a functional declaration rather than a relational one to reduce the number of quantified variables we need. (If we used the above relational approach we would need a new variable for every intermediate state). We call this
takeAction instead of
(declare-fun takeAction (Action Gears) Gears) (assert (forall ((a Action) (g Gears)) (and (=> (= PullLeft a) (= (takeAction a g) (left g))) (=> (= PullRight a) (= (takeAction a g) (right g))) (=> (= Hold a) (= (takeAction a g) (hold g))) (=> (= Noop a) (= (takeAction a g) g)))))
Now we can test whether 5
Actions are sufficient by checking the following query:
(declare-const start Gears) (declare-const end Gears) (assert (forall ((a1 Action) (a2 Action) (a3 Action) (a4 Action) (a5 Action)) (not (= end (takeAction a5 (takeAction a4 (takeAction a3 (takeAction a2 (takeAction a1 start))))))))) (check-sat) (get-value (start end))
But this is insufficient! Giving us the output
sat ((start (gears one one one)) (end (gears three one three)))
I haven’t tried to come up with a solution to check that it actually is impossible in 5 operations, but (for better or for worse) I believe Z3.
So it seems that we need at least 6. Let’s check:
(assert (forall ((a1 Action) (a2 Action) (a3 Action) (a4 Action) (a5 Action) (a6 Action)) (not (= end (takeAction a6 (takeAction a5 (takeAction a4 (takeAction a3 (takeAction a2 (takeAction a1 start)))))))))) (check-sat)
Which lets us conclude that 6 operations are sufficient, which seems sensible, since the search space is small. I could think about this carefully and prove something about this, but I’ll leave that as an exercise for the reader;).